Analytic blow-up sequences: witnesses and marked transforms

A blow-up sequence of length r starting with X is a chain of morphisms Π : X_r → X_{r−1} → ⋯ → X_1 → X_0 = X in which each π_i : X_{i+1} → X_i is a blow-up with centre Z_i ⊂ X_i and exceptional divisor F_{i+1} ⊂ X_{i+1}; trivial and empty blow-ups are allowed [Kol07, Definition 29]. On analytic manifolds, with closed submanifolds as centres, this notion is AnalyticManifold.FiniteSuccession M, the finite sequence of monoidal transformations in which the analytic main theorems are stated [Wlo09, Theorem 2.0.3]; this module adds no second notion of a sequence but equips that structure with the data Kollár's definition reads off a sequence (his constructors FiniteSuccession.nil and FiniteSuccession.cons are in Hironaka/Manifold/FiniteSuccession/Cons.lean). It provides:

• the last witness of isMonoidal i: besides the chosen chart data dimAt, chartAt, codim, the closed submanifold Z_i (isClosedSubmanifold_center) and the blowing-up (isBlowUp_map), the centre C_i is the ideal sheaf of Z_i (isIdealSheafOf_center), so that every step of an arbitrary sequence is a blow-up with centre Z_i;
• trivial and empty blow-ups [Kol07, Warning 20]: IsEmptyAt (Z_i = ∅, the unit ideal sheaf), IsTrivialAt (Z_i a closed submanifold of codimension one, a Cartier divisor), NoEmptyCenters (the empty blow-up convention [Kol07, 32]), and the exceptional divisor exceptionalAt S i = π_i⁻¹(Z_i);
• the marked transforms (X_{i+1}, I_{i+1}, m) := (B_{Z_i} X_i, (π_i)^{-1}_*(I_i, m)) along the sequence [Kol07, Definition 66 (1′)], by recursion on the sequence through MarkedIdealSheaf.birationalTransform at the witnesses of isMonoidal i (markedTransformSeq). The iterated birational transform is defined along the sequence, never as a function of the composite alone, as Kollár warns after his Definition 48. The recursions weakTransformSeq and boundarySeq (the weak transforms and the accumulated exceptional divisors) are those of FiniteSuccession itself.

The marked transforms are the ideals whose orders the order-reduction and resolution algorithms control.

The witnesses of isMonoidal: the centre is the ideal sheaf of a closed submanifold

theorem AnalyticManifold.FiniteSuccession.isIdealSheafOf_center {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : Manifold.IsIdealSheafOf (S.chartAt i) (Manifold.IdealSheaf.support (S.center i)) (S.codim i) (S.center i)

The centre C_i is the ideal sheaf of the closed submanifold Z_i.

Trivial and empty blow-ups, the exceptional divisor

def AnalyticManifold.FiniteSuccession.IsEmptyAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : Prop

The i-th blow-up is empty if its centre is empty, i.e. the unit ideal sheaf [Kol07, Warning 20].

Equations

• S.IsEmptyAt i = (S.center i = ⊤)

def AnalyticManifold.FiniteSuccession.IsTrivialAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (i : Fin S.length) : Prop

The i-th blow-up is trivial if its centre is a Cartier divisor [Kol07, Warning 20]: on a manifold, a closed submanifold of codimension one, with its ideal sheaf as the centre.

Equations

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

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

No blow-up of the sequence is empty (the empty blow-up convention [Kol07, 32]).

Equations

• S.NoEmptyCenters = ∀ (i : Fin S.length), ¬S.IsEmptyAt i

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

The exceptional divisor F_{i+1} = π_i⁻¹(Z_i) ⊂ X_{i+1} of the i-th blow-up [Kol07, Definition 29], as a subset of the stage X_{i+1}.

Equations

• S.exceptionalAt i = ⇑(S.map i) ⁻¹' Manifold.IdealSheaf.support (S.center i)

The marked transforms along the sequence

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

The i-th marked transform (π_{i-1})^{-1}_* ⋯ (π_0)^{-1}_*(J, m) on the stage X_i, by recursion on i [Kol07, Definition 66 (1′)]: each step is MarkedIdealSheaf.birationalTransform at the witnesses chosen from isMonoidal.

Equations

• S.markedTransformSeqAux J m 0 x_2 = J
• S.markedTransformSeqAux J m i.succ h = (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := S.markedTransformSeqAux J m i ⋯, m := m }).I

noncomputable def AnalyticManifold.FiniteSuccession.markedTransformSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (m : ℕ) (i : Fin (S.length + 1)) : (S.stage i).IdealSheaf

The marked transforms (I_i, m) along the sequence [Kol07, Definition 66 (1′)]: I_0 = J and I_{i+1} = (π_i)^{-1}_*(I_i, m), defined recursively along the sequence and never as a function of the composite alone (the caution Kollár attaches to his Definition 48).

Equations

• S.markedTransformSeq J m i = S.markedTransformSeqAux J m ↑i ⋯