Strict transforms of a subset along a blow-up sequence; centres inside a submanifold

Kollár restricts a blow-up sequence Π : X_r → ⋯ → X_0 = X with centres Z_i to a closed subscheme S ⊆ X [Kol07, Definition 30.2]: the restricted sequence runs through the subschemes S_{i+1} := Bl_{Z_i ∩ S_i} S_i, naturally identified with the birational transform of S_i in X_{i+1}. On analytic manifolds the S_i are the iterated strict transforms S_0 = S, S_{i+1} = closure (π_i⁻¹(S_i ∖ Z_i)) (strictTransformSet). Since the restriction of a smooth blow-up sequence need not be a smooth blow-up sequence [Kol07, Definition 30.2], and a finite succession (FiniteSuccession) has smooth centres, the restricted succession is formed under the hypothesis that every centre lies in the strict transform of S at its stage, so that the restricted centres Z_i ∩ S_i = Z_i are smooth. This module provides

• FiniteSuccession.strictTransformSeq S H i: the strict transforms H_i ⊆ X_i of a subset H ⊆ M along the succession, by recursion on i (H_0 = H, H_{i+1} = strictTransformSet (S.map i) (S.center i).support H_i);
• FiniteSuccession.CentersIn S H: every centre Z_i lies in the strict transform H_i.

These are the stages and the hypothesis of the restricted succession constructed in StrictSubmanifold.lean and Restrict.lean.

def AnalyticManifold.FiniteSuccession.strictTransformSeqAux {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) (i : ℕ) (h : i < S.length + 1) : Set (M.finStages S.later ⟨i, h⟩).carrier

The strict transforms H_i ⊆ X_i of a subset H ⊆ M along the succession, indexed by a natural number together with a proof that it is a stage: H_0 = H, H_{i+1} = closure (π_i⁻¹(H_i ∖ Z_i)) (strictTransformSet); Kollár's S_{i+1}, identified with the birational transform of S_i [Kol07, Definition 30.2].

Equations

• S.strictTransformSeqAux H 0 x_2 = H
• S.strictTransformSeqAux H i.succ h = Manifold.strictTransformSet (⇑(S.map ⟨i, ⋯⟩)) (Manifold.IdealSheaf.support (S.center ⟨i, ⋯⟩)) (S.strictTransformSeqAux H i ⋯)

def AnalyticManifold.FiniteSuccession.strictTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) (i : Fin (S.length + 1)) : Set (S.stage i).carrier

The strict transform H_i ⊆ X_i of H ⊆ M at the stage i of the succession, Kollár's S_i [Kol07, Definition 30.2].

Equations

• S.strictTransformSeq H i = S.strictTransformSeqAux H ↑i ⋯

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) : S.strictTransformSeq H 0 = H

theorem AnalyticManifold.FiniteSuccession.strictTransformSeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) (i : Fin S.length) : S.strictTransformSeq H i.succ = Manifold.strictTransformSet (⇑(S.map i)) (Manifold.IdealSheaf.support (S.center i)) (S.strictTransformSeq H i.castSucc)

def AnalyticManifold.FiniteSuccession.CentersIn {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (H : Set M.carrier) : Prop

Every centre of the succession lies in the strict transform of H at its stage: the hypothesis under which the restriction of the succession to H [Kol07, Definition 30.2] has the smooth centres Z_i ∩ H_i = Z_i.

Equations

• S.CentersIn H = ∀ (i : Fin S.length), Manifold.IdealSheaf.support (S.center i) ⊆ S.strictTransformSeq H i.castSucc