The push-forward of a list of centres commutes with pull-back along a local analytic isomorphism

In the proof of [Kol07, Lemma 102] one pulls back by h, restricts to h⁻¹(Eʲ) = Eʲ, and pulls back by h|_{h⁻¹Eʲ}: the push-forward of a blow-up sequence of a closed submanifold S ⊆ M (BlowUpSequence.pushforward, [Kol07, Definition 30, 30.3]) pulled back along a local analytic isomorphism g : N → M is the push-forward, from g⁻¹(S) ⊆ N, of the sequence pulled back along the restricted local isomorphism g|_{g⁻¹S} : g⁻¹S → S:

• IsClosedSubmanifold.restrictInvFunOfPreimage, restrictPartialDiffeomorphOfPreimage, IsClosedSubmanifold.isLocalDiffeomorph_restrictMap, surjective_restrictMap: the restricted map is a local analytic isomorphism between the bundled submanifolds, surjective when g is (the codimension-one lemmas of Hironaka.Resolution.Analytic.OrderReduction.Functoriality, at any codimension s);
• PushforwardStage.IsPullbackStage P P' G gᵢ, the invariant of the induction: a local isomorphism G : P'.space → P.space of ambient stages with P'.sub = G⁻¹(P.sub) and the square P.incl ∘ gᵢ = G ∘ P'.incl; IsPullbackStage.preimage_imageVal (the pulled-back pushed centre is the pushed pulled-back centre), and the step isPullbackStage_blowUpStep: the invariant propagates through blowUpStep along the lift stepMap of G (liftStep composed with the identification of the two blow-ups of the same centre), the next square by uniqueness of lifts on the dense complement of the exceptional divisor, the next sub-identity by strictTransformSet being the closure of a preimage under the open map stepMap;
• BlowUpSequence.pushforward_pullback: the statement above, by induction on the list through pushforwardAux_pullback (any pair of stages with the invariant; cons_congr_heq and heq_pullback_of_heq identify the two cons whose centres are propositionally equal).

This is used to show that the functors built by descent commute with local isomorphisms.

The restricted map at any codimension

noncomputable def Manifold.IsClosedSubmanifold.restrictInvFunOfPreimage {𝕜 : 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) {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΨ : Set.EqOn (⇑h) (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : ⋯.toAnalyticManifold.carrier) (y : hS.toAnalyticManifold.carrier) : ⋯.toAnalyticManifold.carrier

BD.restrictInvFunOfPreimage at any codimension (as in the proof of [Kol07, Lemma 102]): the local inverse Ψ of h read on the bundled submanifolds.

Equations

• Manifold.IsClosedSubmanifold.restrictInvFunOfPreimage h hh hS Ψ hΨ p₀ y = if hy : ↑y ∈ Ψ.target then ⟨Ψ.invFun ↑y, ⋯⟩ else p₀

theorem Manifold.IsClosedSubmanifold.restrictInvFunOfPreimage_of_mem {𝕜 : 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) {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΨ : Set.EqOn (⇑h) (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : ⋯.toAnalyticManifold.carrier) {y : hS.toAnalyticManifold.carrier} (hy : ↑y ∈ Ψ.target) : restrictInvFunOfPreimage h hh hS Ψ hΨ p₀ y = ⟨Ψ.invFun ↑y, ⋯⟩

The value of restrictInvFunOfPreimage on the target of Ψ.

noncomputable def Manifold.IsClosedSubmanifold.restrictPartialDiffeomorphOfPreimage {𝕜 : 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) {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (Ψ : PartialDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) N.carrier M.carrier ⊤) (hΨ : Set.EqOn (⇑h) (↑Ψ.toPartialEquiv) Ψ.source) (p₀ : ⋯.toAnalyticManifold.carrier) : PartialDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⋯.toAnalyticManifold.carrier hS.toAnalyticManifold.carrier ⊤

BD.restrictPartialDiffeomorphOfPreimage at any codimension: a local inverse of h restricted to the bundled submanifolds h⁻¹(S) and S is a partial diffeomorphism agreeing with the restricted map on h⁻¹(S) ∩ Ψ.source.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.IsClosedSubmanifold.isLocalDiffeomorph_restrictMap {𝕜 : 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) {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑(⋯.restrictMap hS ⇑h ⋯ ⋯)

BD.isLocalDiffeomorph_restrictMap at any codimension (the proof of [Kol07, Lemma 102] "h|_{E^j_Y} is also a smooth surjection"): the restriction of a local analytic isomorphism to the preimage of a closed submanifold is a local analytic isomorphism between the bundled submanifolds.

theorem Manifold.IsClosedSubmanifold.surjective_restrictMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (h : AnalyticMap N M) {S : Set M.carrier} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (hS' : IsClosedSubmanifold ψ (⇑h ⁻¹' S) s) (hs : Function.Surjective ⇑h) : Function.Surjective ⇑(hS'.restrictMap hS ⇑h ⋯ ⋯)

BD.surjective_restrictMap at any codimension: the restriction of a surjection to the preimage of a submanifold is a surjection onto the submanifold.

theorem Manifold.isBlowUp_blowUpπ_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y Y' : Set M.carrier} {c : ℕ} (e : Y' = Y) (hY' : IsClosedSubmanifold ψ Y' c) : IsBlowUp ψ Y c ⇑(blowUpπ ψ hY')

A chosen blowing-up along a set propositionally equal to Y is a blowing-up with centre Y.

theorem Manifold.heq_liftStep_comp_diffeomorph {𝕜 : 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) {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {Y' : Set N.carrier} (hY' : IsClosedSubmanifold ψ Y' c) (e : Y' = ⇑h ⁻¹' Y) : AnalyticManifold.BlowUpSequence.liftStep h hh hY ≍ ContMDiffMap.comp (AnalyticManifold.BlowUpSequence.liftStep h hh hY) (IsBlowUp.diffeomorph ⋯ ⋯ ⋯).toAnalyticMap

The lift of h from a blowing-up of a centre propositionally equal to h⁻¹(Y), through the identification of the two blowings-up, is heterogeneously the lift liftStep.

The invariant

structure Manifold.PushforwardStage.IsPullbackStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) (P' : PushforwardStage ψ s Tᵢ') (G : AnalyticMap P'.space P.space) (gᵢ : AnalyticMap Tᵢ' Tᵢ) : Prop

The invariant of the induction in the proof of [Kol07, Lemma 102], at one stage: G : P'.space → P.space is a local analytic isomorphism of the ambient stages under which the strict transform P'.sub is the preimage of P.sub and the inclusions of the bundled stages commute with gᵢ : Tᵢ' → Tᵢ.

• isLocalDiffeomorph : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑G
• sub_eq : P'.sub = ⇑G ⁻¹' P.sub
• square (q : Tᵢ'.carrier) : P.incl (gᵢ q) = G (P'.incl q)

theorem Manifold.PushforwardStage.IsPullbackStage.preimage_imageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (Z : Set Tᵢ.carrier) : ⇑G ⁻¹' ⋯.imageVal (⇑P.iso '' Z) = ⋯.imageVal (⇑P'.iso '' ⇑gᵢ ⁻¹' Z)

The pull-back along G of the pushed-forward centre (j_i)_* Z is the pushed-forward pulled-back centre (j_i')_* (gᵢ⁻¹ Z).

The step

noncomputable def Manifold.PushforwardStage.stepIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) (blowUp ψ ⋯).carrier (blowUp ψ ⋯).carrier ⊤

The identification of the blowing-up of P'.space along the pushed pulled-back centre with the blowing-up along the pulled-back pushed centre (the same set, preimage_imageVal).

Equations

• Manifold.PushforwardStage.stepIso h hgᵢ hZ = Manifold.IsBlowUp.diffeomorph ⋯ ⋯ ⋯

theorem Manifold.PushforwardStage.blowUpπ_stepIso {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (p : (blowUp ψ ⋯).carrier) : (blowUpπ ψ ⋯) ((stepIso h hgᵢ hZ) p) = (blowUpπ ψ ⋯) p

noncomputable def Manifold.PushforwardStage.stepMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : AnalyticMap (blowUp ψ ⋯) (blowUp ψ ⋯)

The lift of G to the next stages: liftStep after the identification stepIso.

Equations

• Manifold.PushforwardStage.stepMap h hgᵢ hZ = ContMDiffMap.comp (AnalyticManifold.BlowUpSequence.liftStep G ⋯ ⋯) (Manifold.PushforwardStage.stepIso h hgᵢ hZ).toAnalyticMap

theorem Manifold.PushforwardStage.isLocalDiffeomorph_stepMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑(stepMap h hgᵢ hZ)

theorem Manifold.PushforwardStage.blowUpπ_stepMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (p : (blowUp ψ ⋯).carrier) : (blowUpπ ψ ⋯) ((stepMap h hgᵢ hZ) p) = G ((blowUpπ ψ ⋯) p)

The lift lies over G.

theorem Manifold.PushforwardStage.blowUpπ_incl_blowUpStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {Z : Set Tᵢ.carrier} {c : ℕ} (P : PushforwardStage ψ s Tᵢ) (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (p : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ).carrier) : (blowUpπ ψ ⋯) ((P.blowUpStep hZ ⋯).incl p) = P.incl ((blowUpπ (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ) p)

The blow-down of a pushed-forward point is the push-forward of its blow-down (restrictMap_blowUpStep_iso read through the inclusions).

theorem Manifold.PushforwardStage.incl_blowUpStep_liftStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (q : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) ⋯).carrier) : (P.blowUpStep hZ ⋯).incl ((AnalyticManifold.BlowUpSequence.liftStep gᵢ hgᵢ hZ) q) = (stepMap h hgᵢ hZ) ((P'.blowUpStep ⋯ ⋯).incl q)

The next square: the two lifts of the inclusions agree, by uniqueness of lifts on the dense complement of the exceptional divisor.

theorem Manifold.PushforwardStage.isPullbackStage_blowUpStep {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P : PushforwardStage ψ s Tᵢ} {P' : PushforwardStage ψ s Tᵢ'} {G : AnalyticMap P'.space P.space} {gᵢ : AnalyticMap Tᵢ' Tᵢ} (h : P.IsPullbackStage P' G gᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : (P.blowUpStep hZ ⋯).IsPullbackStage (P'.blowUpStep ⋯ ⋯) (stepMap h hgᵢ hZ) (AnalyticManifold.BlowUpSequence.liftStep gᵢ hgᵢ hZ)

The invariant propagates through one blow-up step.

The induction

theorem Manifold.PushforwardStage.pushforwardAux_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ Tᵢ' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) (P' : PushforwardStage ψ s Tᵢ') (G : AnalyticMap P'.space P.space) (gᵢ : AnalyticMap Tᵢ' Tᵢ) (hgᵢ : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ ⇑gᵢ) (h : P.IsPullbackStage P' G gᵢ) (L : AnalyticManifold.BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Tᵢ) : (AnalyticManifold.BlowUpSequence.pushforwardAux P L).pullback G ⋯ = AnalyticManifold.BlowUpSequence.pushforwardAux P' (L.pullback gᵢ hgᵢ)

The induction of the proof of [Kol07, Lemma 102] on lists, from any pair of stages with the invariant: the pull-back along G of the push-forward of L is the push-forward of the pull-back of L along gᵢ.

The statement

theorem AnalyticManifold.BlowUpSequence.pushforward_pullback {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hS.toAnalyticManifold) : (pushforward hS L).pullback g hg = pushforward ⋯ (L.pullback (⋯.restrictMap hS ⇑g ⋯ ⋯) ⋯)

The push-forward along a closed submanifold ([Kol07, Definition 30, 30.3]) commutes with pull-back along a local analytic isomorphism (the proof of [Kol07, Lemma 102]): for a closed submanifold hS : IsClosedSubmanifold ψ S s, a local analytic isomorphism g : N → M and a list of centres L on the bundled S, the pull-back along g of the push-forward of L is the push-forward, from g⁻¹(S), of the pull-back of L along the restricted local isomorphism g|_{g⁻¹S}.