The push-forward of a list of centres is the push-forward of its succession

The push-forward of a blow-up sequence of a closed submanifold S ⊆ M to M [Kol07, Definition 30, 30.3] exists in two forms: FiniteSuccession.pushforward on finite successions, recursing on the stage index from the start (M, S, e_0 = id), and BlowUpSequence.pushforward on lists of centres, recursing on the list from any PushforwardStage. The commutation of the order-reduction functor with closed embeddings ([Kol07, 34.3]; [Kol07, Theorem 103, (3)]) is stated on the former, the push-forward being the correspondence of [Kol07, Corollary 85], while a blow-up sequence functor's value is a list. This file identifies the two:

• FiniteSuccession.ext_of: two successions with equal lengths and stages and heterogeneously equal centres and maps are equal;
• PushforwardStage.pushforwardOfStage P T: the succession recursion from an arbitrary start stage P (FiniteSuccession.pushforward_eq_pushforwardOfStage is the identification at the canonical start), and the peeling lemma pushforwardOfStage_cons: on cons hZ R with a nonempty centre Z, the push-forward starts with (j_0)_* Z and continues from the next stage; the chosen codimension of the first blow-up of the succession, a classical choice from isMonoidal, equals the codimension c of hZ by IsClosedSubmanifold.codim_eq_of_nonempty;
• BlowUpSequence.toSuccession_pushforward: for a list L with no empty centre (the output convention of every blow-up sequence functor, [Kol07, 32]), (L.pushforward hS).toSuccession = L.toSuccession.pushforward hS. The hypothesis is needed: for an empty centre every codimension is legitimate (isClosedSubmanifold_empty'), the chosen codimension of the succession is free, and the two push-forwards may blow up M along "the empty set of codimension c'" for different c'.

The identification is used where a functor's value, a list, is compared with the push-forward of a succession, in the descent of the order-reduction functors to a hypersurface of maximal contact.

theorem Manifold.heq_pi_of_forall {α : Sort w} {β₁ β₂ : α → Sort v} (e : β₁ = β₂) (f₁ : (a : α) → β₁ a) (f₂ : (a : α) → β₂ a) (h : ∀ (a : α), f₁ a ≍ f₂ a) : f₁ ≍ f₂

Heterogeneous equality of dependent functions over propositionally equal families, from the pointwise heterogeneous equalities.

theorem AnalyticManifold.FiniteSuccession.ext_of {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {S T : M.FiniteSuccession} (hl : S.length = T.length) (hlater : ∀ (i : Fin S.length), S.later i = T.later (Fin.cast hl i)) (hc : S.center ≍ T.center) (hm : S.map ≍ T.map) : S = T

Extensionality of finite successions: two successions of the same length whose stages agree and whose centres and blow-downs are heterogeneously equal are equal (isMonoidal is a proof).

theorem AnalyticManifold.FiniteSuccession.centerSub {𝕜 : Type} [RCLike 𝕜] {n s : ℕ} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (Manifold.IdealSheaf.support (T.center ⟨i, hi⟩)) (T.codim ⟨i, hi⟩)

The centre Z_i of a succession on a manifold modelled on 𝕜^{n-s}, as a closed submanifold for the identity chart (pushforwardCenterSub from any base).

theorem AnalyticManifold.FiniteSuccession.isBlowUpSub {𝕜 : Type} [RCLike 𝕜] {n s : ℕ} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : Manifold.IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (Manifold.IdealSheaf.support (T.center ⟨i, hi⟩)) (T.codim ⟨i, hi⟩) ⇑(T.map ⟨i, hi⟩)

The blow-down T_{i+1} → T_i as a blowing-up for the identity chart (pushforwardIsBlowUp from any base).

The recursion from an arbitrary start stage

def Manifold.PushforwardStage.stageAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length + 1) : PushforwardStage ψ s (T₀.finStages T.later ⟨i, hi⟩)

The stages of the push-forward of T started at P (pushforwardAux with P in place of (M, S, id)).

Equations

• P.stageAux T 0 x_2 = P
• P.stageAux T i.succ hi = (P.stageAux T i ⋯).blowUpStep ⋯ ⋯

noncomputable def Manifold.PushforwardStage.laterAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : Fin T.length) : AnalyticManifold 𝕜 E

The later stages of the push-forward started at P.

Equations

• P.laterAux T i = (P.stageAux T (↑i + 1) ⋯).space

theorem Manifold.PushforwardStage.centerOfSub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : IsClosedSubmanifold ψ (⋯.imageVal (⇑(P.stageAux T i ⋯).iso '' IdealSheaf.support (T.center ⟨i, hi⟩))) (T.codim ⟨i, hi⟩ + s)

The centre of the push-forward at step i, as a closed submanifold.

noncomputable def Manifold.PushforwardStage.centerOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : (P.stageAux T i ⋯).space.IdealSheaf

The centre of the push-forward at step i: the ideal sheaf of Z_i^X.

Equations

• P.centerOf T i hi = ⋯.idealSheaf

noncomputable def Manifold.PushforwardStage.mapOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : AnalyticMap (P.stageAux T (i + 1) ⋯).space (P.stageAux T i ⋯).space

The blow-down of the push-forward at step i.

Equations

• P.mapOf T i hi = Manifold.blowUpπ ψ ⋯

noncomputable def Manifold.PushforwardStage.centerAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : (P.space.finStages (P.laterAux T) ⟨i, ⋯⟩).IdealSheaf

The centres, typed on finStages.

Equations

• P.centerAux T 0 hi = P.centerOf T 0 hi
• P.centerAux T i.succ hi = P.centerOf T (i + 1) hi

noncomputable def Manifold.PushforwardStage.mapAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : AnalyticMap (P.space.finStages (P.laterAux T) ⟨i + 1, ⋯⟩) (P.space.finStages (P.laterAux T) ⟨i, ⋯⟩)

The blow-downs, typed on finStages.

Equations

• P.mapAux T 0 hi = P.mapOf T 0 hi
• P.mapAux T i.succ hi = P.mapOf T (i + 1) hi

theorem Manifold.PushforwardStage.isMonoidalAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) (i : ℕ) (hi : i < T.length) : (P.mapAux T i hi).IsMonoidalTransformation (P.centerAux T i hi)

Each blow-down is the monoidal transformation with centre the ideal sheaf of Z_i^X.

noncomputable def Manifold.PushforwardStage.pushforwardOfStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) (T : T₀.FiniteSuccession) : P.space.FiniteSuccession

[Kol07, Definition 30, 30.3] from an arbitrary start stage P: the push-forward of the succession T on T₀ to P.space (FiniteSuccession.pushforward is the instance at the canonical start, FiniteSuccession.pushforward_eq_pushforwardOfStage).

Equations

• P.pushforwardOfStage T = { length := T.length, later := P.laterAux T, center := fun (i : Fin T.length) => P.centerAux T ↑i ⋯, map := fun (i : Fin T.length) => P.mapAux T ↑i ⋯, isMonoidal := ⋯ }

Congruences

theorem Manifold.PushforwardStage.blowUpStep_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) {Z₁ Z₂ : Set T₀.carrier} {c₁ c₂ : ℕ} (eZ : Z₁ = Z₂) (ec : c₁ = c₂) (h₁ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₁ c₁) (h₂ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₂ c₂) {T' : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {π : AnalyticMap T' T₀} (hπ₁ : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₁ c₁ ⇑π) (hπ₂ : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₂ c₂ ⇑π) : P.blowUpStep h₁ hπ₁ = P.blowUpStep h₂ hπ₂

blowUpStep depends on the centre and its codimension only up to propositional equality.

theorem Manifold.PushforwardStage.idealSheaf_imageVal_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) {Z₁ Z₂ : Set T₀.carrier} {c₁ c₂ : ℕ} (eZ : Z₁ = Z₂) (ec : c₁ = c₂) (h₁ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₁ c₁) (h₂ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₂ c₂) : ⋯.idealSheaf = ⋯.idealSheaf

The pushed-forward centre depends on the centre and its codimension only up to propositional equality.

theorem Manifold.PushforwardStage.heq_blowUpπ_imageVal_congr {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) {Z₁ Z₂ : Set T₀.carrier} {c₁ c₂ : ℕ} (eZ : Z₁ = Z₂) (ec : c₁ = c₂) (h₁ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₁ c₁) (h₂ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z₂ c₂) : blowUpπ ψ ⋯ ≍ blowUpπ ψ ⋯

The blow-down along the pushed-forward centre, up to propositional equality of the centre and its codimension.

theorem Manifold.PushforwardStage.heq_idealSheaf_imageVal_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P₁ P₂ : PushforwardStage ψ s X} (e : P₁ = P₂) {Z : Set X.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : ⋯.idealSheaf ≍ ⋯.idealSheaf

The pushed-forward centre, along an equality of stages.

theorem Manifold.PushforwardStage.heq_blowUpπ_imageVal_of_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {X : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {P₁ P₂ : PushforwardStage ψ s X} (e : P₁ = P₂) {Z : Set X.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : blowUpπ ψ ⋯ ≍ blowUpπ ψ ⋯

The blow-down along the pushed-forward centre, along an equality of stages.

The push-forward of nil and of cons

theorem Manifold.PushforwardStage.pushforwardOfStage_nil {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s T₀) : P.pushforwardOfStage (AnalyticManifold.FiniteSuccession.nil T₀) = AnalyticManifold.FiniteSuccession.nil P.space

The push-forward of the empty succession is the empty succession on P.space.

theorem Manifold.PushforwardStage.support_center_cons_zero {𝕜 : Type} [RCLike 𝕜] {n s : ℕ} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {Z : Set T₀.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (R : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ).FiniteSuccession) : IdealSheaf.support ((AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R).center 0) = Z

The support of the first centre of cons hZ R is Z.

theorem Manifold.PushforwardStage.codim_cons_zero {𝕜 : Type} [RCLike 𝕜] {n s : ℕ} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {Z : Set T₀.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (R : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ).FiniteSuccession) (hne : Z.Nonempty) : (AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R).codim 0 = c

[Kol07, 32] removing the obstruction: for a nonempty first centre, the succession's chosen codimension of the first blow-up of cons hZ R is the codimension c of hZ (IsClosedSubmanifold.codim_eq_of_nonempty, across the chosen chart and the identity chart).

theorem Manifold.PushforwardStage.stageAux_cons_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {Z : Set T₀.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (R : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ).FiniteSuccession) (P : PushforwardStage ψ s T₀) (hne : Z.Nonempty) (i : ℕ) (hi : i + 1 < (AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R).length + 1) : P.stageAux (AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R) (i + 1) hi = (P.blowUpStep hZ ⋯).stageAux R i ⋯

The stages of the push-forward of cons hZ R after the first are those of the push-forward of R started at the first blow-up step (the peeling of the recursion; the first step's data are identified through codim_cons_zero).

theorem Manifold.PushforwardStage.heq_mapOf_cons_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {Z : Set T₀.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (R : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ).FiniteSuccession) (P : PushforwardStage ψ s T₀) (hne : Z.Nonempty) (i : ℕ) (hi : i + 1 < (AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R).length) : P.mapOf (AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R) (i + 1) hi ≍ (P.blowUpStep hZ ⋯).mapOf R i ⋯

The blow-downs of the push-forward of cons hZ R after the first are those of the push-forward of R started at the first blow-up step (typed on the stages, stageAux_cons_succ).

theorem Manifold.PushforwardStage.pushforwardOfStage_cons {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} {Z : Set T₀.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) (R : (blowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ).FiniteSuccession) (P : PushforwardStage ψ s T₀) (hne : Z.Nonempty) : P.pushforwardOfStage (AnalyticManifold.FiniteSuccession.cons (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hZ R) = AnalyticManifold.FiniteSuccession.cons ψ ⋯ ((P.blowUpStep hZ ⋯).pushforwardOfStage R)

The peeling lemma: for a nonempty first centre Z, the push-forward of cons hZ R started at P is cons of the pushed-forward centre (j_0)_* Z and the push-forward of R started at the first blow-up step.

theorem AnalyticManifold.FiniteSuccession.pushforwardAux_eq_stageAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) (i : ℕ) (hi : i < T.length + 1) : pushforwardAux hS T i hi = { space := M, sub := S, isClosedSubmanifold := hS, iso := Diffeomorph.refl (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) hS.toAnalyticManifold.carrier ⊤ }.stageAux T i hi

The stages are the general recursion's at the canonical start (M, S, id).

theorem AnalyticManifold.FiniteSuccession.pushforward_eq_pushforwardOfStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} {s : ℕ} (hS : Manifold.IsClosedSubmanifold ψ S s) (T : hS.toAnalyticManifold.FiniteSuccession) : pushforward hS T = { space := M, sub := S, isClosedSubmanifold := hS, iso := Diffeomorph.refl (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) hS.toAnalyticManifold.carrier ⊤ }.pushforwardOfStage T

The push-forward is the general recursion's at the canonical start (M, S, id).

theorem AnalyticManifold.BlowUpSequence.toSuccession_pushforwardAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {T₀ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : Manifold.PushforwardStage ψ s T₀) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) T₀) : L.NoEmptyCenters → (pushforwardAux P L).toSuccession = P.pushforwardOfStage L.toSuccession

The list push-forward from any start stage, as a succession, is the general succession push-forward of the list's succession — for a list with no empty centre.

theorem AnalyticManifold.BlowUpSequence.toSuccession_pushforward {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n s : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S s) (L : BlowUpSequence (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) hS.toAnalyticManifold) (hL : L.NoEmptyCenters) : (pushforward hS L).toSuccession = FiniteSuccession.pushforward hS L.toSuccession

The push-forward of lists agrees with the push-forward of successions: for a closed submanifold hS : IsClosedSubmanifold ψ S s and a list of centres L on the bundled S with no empty centre ([Kol07, 32]), the succession of the list push-forward is the push-forward of the list's succession. The hypothesis is load-bearing: at an empty centre the chosen codimension is free (isClosedSubmanifold_empty'), and the two push-forwards need not agree.