The restriction of a blow-up sequence to a closed submanifold

For a blow-up sequence Π of X (a finite succession, FiniteSuccession) and a closed submanifold S ⊆ X with Z_i ⊆ S_i for all i (FiniteSuccession.CentersIn), the restriction Π|_S of [Kol07, Definition 30.2] is the blow-up sequence of the bundled S whose stages are the strict transforms S_i (strictTransformSeq, closed submanifolds of X_i by isClosedSubmanifold_strictTransformSeq), whose centres are the Z_i = Z_i ∩ S_i regarded inside S_i (IsClosedSubmanifold.preimage_val_of_subset, with the ideal sheaf IsClosedSubmanifold.idealSheaf), and whose blow-downs are the restrictions π_i|_{S_{i+1}} : S_{i+1} → S_i — blowings-up of S_i along Z_i by isBlowUp_restrictMap (Lift.lean), so that Π|_S is a succession of monoidal transformations (restrictSubmanifold). Kollár's natural embeddings S_i ↪ X_i are the inclusions restrictIncl, closed embeddings with image S_i, commuting with the blow-downs.

A succession carries one chosen chart chartAt i per step; the restriction is stated for one chart ψ of E, exchanged for chartAt i through IsClosedSubmanifold.congr_chart and IsBlowUp.congr_chart. The stages are typed on the stages finStages of a succession by a case split on the index.

def Manifold.IsClosedSubmanifold.inclusionMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E) hS.toAnalyticManifold.carrier M ⊤

The inclusion of a closed submanifold as a bundled analytic map (between the model 𝕜^{n-s} of the submanifold and the model E of M); the natural embeddings S_i ↪ X_i of [Kol07, Definition 30.2] are of this form.

Equations

• hS.inclusionMap = ⟨Subtype.val, ⋯⟩

theorem Manifold.IsClosedSubmanifold.inclusionMap_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) (p : hS.toAnalyticManifold.carrier) : hS.inclusionMap p = ↑p

The pieces at the level of the recursion

theorem AnalyticManifold.FiniteSuccession.restrictCenterSub {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : ℕ) (hi : i < S.length) : Manifold.IsClosedSubmanifold ψ (Manifold.IdealSheaf.support (S.center ⟨i, hi⟩)) (S.codim ⟨i, hi⟩)

The centre Z_i as a closed submanifold of X_i for the chart ψ.

theorem AnalyticManifold.FiniteSuccession.restrictCenterSub' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⋯.preimageVal (Manifold.IdealSheaf.support (S.center ⟨i, hi⟩))) (S.codim ⟨i, hi⟩ - s)

Kollár's Z_i ∩ S_i: the centre as a closed submanifold of the bundled S_i, of codimension c_i − s.

theorem AnalyticManifold.FiniteSuccession.restrictMapsTo {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (i : ℕ) (hi : i < S.length) (x : (M.finStages S.later ⟨i + 1, ⋯⟩).carrier) : x ∈ S.strictTransformSeqAux H (i + 1) ⋯ → (S.map ⟨i, hi⟩) x ∈ S.strictTransformSeqAux H i ⋯

The blow-down carries S_{i+1} into S_i.

noncomputable def AnalyticManifold.FiniteSuccession.restrictLater {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)

The later stages S_1, …, S_r of the restriction.

Equations

• S.restrictLater hH hc i = ⋯.toAnalyticManifold

noncomputable def AnalyticManifold.FiniteSuccession.restrictCenterOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : ⋯.toAnalyticManifold.IdealSheaf

The centre of the restriction at step i: the ideal sheaf of Z_i ∩ S_i in S_i.

Equations

• S.restrictCenterOf hH hc i hi = ⋯.idealSheaf

def AnalyticManifold.FiniteSuccession.restrictMapOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : AnalyticMap ⋯.toAnalyticManifold ⋯.toAnalyticManifold

The blow-down of the restriction at step i: π_i|_{S_{i+1}} : S_{i+1} → S_i.

Equations

• S.restrictMapOf hH hc i hi = ⋯.restrictMap ⋯ ⇑(S.map ⟨i, hi⟩) ⋯ ⋯

theorem AnalyticManifold.FiniteSuccession.isBlowUp_restrictMapOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : Manifold.IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⋯.preimageVal (Manifold.IdealSheaf.support (S.center ⟨i, hi⟩))) (S.codim ⟨i, hi⟩ - s) ⇑(S.restrictMapOf hH hc i hi)

Each blow-down of the restriction is a blowing-up of S_i along Z_i ∩ S_i (isBlowUp_restrictMap, with the succession's chart exchanged for ψ).

theorem AnalyticManifold.FiniteSuccession.restrictIsMonoidalOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : (S.restrictMapOf hH hc i hi).IsMonoidalTransformation (S.restrictCenterOf hH hc i hi)

Each blow-down of the restriction is a monoidal transformation with centre the ideal sheaf of Z_i ∩ S_i (IsMonoidalTransformation).

The pieces typed on the stages of a succession

noncomputable def AnalyticManifold.FiniteSuccession.restrictCenterAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : (hH.toAnalyticManifold.finStages (S.restrictLater hH hc) ⟨i, ⋯⟩).IdealSheaf

The centres of the restriction, typed on the stages finStages (a case split on the index makes the stage reduce to the recursion's).

Equations

• S.restrictCenterAux hH hc 0 hi = S.restrictCenterOf hH hc 0 hi
• S.restrictCenterAux hH hc i.succ hi = S.restrictCenterOf hH hc (i + 1) hi

def AnalyticManifold.FiniteSuccession.restrictMapAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : AnalyticMap (hH.toAnalyticManifold.finStages (S.restrictLater hH hc) ⟨i + 1, ⋯⟩) (hH.toAnalyticManifold.finStages (S.restrictLater hH hc) ⟨i, ⋯⟩)

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

Equations

• S.restrictMapAux hH hc 0 hi = S.restrictMapOf hH hc 0 hi
• S.restrictMapAux hH hc i.succ hi = S.restrictMapOf hH hc (i + 1) hi

theorem AnalyticManifold.FiniteSuccession.restrictIsMonoidalAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : ℕ) (hi : i < S.length) : (S.restrictMapAux hH hc i hi).IsMonoidalTransformation (S.restrictCenterAux hH hc i hi)

Each blow-down of the restriction is a monoidal transformation, typed on the stages.

The restriction and the inclusions

noncomputable def AnalyticManifold.FiniteSuccession.restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) : hH.toAnalyticManifold.FiniteSuccession

The restriction Π|_S of a blow-up sequence to a closed submanifold S with Z_i ⊆ S_i for all i [Kol07, Definition 30.2]: the blow-up sequence of the bundled S of the same length whose i-th stage is the strict transform S_i, whose i-th centre is (the ideal sheaf of) Z_i ∩ S_i = Z_i, and whose i-th blow-down is π_i|_{S_{i+1}}.

Equations

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

def AnalyticManifold.FiniteSuccession.restrictIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin (S.length + 1)) : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 E) ((S.restrictSubmanifold hH hc).stage i).carrier (S.stage i).carrier ⊤

The natural embeddings S_i ↪ X_i of [Kol07, Definition 30.2]: the inclusions of the stages of the restriction into those of Π.

Equations

• S.restrictIncl hH hc ⟨0, hi⟩ = ⋯.inclusionMap
• S.restrictIncl hH hc ⟨i.succ, hi⟩ = ⋯.inclusionMap

The properties of the restriction

theorem AnalyticManifold.FiniteSuccession.length_restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) : (S.restrictSubmanifold hH hc).length = S.length

theorem AnalyticManifold.FiniteSuccession.stage_restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin (S.length + 1)) : (S.restrictSubmanifold hH hc).stage i = ⋯.toAnalyticManifold

The stages of Π|_S are the strict transforms S_i, as bundled closed submanifolds.

theorem AnalyticManifold.FiniteSuccession.isClosedEmbedding_restrictIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin (S.length + 1)) : Topology.IsClosedEmbedding ⇑(S.restrictIncl hH hc i)

The inclusions S_i ↪ X_i are closed embeddings.

theorem AnalyticManifold.FiniteSuccession.range_restrictIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin (S.length + 1)) : Set.range ⇑(S.restrictIncl hH hc i) = S.strictTransformSeq H i

The image of the inclusion S_i ↪ X_i is the strict transform S_i.

theorem AnalyticManifold.FiniteSuccession.support_center_restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) : Manifold.IdealSheaf.support ((S.restrictSubmanifold hH hc).center i) = ⇑(S.restrictIncl hH hc i.castSucc) ⁻¹' Manifold.IdealSheaf.support (S.center i)

The centre of Π|_S at step i is Z_i ∩ S_i, read through the inclusion.

theorem AnalyticManifold.FiniteSuccession.restrictIncl_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) (p : ((S.restrictSubmanifold hH hc).stage i.succ).carrier) : (S.restrictIncl hH hc i.castSucc) (((S.restrictSubmanifold hH hc).map i) p) = (S.map i) ((S.restrictIncl hH hc i.succ) p)

The inclusions commute with the blow-downs: π_i^S is the restriction of π_i.

theorem AnalyticManifold.FiniteSuccession.isBlowUp_map_restrictSubmanifold {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {H : Set M.carrier} {s : ℕ} (hH : Manifold.IsClosedSubmanifold ψ H s) (hc : S.CentersIn H) (i : Fin S.length) : Manifold.IsBlowUp (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (⇑(S.restrictIncl hH hc i.castSucc) ⁻¹' Manifold.IdealSheaf.support (S.center i)) (S.codim i - s) ⇑((S.restrictSubmanifold hH hc).map i)

Each blow-down of Π|_S is a blowing-up of S_i along Z_i ∩ S_i, of codimension c_i − s, in the induced charts.