Finite successions of monoidal transformations #
Włodarczyk's finite sequence of blow-ups with smooth centres Wlo09, Theorem 2.0.3 (1);
Theorem 3.6.1 — in Hironaka's words [Hir64, p. 155] a succession of monoidal transformations
indexed by the finite well-ordered set Λ = {0 < 1 < ⋯ < r}. A FiniteSuccession M has stages
U_0 = M, U_1, …, U_r (finStages), centres C_i ⊆ U_i given by ideal sheaves, and maps
σ_{i+1} : U_{i+1} → U_i, each the monoidal transformation of U_i with centre C_i
(AnalyticMap.IsMonoidalTransformation: the centre is a closed submanifold, Włodarczyk's "smooth
centers"). Local finiteness is automatic for a finite Λ; empty centres are admitted (a monoidal
transformation with empty centre is an isomorphism).
stage,stageMap(the compositeσ^i : U_i → M),lastandcomposite(σ^r), by recursion on the stage;weakTransformSeq(Hironaka's weak transformsJ_i) andboundarySeq(his boundariesE_i), by recursion from the one-stepIdealSheaf.weakTransformandIdealSheaf.reducedTransform(clauses (ii) and (iii) of [Hir64, Main Theorem II'(N), p. 156]);- the data witnessing that each step is a monoidal transformation, extracted by choice:
dimAt,chartAt,codim, with the centre a closed submanifold (isClosedSubmanifold_center) and the map a blowing-up along it (isBlowUp_map). strictTransformSubspaceSeq(the strict transformsY_iof a closed subspaceY, Kollár's restricted sequence [Kol07, Definition 30.2]), by recursion from the one-stepstrictTransformSubspaceat those witnesses.
The analytic main theorems assert, for the succession over each compact set of a compatible
family (ExtensionCompatibleFamily), Hironaka's clauses on the centres, the weak transforms and the
boundaries.
The stages of a finite succession from the data of the later stages: U_0 = M,
U_{i+1} = later i.
Instances For
Finite successions of monoidal transformations #
Włodarczyk's finite sequence of blow-ups with smooth centres Wlo09, Theorem 2.0.3 (1);
Theorem 3.6.1: Hironaka's succession of monoidal transformations {f_λ : X_{λ+1} → X_λ}_{λ ∈ Λ}
[Hir64, p. 155] for the finite well-ordered set Λ = {0 < 1 < ⋯ < r} — stages U_i with
U_0 = M, centres C_i ⊆ U_i and maps σ_{i+1} : U_{i+1} → U_i for 0 ≤ i < r, each the
monoidal transformation of U_i with centre C_i. The empty succession (length = 0) is
Λ = {0}. Empty centres are admitted (a monoidal transformation with empty centre is an
isomorphism: Włodarczyk's "isomorphisms" in [Wlo09, Definitions 3.2.5, 3.2.6]).
- length : ℕ
The length
r: the number of blow-ups. - later : Fin self.length → AnalyticManifold 𝕜 E
The later stages
U_1, …, U_r. The centre
C_i ⊆ U_iof the blow-upσ_{i+1},0 ≤ i < r.- map (i : Fin self.length) : AnalyticMap (M.finStages self.later i.succ) (M.finStages self.later i.castSucc)
The blow-up
σ_{i+1} : U_{i+1} → U_i. - isMonoidal (i : Fin self.length) : (self.map i).IsMonoidalTransformation (self.center i)
σ_{i+1}is the monoidal transformation ofU_iwith centreC_i(the centre is a closed submanifold: Włodarczyk's "smooth centers").
Instances For
The stage U_i, 0 ≤ i ≤ r, with U_0 = M.
Instances For
The composite σ^i = σ_1 ∘ ⋯ ∘ σ_i : U_i → U_0 = M (Włodarczyk's σ^i,
[Wlo09, Theorem 2.0.3 (2)]; Hironaka's canonical morphism X_λ → X_0 [Hir64, p. 155]), by
recursion on i.
Equations
- S.stageMapAux 0 x_2 = ContMDiffMap.id
- S.stageMapAux i.succ h = ContMDiffMap.comp (S.stageMapAux i ⋯) (S.map ⟨i, ⋯⟩)
Instances For
The composite σ^i : U_i → M.
Equations
- S.stageMap i = S.stageMapAux ↑i ⋯
Instances For
The end result U_r.
Instances For
The composite σ^r = σ_1 ∘ ⋯ ∘ σ_r : U_r → M of the whole succession (Włodarczyk's σ^r;
Hironaka's canonical modification X_γ → X [Hir64, p. 155]).
Instances For
The weak transforms J_i along the succession: J_0 = J, J_{i+1} the weak transform of
J_i by σ_{i+1} (clause (ii) of [Hir64, Main Theorem II'(N), p. 156]), by recursion on i.
Equations
- S.weakTransformSeqAux J 0 x_2 = J
- S.weakTransformSeqAux J i.succ h = AnalyticManifold.IdealSheaf.weakTransform (S.map ⟨i, ⋯⟩) (S.weakTransformSeqAux J i ⋯) (S.center ⟨i, ⋯⟩)
Instances For
The weak transform J_i on the stage U_i.
Equations
- S.weakTransformSeq J i = S.weakTransformSeqAux J ↑i ⋯
Instances For
The boundaries E_i along the succession: E_0 = E,
E_{i+1} = red(σ_{i+1}⁻¹(E_i) ∪ σ_{i+1}⁻¹(C_i)) (clause (iii) of Hir64, Main Theorem II'(N),
p. 156), by recursion on i.
Equations
- S.boundarySeqAux E₀ 0 x_2 = E₀
- S.boundarySeqAux E₀ i.succ h = AnalyticManifold.IdealSheaf.reducedTransform (S.map ⟨i, ⋯⟩) (S.boundarySeqAux E₀ i ⋯) (S.center ⟨i, ⋯⟩)
Instances For
The boundary E_i on the stage U_i.
Equations
- S.boundarySeq E₀ i = S.boundarySeqAux E₀ ↑i ⋯
Instances For
The witnesses of isMonoidal: every step is a blowing-up with a specified centre #
The dimension n of the model space in the chart data of the i-th blow-up (a witness of
isMonoidal i, chosen).
Equations
- S.dimAt i = Exists.choose ⋯
Instances For
The chart E ≃ 𝕜ⁿ of the i-th blow-up (chosen).
Instances For
The codimension c_i of the centre Z_i (chosen).
Instances For
The centre Z_i ⊂ X_i of the i-th blow-up, the cosupport of the ideal sheaf C_i, is a
closed submanifold.
π_i is a blow-up with centre Z_i [Kol07, Definition 29], in the sense of
[BM88, Definition 4.1].
The strict transforms of a closed subspace #
The ideal-theoretic strict transforms Y_i ⊆ U_i of the closed subspace J ⊆ 𝒪_M along
the succession, indexed by a natural number together with a proof that it is a stage: Y_0 = J,
Y_{i+1} the strict transform (strictTransformSubspace) of Y_i under the i-th blow-up at
its witnesses.
Equations
- S.strictTransformSubspaceSeqAux J 0 x_2 = J
- S.strictTransformSubspaceSeqAux J i.succ h = Manifold.strictTransformSubspace ⋯ ⋯ (S.strictTransformSubspaceSeqAux J i ⋯)
Instances For
The strict transform Y_i ⊆ U_i of the closed subspace J at stage i of the
succession ([Kol07, Definition 30.2]; the chain Ỹ_Z of [Wlo09, §4, (3)⇒(4)]): Y_0 = J and
Y_{i+1} the strict transform of Y_i under the i-th blow-up, the saturation of its total
transform by the exceptional divisor ([BM97, §3, Proposition 3.13]).
Equations
- S.strictTransformSubspaceSeq J i = S.strictTransformSubspaceSeqAux J ↑i ⋯