Restricting the shrink-and-append step

The value of the principalization family on a relatively compact open U (Assembly.lean) is a shrink-and-append step (shrinkAppend of Hironaka/Resolution/Analytic/OrderReduction/FamilyChain.lean): the disjoining list L over the shrinking open W, pulled back along the open inclusion U → W, followed by the order-reduction value read on the reading open, carried along the corestricted lift, with the empty rounds erased. The compatibility clause of the compatible-family form ([Wlo09, Theorem 2.0.3 (4)]; Kollár's functoriality for smooth morphisms, [Kol07, 34.1], per open) compares the value on U ≤ V: this module proves the general restriction law of the step,

• shrinkAppend_pullback_eraseEmpty: pulling L.shrinkAppend h B back along a further local isomorphism k and erasing the empty rounds gives L.shrinkAppend (h ∘ k) B', up to empty rounds, whenever B' is B restricted to the smaller reading open (up to empty rounds) — by induction on L, the cons step being liftStep_comp, the nil step the commutation of eraseEmpty with pull-back (eraseEmpty_pullback_eraseEmpty) and the functoriality of the pull-back of a sequence (pullback_comp; [Kol07, 30.1]);

together with the bookkeeping it needs: the reading opens are nested (range_pullbackLiftLast_subset_of_comp), the last-stage lift carries the reading open of a composite into the reading open (image_pullbackLiftLast_liftRange_subset), eraseEmpty respects a common head (eraseEmpty_cons_congr), and the nil case in plain variables (pullback_pullback_eraseEmpty_of_restrict). The statements carry the composite as a separate map e with h.comp k = e so that the induction can instantiate it with liftStep e (the equation liftStep (h ∘ k) = liftStep h ∘ liftStep k is propositional; it enters through subst). Used by ValueRestrict.lean, ShrinkAppendPullback.lean and the functoriality for closed embeddings (Hironaka/Resolution/Analytic/OrderReduction/ClosedEmbeddingFam.lean).

eraseEmpty and the constructors of the step

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_cons_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) {R₁ R₂ : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)} (h : R₁.eraseEmpty = R₂.eraseEmpty) : (cons hY R₁).eraseEmpty = (cons hY R₂).eraseEmpty

eraseEmpty respects a common head: two lists with the same first centre whose tails agree up to empty rounds agree up to empty rounds.

theorem AnalyticManifold.BlowUpSequence.shrinkAppend_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (B : BlowUpSequence ψ₀ (((nil M).stage (Fin.last (nil M).length)).restrict ((nil M).liftRange h hh))) : (nil M).shrinkAppend h hh B = B.pullback ((nil M).liftCorestrict h hh) ⋯

The shrink-and-append step of the empty list: the appended list pulled back along the corestriction of h onto its range.

theorem AnalyticManifold.BlowUpSequence.shrinkAppend_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (rest : BlowUpSequence ψ₀ (Manifold.blowUp ψ₀ hY)) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (B : BlowUpSequence ψ₀ (((cons hY rest).stage (Fin.last (cons hY rest).length)).restrict ((cons hY rest).liftRange h hh))) : (cons hY rest).shrinkAppend h hh B = cons ⋯ (rest.shrinkAppend (liftStep h hh hY) ⋯ B)

The shrink-and-append step of cons hY rest: the pulled-back first centre, then the step of rest along the lift of h to the blow-ups (liftStep).

The reading opens of a composite

theorem AnalyticManifold.BlowUpSequence.range_pullbackLiftLast_subset_of_comp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (k : AnalyticMap P N) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k → ∀ (e : AnalyticMap P M) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e), ContMDiffMap.comp h k = e → Set.range ⇑(L.pullbackLiftLast e he) ⊆ Set.range ⇑(L.pullbackLiftLast h hh)

The reading open of a composite h ∘ k lies in the reading open of h: the ranges of the last-stage lifts are nested.

theorem AnalyticManifold.BlowUpSequence.image_pullbackLiftLast_liftRange_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M X P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (π : AnalyticMap X M) (hπ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑π) (j : AnalyticMap P X) (hj : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑j) (e : AnalyticMap P M) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e) : ContMDiffMap.comp π j = e → ⇑(L.pullbackLiftLast π hπ) '' ↑((L.pullback π hπ).liftRange j hj) ⊆ ↑(L.liftRange e he)

The last-stage lift of π carries the reading open of j (through π^* L) into the reading open of the composite π ∘ j (through L).

The restriction law of the step

theorem AnalyticManifold.BlowUpSequence.pullback_pullback_eraseEmpty_of_restrict {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {X N P : AnalyticManifold 𝕜 E} {R R' : TopologicalSpace.Opens X.carrier} (hle : R' ≤ R) (B : BlowUpSequence ψ₀ (X.restrict R)) (B' : BlowUpSequence ψ₀ (X.restrict R')) (hB : B'.eraseEmpty = (B.pullback (X.restrictLE hle) ⋯).eraseEmpty) (c₁ : AnalyticMap N (X.restrict R)) (hc₁ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑c₁) (k : AnalyticMap P N) (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) (c₂ : AnalyticMap P (X.restrict R')) (hc₂ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑c₂) (hcomp : ContMDiffMap.comp c₁ k = ContMDiffMap.comp (X.restrictLE hle) c₂) : ((B.pullback c₁ hc₁).pullback k hk).eraseEmpty = (B'.pullback c₂ hc₂).eraseEmpty

The nil case of the restriction law, in plain variables: two pull-backs of B along maps into the reading open agree with the pull-back of the restricted list B' along the composite, up to empty rounds (eraseEmpty_pullback_eraseEmpty, pullback_comp, pullback_congr).

theorem AnalyticManifold.BlowUpSequence.shrinkAppend_pullback_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N P : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) (k : AnalyticMap P N) (hk : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑k) (e : AnalyticMap P M) (he : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑e) : ContMDiffMap.comp h k = e → ∀ (B : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange h hh))) (B' : BlowUpSequence ψ₀ ((L.stage (Fin.last L.length)).restrict (L.liftRange e he))) (hle : L.liftRange e he ≤ L.liftRange h hh), B'.eraseEmpty = (B.pullback ((L.stage (Fin.last L.length)).restrictLE hle) ⋯).eraseEmpty → ((L.shrinkAppend h hh B).pullback k hk).eraseEmpty = (L.shrinkAppend e he B').eraseEmpty

The shrink-and-append step restricts (the compatibility clause of [Wlo09, Theorem 2.0.3 (4)]; [Kol07, 34.1] per open). Pulling L.shrinkAppend h B back along a further local analytic isomorphism k and erasing the empty rounds is L.shrinkAppend (h ∘ k) B' up to empty rounds, whenever B' is B restricted to the smaller reading open, up to empty rounds. The composite is carried as a separate map e with h.comp k = e so the induction can instantiate it with liftStep e (liftStep_comp).