The push-forward of a blow-up sequence from a closed submanifold

Given a blow-up sequence B(S) : S_r → ⋯ → S_0 = S with centres Z_i^S ⊂ S_i of a closed subscheme S ⊆ X, Kollár defines its push-forward as the sequence j_* B : X_r → ⋯ → X_0 = X whose centres Z_i^X ⊂ X_i are defined inductively as Z_i^X := (j_i)_* Z_i^S, where the j_i : S_i ↪ X_i are the natural inclusions; if B is a smooth blow-up sequence, so is j_* B [Kol07, Definition 30.3]. On manifolds the centres Z_i^S ⊆ S_i ⊆ X_i are regarded as closed submanifolds of X_i (a closed submanifold of a closed submanifold is a closed submanifold, ImageVal.lean), X_{i+1} = Bl_{Z_i^S} X_i, and S_{i+1} is the strict transform, identified with Bl_{Z_i^S} S_i by Lift.lean.

The recursion carries, at each stage, the ambient manifold X_i, the strict transform S_i ⊆ X_i (a closed submanifold of codimension s) and the identification e_i : T_i ≃ S_i of the given stage with it (PushforwardStage). One step (PushforwardStage.blowUpStep): the centre Z_i^X := j_i(e_i(Z_i^T)) is a closed submanifold of X_i of codimension c_i + s (IsClosedSubmanifold.image_diffeomorph, imageVal_isClosedSubmanifold); X_{i+1} := Bl_{Z_i^X} X_i is the blowing-up blowUp; S_{i+1} is the strict transform of S_i, a closed submanifold by StrictSubmanifold.lean; and e_{i+1} is the unique diffeomorphism over S_i between the two blowings-up of S_i along e_i(Z_i^T) (IsBlowUp.diffeomorph) — the given T_{i+1} → T_i composed with e_i (IsBlowUp.diffeomorph_comp) and the restricted blow-down S_{i+1} → S_i (isBlowUp_restrictMap). The properties of the push-forward are then read off stage by stage (a case split on the index, as for the pull-back of a succession). Not in the sources beyond Kollár's definition; the proofs are routine.

One stage of the push-forward

structure Manifold.PushforwardStage {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (s : ℕ) (Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)) : Type (max (u + 1) u_1)

The data of a stage of the push-forward [Kol07, Definition 30.3]: the ambient stage X, the strict transform S' ⊆ X as a closed submanifold of codimension s, and the identification e of the given stage Tᵢ with the bundled S'.

• space : AnalyticManifold 𝕜 E

  The ambient stage X_i.

• sub : Set self.space.carrier

  The strict transform S_i ⊆ X_i.

• isClosedSubmanifold : IsClosedSubmanifold ψ self.sub s

  S_i is a closed submanifold of X_i of codimension s.

• iso : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) Tᵢ.carrier ⋯.toAnalyticManifold.carrier ⊤

  The identification e_i : T_i ≃ S_i.

noncomputable def Manifold.PushforwardStage.incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E) Tᵢ.carrier P.space.carrier ⊤

The natural inclusion j_i ∘ e_i : T_i → X_i.

Equations

• P.incl = ⋯.inclusionMap.comp ⟨⇑P.iso, ⋯⟩

theorem Manifold.PushforwardStage.incl_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) (p : Tᵢ.carrier) : P.incl p = ↑(P.iso p)

theorem Manifold.PushforwardStage.isClosedEmbedding_incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) : Topology.IsClosedEmbedding ⇑P.incl

The inclusion is a closed embedding.

theorem Manifold.PushforwardStage.range_incl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) : Set.range ⇑P.incl = P.sub

The image of the inclusion is the strict transform.

theorem Manifold.PushforwardStage.isClosedSubmanifold_imageVal_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : IsClosedSubmanifold ψ (⋯.imageVal (⇑P.iso '' Z)) (c + s)

The centre Z_i^X := j_i(e_i(Z)) of the push-forward, a closed submanifold of X_i of codimension c + s.

theorem Manifold.PushforwardStage.imageVal_image_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) (Z : Set Tᵢ.carrier) : ⋯.imageVal (⇑P.iso '' Z) = ⇑P.incl '' Z

theorem Manifold.PushforwardStage.isBlowUp_restrictMap_imageVal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {s : ℕ} {Tᵢ : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (P : PushforwardStage ψ s Tᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑P.iso '' Z) c ⇑(⋯.restrictMap ⋯ ⇑(blowUpπ ψ ⋯) ⋯ ⋯)

The restricted blow-down S_{i+1} → S_i is a blowing-up of S_i along e_i(Z).

noncomputable def Manifold.PushforwardStage.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ᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) {π : AnalyticMap T' Tᵢ} (hπ : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c ⇑π) : PushforwardStage ψ s T'

One step of the push-forward: from the stage data at T_i and a blowing-up π : T' → T_i along Z, the stage data at T' — X_{i+1} = Bl_{Z_i^X} X_i, S_{i+1} the strict transform, e_{i+1} the unique diffeomorphism over S_i (IsBlowUp.diffeomorph).

Equations

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

theorem Manifold.PushforwardStage.restrictMap_blowUpStep_iso {𝕜 : 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ᵢ) {Z : Set Tᵢ.carrier} {c : ℕ} (hZ : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c) {π : AnalyticMap T' Tᵢ} (hπ : IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) Z c ⇑π) (p : T'.carrier) : (⋯.restrictMap ⋯ ⇑(blowUpπ ψ ⋯) ⋯ ⋯) ((P.blowUpStep hZ hπ).iso p) = P.iso (π p)

The square of the step: the restricted blow-down after e_{i+1} is e_i after π.

The recursion

theorem AnalyticManifold.FiniteSuccession.pushforwardCenterSub {𝕜 : 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) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (Manifold.IdealSheaf.support (T.center ⟨i, hi⟩)) (T.codim ⟨i, hi⟩)

The centre Z_i^T of the given sequence as a closed submanifold for the identity chart.

theorem AnalyticManifold.FiniteSuccession.pushforwardIsBlowUp {𝕜 : 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) : 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.

def AnalyticManifold.FiniteSuccession.pushforwardAux {𝕜 : 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) : Manifold.PushforwardStage ψ s (hS.toAnalyticManifold.finStages T.later ⟨i, hi⟩)

The stages of the push-forward, by recursion — X_0 = X with S_0 = S and the identity, then one blowUpStep per step of the given sequence.

Equations

• One or more equations did not get rendered due to their size.
• AnalyticManifold.FiniteSuccession.pushforwardAux hS T i.succ hi = (AnalyticManifold.FiniteSuccession.pushforwardAux hS T i ⋯).blowUpStep ⋯ ⋯

noncomputable def AnalyticManifold.FiniteSuccession.pushforwardLater {𝕜 : 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 : Fin T.length) : AnalyticManifold 𝕜 E

The later stages X_1, …, X_r of the push-forward.

Equations

• AnalyticManifold.FiniteSuccession.pushforwardLater hS T i = (AnalyticManifold.FiniteSuccession.pushforwardAux hS T (↑i + 1) ⋯).space

theorem AnalyticManifold.FiniteSuccession.pushforwardCenterOfSub {𝕜 : 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) : Manifold.IsClosedSubmanifold ψ (⋯.imageVal (⇑(pushforwardAux hS T i ⋯).iso '' Manifold.IdealSheaf.support (T.center ⟨i, hi⟩))) (T.codim ⟨i, hi⟩ + s)

The centre Z_i^X of the push-forward, as a closed submanifold of X_i.

noncomputable def AnalyticManifold.FiniteSuccession.pushforwardCenterOf {𝕜 : 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) : (pushforwardAux hS T i ⋯).space.IdealSheaf

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

Equations

• AnalyticManifold.FiniteSuccession.pushforwardCenterOf hS T i hi = ⋯.idealSheaf

noncomputable def AnalyticManifold.FiniteSuccession.pushforwardMapOf {𝕜 : 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) : AnalyticMap (pushforwardAux hS T (i + 1) ⋯).space (pushforwardAux hS T i ⋯).space

The blow-down of the push-forward at step i: the blowing-up of X_i along Z_i^X.

Equations

• AnalyticManifold.FiniteSuccession.pushforwardMapOf hS T i hi = Manifold.blowUpπ ψ ⋯

theorem AnalyticManifold.FiniteSuccession.support_pushforwardCenterOf {𝕜 : 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) : Manifold.IdealSheaf.support (pushforwardCenterOf hS T i hi) = ⋯.imageVal (⇑(pushforwardAux hS T i ⋯).iso '' Manifold.IdealSheaf.support (T.center ⟨i, hi⟩))

The support of the centre of the push-forward at step i is Z_i^X.

noncomputable def AnalyticManifold.FiniteSuccession.pushforwardCenterAux {𝕜 : 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) : (M.finStages (pushforwardLater hS T) ⟨i, ⋯⟩).IdealSheaf

The centres of the push-forward, typed on the stages finStages.

Equations

• AnalyticManifold.FiniteSuccession.pushforwardCenterAux hS T 0 hi = AnalyticManifold.FiniteSuccession.pushforwardCenterOf hS T 0 hi
• AnalyticManifold.FiniteSuccession.pushforwardCenterAux hS T i.succ hi = AnalyticManifold.FiniteSuccession.pushforwardCenterOf hS T (i + 1) hi

noncomputable def AnalyticManifold.FiniteSuccession.pushforwardMapAux {𝕜 : 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) : AnalyticMap (M.finStages (pushforwardLater hS T) ⟨i + 1, ⋯⟩) (M.finStages (pushforwardLater hS T) ⟨i, ⋯⟩)

The blow-downs of the push-forward, typed on the stages finStages.

Equations

• AnalyticManifold.FiniteSuccession.pushforwardMapAux hS T 0 hi = AnalyticManifold.FiniteSuccession.pushforwardMapOf hS T 0 hi
• AnalyticManifold.FiniteSuccession.pushforwardMapAux hS T i.succ hi = AnalyticManifold.FiniteSuccession.pushforwardMapOf hS T (i + 1) hi

theorem AnalyticManifold.FiniteSuccession.pushforwardIsMonoidalAux {𝕜 : 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) : (pushforwardMapAux hS T i hi).IsMonoidalTransformation (pushforwardCenterAux hS T i hi)

Each blow-down of the push-forward is a monoidal transformation with centre the ideal sheaf of Z_i^X (isMonoidalTransformation_blowUpπ).

The push-forward and the inclusions

noncomputable def AnalyticManifold.FiniteSuccession.pushforward {𝕜 : 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) : M.FiniteSuccession

The push-forward j_* B of a blow-up sequence of the bundled S to M [Kol07, Definition 30.3]: the blow-up sequence of M of the same length whose i-th stage is X_{i+1} = Bl_{Z_i^X} X_i and whose i-th centre is (the ideal sheaf of) Z_i^X = (j_i)_* Z_i^S, j_i : S_i ↪ X_i the natural inclusion of the strict transform, with which the given stage is identified.

Equations

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

noncomputable def AnalyticManifold.FiniteSuccession.pushforwardIncl {𝕜 : 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 : Fin (T.length + 1)) : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E) (T.stage i).carrier ((pushforward hS T).stage i).carrier ⊤

The natural inclusions j_i : S_i ↪ X_i of [Kol07, Definition 30.3]: the inclusions of the stages of the given sequence into those of the push-forward.

Equations

• AnalyticManifold.FiniteSuccession.pushforwardIncl hS T ⟨0, hi⟩ = (AnalyticManifold.FiniteSuccession.pushforwardAux hS T 0 hi).incl
• AnalyticManifold.FiniteSuccession.pushforwardIncl hS T ⟨i.succ, hi⟩ = (AnalyticManifold.FiniteSuccession.pushforwardAux hS T (i + 1) hi).incl

The properties of the push-forward

theorem AnalyticManifold.FiniteSuccession.length_pushforward {𝕜 : 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).length = T.length

theorem AnalyticManifold.FiniteSuccession.strictTransformSeqAux_pushforward_succ {𝕜 : 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 + 1 < T.length + 1) : (pushforward hS T).strictTransformSeqAux S (i + 1) hi = (pushforwardAux hS T (i + 1) hi).sub

The strict transforms of S along the push-forward are the carried S_i (stages ≥ 1; stage 0 is S by definition).

theorem AnalyticManifold.FiniteSuccession.centersIn_pushforward {𝕜 : 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).CentersIn S

The centres of the push-forward lie in the strict transforms of S, so that the restriction of [Kol07, Definition 30.2] applies to j_* B.

theorem AnalyticManifold.FiniteSuccession.isClosedEmbedding_pushforwardIncl {𝕜 : 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 : Fin (T.length + 1)) : Topology.IsClosedEmbedding ⇑(pushforwardIncl hS T i)

The inclusions S_i ↪ X_i are closed embeddings.

theorem AnalyticManifold.FiniteSuccession.range_pushforwardIncl {𝕜 : 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 : Fin (T.length + 1)) : Set.range ⇑(pushforwardIncl hS T i) = (pushforward hS T).strictTransformSeq S i

The image of the inclusion S_i ↪ X_i is the strict transform of S along the push-forward.

theorem AnalyticManifold.FiniteSuccession.pushforwardIncl_zero {𝕜 : 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) : pushforwardIncl hS T 0 = hS.inclusionMap

The inclusion at stage 0 is the inclusion S ↪ M.

theorem AnalyticManifold.FiniteSuccession.support_center_pushforward {𝕜 : 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 : Fin T.length) : Manifold.IdealSheaf.support ((pushforward hS T).center i) = ⇑(pushforwardIncl hS T i.castSucc) '' Manifold.IdealSheaf.support (T.center i)

The centre of the push-forward at step i is the image of the centre of the given sequence under the inclusion (Z_i^X := (j_i)_* Z_i^S, [Kol07, Definition 30.3]).

theorem AnalyticManifold.FiniteSuccession.pushforwardIncl_map {𝕜 : 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 : Fin T.length) (p : (T.stage i.succ).carrier) : (pushforwardIncl hS T i.castSucc) ((T.map i) p) = ((pushforward hS T).map i) ((pushforwardIncl hS T i.succ) p)

The inclusions commute with the blow-downs (the squares of Kollár's diagram).

theorem AnalyticManifold.FiniteSuccession.isClosedSubmanifold_center_pushforward {𝕜 : 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 : Fin T.length) : Manifold.IsClosedSubmanifold ψ (Manifold.IdealSheaf.support ((pushforward hS T).center i)) (T.codim i + s)

The centre Z_i^X is a closed submanifold of X_i of codimension c_i + s.

theorem AnalyticManifold.FiniteSuccession.isBlowUp_map_pushforward {𝕜 : 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 : Fin T.length) : Manifold.IsBlowUp ψ (Manifold.IdealSheaf.support ((pushforward hS T).center i)) (T.codim i + s) ⇑((pushforward hS T).map i)

Every step of the push-forward is a blowing-up of X_i along Z_i^X, of codimension c_i + s (if B is a smooth blow-up sequence, so is j_* B, [Kol07, Definition 30.3]).