One round of Main Theorem II on a triple

Hironaka's Main Theorem II [Hir64, Main Theorem II, pp. 142–143] on Kollár's triple (X, I, E) [Kol07, Notation 64] is Theorem 68 [Kol07, Theorem 68] with m := d = max-ord I, refined to irreducible centers (Hironaka/Resolution/Algebraic/Kol07/RefineIrreducible.lean) and read through the dictionary between the two vocabularies (Hironaka/Sequence/Dictionary*.lean). The round exists_orderReductionRound is the refined value of the order reduction functor BO_d: a smooth blow-up sequence of order d for the triple, with regular irreducible centers, whose last weak transform has max-ord < d (Theorem 68 (1)). IsOrderSeq.hironakaClauses reads Hironaka's clauses (ii), (iii) and the first part of (iv) off any such sequence, with Hironaka's E₀ the reduced union T.E.unionIdeal of Kollár's family (whose members may be reducible or empty), and IsOrderSeq.clause2 reads clause (2) of [Hir64, Main Theorem II(N)] off a round with irreducible centers. The only transport along the refinement's isomorphism is max-ord (maxOrd_comap_of_isIso). Main Theorem II(N) is proved by concatenating such rounds.

theorem Hironaka.Sequence.exists_orderReductionRound {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), S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E d ∧ (∀ (i : Fin S.length), AlgebraicGeometry.IsRegular (S.center i).subscheme ∧ IrreducibleSpace ↥(S.center i).subscheme) ∧ (S.weakTransformSeq T.I (Fin.last S.length)).maxOrd < ↑d

One round of Main Theorem II on a triple T with max-ord T.I = d ≥ 1: a smooth blow-up sequence of order d for (T.X.left, T.I, T.E) [Kol07, Definition 66] with regular irreducible centers, whose last weak transform has max-ord < d. It is the value of the order reduction functor BO_d Kol07, Theorem 68, with m := d refined to irreducible centers; the refinement's isomorphism e : S'.last ≅ S.last carries the last weak transform by inverse image, so its max-ord is that of the value of BO_d (maxOrd_comap_of_isIso).

theorem Hironaka.Sequence.IsOrderSeq.hironakaClauses {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {d : ℕ} {S : T.X.left.BlowUpSequence} (h : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E d) : (∀ (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

Hironaka's clauses (ii), (iii) and the first part of (iv) of [Hir64, Main Theorem II], read off a smooth blow-up sequence of order d for (T.X.left, T.I, T.E) [Kol07, Definition 66] at every index, with Hironaka's E₀ := T.E.unionIdeal (the reduced union of Kollár's family): (ii) ν(J_i) ≥ d on every center; (iii) the boundary E_i, the reduced union of Kollár's total transform E_i, has only normal crossings with the center (condition (3) of Definition 66 at the stage's structure morphism); (iv) the last boundary has only normal crossings (the total transforms are simple normal crossing families).

theorem Hironaka.Sequence.IsOrderSeq.clause2 {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) {d : ℕ} {S : T.X.left.BlowUpSequence} (h : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.E d) (hd : T.I.maxOrd = ↑d) (hd0 : 0 < d) (hirr : ∀ (i : Fin S.length), 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'

Clause (2) of [Hir64, Main Theorem II(N)] inside one round (Hironaka's remark after Main Theorem II: d is the maximum of ν(J_i) at every stage): along a smooth blow-up sequence of order d = max-ord J with irreducible, hence nonempty, centers, at every stage i the maximal order of J_i is the positive integer d, attained at every point of the center.