Finite successions of monoidal transformations

A finite succession of monoidal transformations X_r → ⋯ → X_1 → X_0 = X with centres D_i ⊆ X_i, X_{i+1} = D_i.blowUp [Hir64, Main Theorem I, p. 132]; [Kol07, Definition 29], as an inductive type BlowUpSequence X: a list of centres, each living on the blow-up of the previous stage. Empty and trivial centres are allowed [Kol07, Warning 20]. Everything attached to a succession is a recursive function of its list of centres:

• its length r, stages X_i, centres D_i, partial composites Π_i : X_i ⟶ X and composite Π : X_r ⟶ X (Hironaka's f);
• Hironaka's weak transforms J_i and boundaries E_i, E_{i+1} = red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i)) [Hir64, Main Theorem II (ii), (iii)]; Kollár's total transforms of a divisor family and the strict transforms of a closed subscheme [Kol07, Definitions 25 and 30];
• the pull-back along a morphism and the push-forward along a closed immersion [Kol07, Definition 30], and the deletion of the blow-ups with empty centre [Kol07, 32 and 34.1].

The functorial theorems assert the existence of blow-up sequence functors on their inputs [Kol07, Definition 31, Theorems 35 and 36]; [Wlo05, Theorem 1.0.2] (AlgebraicGeometry.BlowUpSequenceFunctor, Hironaka.Scheme.Resolution.Defs). Every scheme is over Spec k through a structure morphism that is separated and of finite type (FiniteType; Kollár's schemes of finite type over a field, made separated); smoothness over k is Mathlib's Smooth of the structure morphism.

Finite successions of monoidal transformations

inductive AlgebraicGeometry.Scheme.BlowUpSequence : Scheme → Type (u + 1)

A finite succession of monoidal transformations starting at X Hir64, Main Theorem I, p. 132; [Kol07, Definition 29]: nil X is the empty succession, and cons X D S' is the blow-up of X with centre D followed by the succession S' starting at D.blowUp. Stages, centres and composites are recovered by BlowUpSequence.stage, center, stageMap, composite. Empty and trivial centres are allowed [Kol07, Warning 20].

• nil (X : Scheme) : X.BlowUpSequence
• cons (X : Scheme) (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) : X.BlowUpSequence

def AlgebraicGeometry.Scheme.BlowUpSequence.length {X : Scheme} : X.BlowUpSequence → ℕ

The number r of monoidal transformations in the succession.

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝).length = 0
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).length = rest.length + 1

def AlgebraicGeometry.Scheme.BlowUpSequence.stage {X : Scheme} (S : X.BlowUpSequence) : Fin (S.length + 1) → Scheme

The stage X_i, 0 ≤ i ≤ r, with X_0 = X.

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝).stage x_3 = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).stage ⟨0, isLt⟩ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).stage ⟨j.succ, h⟩ = rest.stage ⟨j, ⋯⟩

def AlgebraicGeometry.Scheme.BlowUpSequence.center {X : Scheme} (S : X.BlowUpSequence) (i : Fin S.length) : (S.stage i.castSucc).IdealSheafData

The centre D_i ⊆ X_i of the i-th monoidal transformation, 0 ≤ i < r.

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝).center i = i.elim0
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).center ⟨0, isLt⟩ = D
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).center ⟨j.succ, h⟩ = rest.center ⟨j, ⋯⟩

def AlgebraicGeometry.Scheme.BlowUpSequence.stageMap {X : Scheme} (S : X.BlowUpSequence) (i : Fin (S.length + 1)) : S.stage i ⟶ X

The partial composite Π_i = f_0 ∘ ⋯ ∘ f_{i-1} : X_i ⟶ X (Kollár's Π_{i0}).

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝).stageMap x_3 = CategoryTheory.CategoryStruct.id x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).stageMap ⟨0, isLt⟩ = CategoryTheory.CategoryStruct.id x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝ D rest).stageMap ⟨j.succ, h⟩ = CategoryTheory.CategoryStruct.comp (rest.stageMap ⟨j, ⋯⟩) D.blowUpπ

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.last {X : Scheme} (S : X.BlowUpSequence) : Scheme

The final stage X_r.

Equations

• S.last = S.stage (Fin.last S.length)

noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.composite {X : Scheme} (S : X.BlowUpSequence) : S.last ⟶ X

The composite Π = f_0 ∘ ⋯ ∘ f_{r-1} : X_r ⟶ X of the whole succession (Hironaka's f).

Equations

• S.composite = S.stageMap (Fin.last S.length)

Transforms along a succession

def AlgebraicGeometry.Scheme.BlowUpSequence.weakTransformSeq {X : Scheme} (S : X.BlowUpSequence) : X.IdealSheafData → (i : Fin (S.length + 1)) → (S.stage i).IdealSheafData

Hironaka's sequence of weak transforms: J_0 = J and J_{i+1} the weak transform of J_i by f_i [Hir64, Main Theorem II (ii)].

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹).weakTransformSeq x✝ x_5 = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).weakTransformSeq x✝ ⟨0, isLt⟩ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).weakTransformSeq x✝ ⟨j.succ, h⟩ = rest.weakTransformSeq (x✝.weakTransform D) ⟨j, ⋯⟩

def AlgebraicGeometry.Scheme.BlowUpSequence.boundarySeq {X : Scheme} (S : X.BlowUpSequence) : X.IdealSheafData → (i : Fin (S.length + 1)) → (S.stage i).IdealSheafData

Hironaka's sequence of boundaries: E_0 = E and E_{i+1} = red(f_i⁻¹(E_i) ∪ f_i⁻¹(D_i)) [Hir64, Main Theorem II (iii); Main Theorem II(N) (3)] (II(N) writes red(f_i⁻¹(E_i ∪ D_i)), the same reduced subscheme: both are the reduced structure on f_i⁻¹(|E_i| ∪ |D_i|)).

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹).boundarySeq x✝ x_5 = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).boundarySeq x✝ ⟨0, isLt⟩ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).boundarySeq x✝ ⟨j.succ, h⟩ = rest.boundarySeq (x✝.reducedTransform D) ⟨j, ⋯⟩

def AlgebraicGeometry.Scheme.BlowUpSequence.totalTransformSeq {X : Scheme} (S : X.BlowUpSequence) : X.DivisorFamily → (i : Fin (S.length + 1)) → (S.stage i).DivisorFamily

Kollár's total transform E_i = (π_0 ⋯ π_{i-1})⁻¹_*(E) + Ex_tot(π_0 ⋯ π_{i-1}) of a divisor family at stage i of the succession [Kol07, Definition 25].

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹).totalTransformSeq x✝ x_5 = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).totalTransformSeq x✝ ⟨0, isLt⟩ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).totalTransformSeq x✝ ⟨j.succ, h⟩ = rest.totalTransformSeq (x✝.totalTransform D) ⟨j, ⋯⟩

def AlgebraicGeometry.Scheme.BlowUpSequence.strictTransformSeq {X : Scheme} (S : X.BlowUpSequence) : X.IdealSheafData → (i : Fin (S.length + 1)) → (S.stage i).IdealSheafData

The strict transform Y_i ⊆ X_i of a closed subscheme Y ⊆ X along the succession [Kol07, Definition 30.2]; Włodarczyk's Y_i [Wlo05, Theorem 1.0.2 (b)].

Equations

• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹).strictTransformSeq x✝ x_5 = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).strictTransformSeq x✝ ⟨0, isLt⟩ = x✝
• (AlgebraicGeometry.Scheme.BlowUpSequence.cons x✝¹ D rest).strictTransformSeq x✝ ⟨j.succ, h⟩ = rest.strictTransformSeq (x✝.strictTransform D) ⟨j, ⋯⟩

Pull-back, push-forward, and the deletion of empty blow-ups

def AlgebraicGeometry.Scheme.BlowUpSequence.pullback {X : Scheme} : X.BlowUpSequence → {Y : Scheme} → (Y ⟶ X) → Y.BlowUpSequence

The pull-back h^* B of a succession along h : Y ⟶ X [Kol07, Definition 30.1]: blow up the inverse image centres h⁻¹(Z_i); for smooth (more generally flat) h the stages are X_i ×_X Y.

Equations

• One or more equations did not get rendered due to their size.
• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝²).pullback x✝ = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝¹

def AlgebraicGeometry.Scheme.BlowUpSequence.pushforward {Y : Scheme} : Y.BlowUpSequence → {X : Scheme} → (j : Y ⟶ X) → [IsClosedImmersion j] → X.BlowUpSequence

The push-forward j_* B(S) of a succession on a closed subscheme S ⊆ X along the closed immersion j : S ⟶ X [Kol07, Definition 30.3]: the centres Z_i^S viewed in X_i, Z_i^X := (j_i)_* Z_i^S along the inclusions j_i : S_i ↪ X_i (pushforwardBlowUp). The instance argument [IsClosedImmersion j] is what makes the recursion well defined: pushforwardBlowUp exists only for closed immersions.

Equations

• One or more equations did not get rendered due to their size.
• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝³).pushforward x✝¹ = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝²

def AlgebraicGeometry.Scheme.BlowUpSequence.eraseEmpty {X : Scheme} : X.BlowUpSequence → X.BlowUpSequence

Delete every blow-up whose centre is empty (the unit ideal sheaf ⊤) and reindex the remaining ones [Kol07, 32 and 34.1]. The empty blow-up cons X ⊤ rest is removed by carrying its tail rest, a succession on blowUp X ⊤, back to X along the inverse of the isomorphism blowUpπ X ⊤ (the empty blow-up is trivial, [Kol07, Warning 20]: isInvertible_top, blowUp.isIso_π_of_isInvertible), which is pullback along that inverse.

Equations

• One or more equations did not get rendered due to their size.
• (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝).eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝