Hironaka's Main Theorem II and Main Theorem II(N) on a triple

Hironaka's Main Theorem II [Hir64, Main Theorem II] and Main Theorem II(N) [Hir64, Main Theorem II(N)] on a triple (X, I, E) in the sense of [Kol07, Notation 64], with Hironaka's boundary E₀ the reduced union T.E.unionIdeal of the family: the two theorems here are the triple-level forms. The module Hironaka.Resolution.Algebraic.Hir64.ComponentwiseMainTheorems proves the two main theorems exists_blowUpSequence_ord_weakTransformSeq_lt and exists_blowUpSequence_weakTransformSeq_eq_top, stated in Hironaka's own vocabulary for every smooth scheme, not from these but from the round exists_orderReductionRound and isHironakaIIN_concat, run component by component.

• exists_orderReduction_irreducible (Main Theorem II): one round of order reduction (exists_orderReductionRound, Kollár's BO_d of [Kol07, Theorem 68] with the centers refined to irreducible ones) and its clauses (IsOrderSeq.hironakaClauses; the second part of clause (iv), ν(J_r) < d at every point, is the conclusion max-ord I_r < d of Theorem 68 read pointwise).
• exists_principalization_irreducible (Main Theorem II(N)): Theorem 68 iterated. By induction on a bound for max-ord T.I (a natural number, since T.I is nonzero everywhere on the Noetherian T.X.left): max-ord = 0 means T.I = 𝒪, where the empty sequence does (clause (4)); otherwise one round is followed by the induction hypothesis at the induced triple of the round's last stage (Triple.induced, the transform of [Kol07, Definition 66 (1)]), whose ideal has smaller max-ord and whose family's reduced union is the round's last boundary, so the tail continues Hironaka's E_i; the rounds are concatenated (isHironakaIIN_concat). Clause (2) inside a round, the order of the weak transform along the center being the maximal order, is IsOrderSeq.clause2; this is why Main Theorem II(N) is Theorem 68 iterated and not Kollár's principalization theorem, whose BMO_1 centers have only marked order ≥ 1. Hironaka's own derivation, through his fundamental theorems on resolution data in the paragraph following the statement of Main Theorem II(N), is not followed.

def Hironaka.Sequence.IINStage {Y : AlgebraicGeometry.Scheme} (D J E : Y.IdealSheafData) : Prop

Clauses (1)–(3) of [Hir64, Main Theorem II(N)] at one stage: the center D is regular and irreducible, the maximal order of the ideal J is a positive integer attained on all of D, and the boundary E has only normal crossings with D.

Equations

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

def AlgebraicGeometry.Scheme.BlowUpSequence.IsHironakaIIN {X : Scheme} (S : X.BlowUpSequence) (J E₀ : X.IdealSheafData) : Prop

The conclusion of [Hir64, Main Theorem II(N)] for a sequence S started at (J, E₀): clauses (1)–(3) at every stage, clause (4) (the final boundary has only normal crossings and the final weak transform is the unit ideal) at the end.

Equations

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

theorem Hironaka.Sequence.isHironakaIIN_concat {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (J E₀ : X.IdealSheafData) (hS : ∀ (i : Fin S.length), IINStage (S.center i) (S.weakTransformSeq J i.castSucc) (S.boundarySeq E₀ i.castSucc)) (hT : T.IsHironakaIIN (S.weakTransformSeq J (Fin.last S.length)) (S.boundarySeq E₀ (Fin.last S.length))) : (S.concat T).IsHironakaIIN J E₀

The rounds concatenate: clauses (1)–(3) at every stage of S and the conclusion of Main Theorem II(N) for T started at the last transforms of S give the conclusion for S.concat T.

theorem Hironaka.Sequence.isHironakaIIN_nil_of_eq_top {k : Type u} [Field k] (T : AlgebraicGeometry.Triple k) (hJ : T.I = ⊤) : (AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left).IsHironakaIIN T.I T.E.unionIdeal

Main Theorem II(N) with J = 𝒪: the empty sequence does, clause (4) holding at the start.

theorem Hironaka.Sequence.exists_isHironakaIIN_of_maxOrd_le {k : Type u} [Field k] [CharZero k] (d : ℕ) (T : AlgebraicGeometry.Triple k) : T.I.maxOrd ≤ ↑d → ∃ (S : T.X.left.BlowUpSequence), S.IsHironakaIIN T.I T.E.unionIdeal

[Kol07, Theorem 68] iterated: Main Theorem II(N) on every triple whose ideal has max-ord ≤ d, by induction on d. If max-ord T.I = 0 then T.I = 𝒪 and the empty sequence does; otherwise one round of order d₀ = max-ord T.I (exists_orderReductionRound) is followed by the induction hypothesis at the induced triple of its last stage (Triple.induced), whose ideal has max-ord < d₀ ≤ d + 1, and the two are concatenated.

theorem Hironaka.Sequence.exists_isHironakaIIN {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : ∃ (S : T.X.left.BlowUpSequence), S.IsHironakaIIN T.I T.E.unionIdeal

The conclusion of Main Theorem II(N) on every triple: max-ord T.I is a natural number, since T.I is nonzero everywhere on the Noetherian T.X.left.

theorem Hironaka.Sequence.exists_orderReduction_irreducible {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (d : ℕ) (hd : T.I.maxOrd = ↑d) (hd0 : 0 < d) : ∃ (S : T.X.left.BlowUpSequence), (∀ (i : Fin S.length), AlgebraicGeometry.IsRegular (S.center i).subscheme ∧ IrreducibleSpace ↥(S.center i).subscheme) ∧ (∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, ↑d ≤ (S.weakTransformSeq T.I i.castSucc).ord x) ∧ (∀ (i : Fin S.length), (S.boundarySeq T.E.unionIdeal i.castSucc).IsSncBoundaryWith (S.center i)) ∧ (S.boundarySeq T.E.unionIdeal (Fin.last S.length)).IsSncBoundary ∧ ∀ (y : ↥S.last), (S.weakTransformSeq T.I (Fin.last S.length)).ord y < ↑d

Hironaka's Main Theorem II [Hir64, Main Theorem II] on a triple: a finite succession of monoidal transformations with non-singular irreducible centers such that (i)–(iii) hold at every stage (the center is regular and irreducible, the weak transform has order ≥ d along it, the boundary has only normal crossings with it) and (iv) at the end (the boundary has only normal crossings and the weak transform has order < d everywhere). One round of order reduction, with the second part of (iv) the conclusion max-ord I_r < d of [Kol07, Theorem 68] read pointwise.

theorem Hironaka.Sequence.exists_principalization_irreducible {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) : ∃ (S : T.X.left.BlowUpSequence), (∀ (i : Fin S.length), AlgebraicGeometry.IsRegular (S.center i).subscheme ∧ IrreducibleSpace ↥(S.center i).subscheme) ∧ (∀ (i : Fin S.length), ∃ (d : ℕ), 0 < d ∧ IsGreatest (Set.range (S.weakTransformSeq T.I i.castSucc).ord) ↑d ∧ ∀ z ∈ (S.center i).support, (S.weakTransformSeq T.I i.castSucc).ord z = ↑d) ∧ (∀ (i : Fin S.length), (S.boundarySeq T.E.unionIdeal i.castSucc).IsSncBoundaryWith (S.center i)) ∧ (S.boundarySeq T.E.unionIdeal (Fin.last S.length)).IsSncBoundary ∧ S.weakTransformSeq T.I (Fin.last S.length) = ⊤

Hironaka's Main Theorem II(N) [Hir64, Main Theorem II(N)] on a triple: a finite succession of monoidal transformations with non-singular irreducible centers along which the weak transform has constant order equal to its maximal order, a positive integer, with the boundary having only normal crossings with each center, whose final boundary has only normal crossings and whose final weak transform is the unit ideal; IsHironakaIIN unfolded.