Step 3 of marked order reduction: the geometric monomial step on a marked triple

Step 3 of the proof of [Kol07, Theorem 107] ([Kol07, 111, Step 3]) treats the monomial case: a smooth variety X, a simple normal crossing divisor ∪_{j ∈ J} E^j with ordered index set J, and the monomial ideal I = 𝒪_X(−∑ a_j E^j) for natural numbers a_j. After Step 2 the marked triple (X, I, m, E) has cosupp(I, m) ∩ cosupp N(I) = ∅, and Kollár runs Step 3 for M(I) on X ∖ cosupp N(I), where I = M(I). Here the geometric Step 3 of Hironaka/Resolution/Algebraic/Monomial/Geometric/ is run on X itself for the marked ideal (M(I), m): its centres lie in cosupp(M(I), m) ⊆ cosupp(I, m), hence off cosupp N(I), and the sequence is of order ≥ m for (I, m) because I ⊆ M(I) (Hironaka/Scheme/BlowUpSequence/MarkedMono.lean).

The geometric Step 3 (PieceFamily.realize, Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean) takes a piece family realizing E: the irreducible components of the members, enumerated, with the exponent at each generic point. This module builds that input from a marked triple and reads the results of the run for (I, m).

• labelIso E, componentsEquiv E: the enumerations (the finite linear order E.ι against Fin, and the finitely many generic points of the members on the Noetherian X).
• step3Family T: ofDivisorFamily on T.E with the exponents of the monomial part M(I) = E.monomial (fun η => (ord_η I).toNat) (Kollár's a_j = ord_{E^j} I, the orders of I at the generic points of the components, where ord N(I) = 0, so they are the orders of M(I) too); it realizes T.E (step3Family_realizes), and its marked monomial ideal is M(I) (monomial_exponentAt_step3Family).
• step3Seq T hT: the geometric Step 3 of (X, M(I), m, E) on X (realize on the state toState, valid by valid_of_realizes from the class BMOClass n m): a smooth blow-up sequence of order ≥ m for (X, I, m, E) (step3Seq_isOrderGeSeq), without empty blow-ups (step3Seq_noEmptyCenters), at whose end the marked transform of M(I) has max-ord < m (step3Seq_maxOrd_lt).

The assembly of the three steps is Hironaka/Resolution/Algebraic/MarkedOrderReduction/Assembly.lean; that the run reduces the order of (I, m) itself, not only of (M(I), m), is Hironaka/Resolution/Algebraic/MarkedOrderReduction/Clause1.lean.

theorem Hironaka.BMO.finite_components {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.DivisorFamily) : Finite (Monomial.PieceFamily.Components E)

The finitely many irreducible components of the members of E (their generic points) form a finite type on a Noetherian scheme.

noncomputable def Hironaka.BMO.labelIso {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) : E.ι ≃o Fin (Fintype.card E.ι)

The label isomorphism of Step 3's input: the finite linear order E.ι of the members against Fin (monoEquivOfFin), labels counted from 0 in the order of E.

Equations

• Hironaka.BMO.labelIso E = (monoEquivOfFin E.ι ⋯).symm

noncomputable def Hironaka.BMO.componentsEquiv {X : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥X] (E : X.DivisorFamily) : Fin (Nat.card (Monomial.PieceFamily.Components E)) ≃ Monomial.PieceFamily.Components E

An enumeration of the irreducible components of the members of E (their generic points), the component data of Step 3's input piece family.

Equations

• Hironaka.BMO.componentsEquiv E = (Finite.equivFin (Hironaka.Monomial.PieceFamily.Components E)).symm

noncomputable def Hironaka.BMO.step3Family {k : Type u} [Field k] (T : MarkedTriple k) : Monomial.PieceFamily T.X.left

Step 3's input piece family of a marked triple ([Kol07, 111, Step 3]: the normal-crossings divisor ∪ E^j with ordered index set J and the exponents a_j of the monomial ideal 𝒪_X(−∑ a_j E^j), here for M(I) after Step 2): ofDivisorFamily on T.E, the irreducible components of the members with the exponents a_j = ord_{E^j} I of the monomial part M(I) at their generic points (monomialPart I E = E.monomial (fun η => (ord_η I).toNat)).

Equations

• Hironaka.BMO.step3Family T = Hironaka.Monomial.PieceFamily.ofDivisorFamily T.E (fun (x : ↥T.X.left) => (T.I.ord x).toNat) (Hironaka.BMO.labelIso T.E) (Hironaka.BMO.componentsEquiv T.E)

theorem Hironaka.BMO.step3Family_realizes {k : Type u} [Field k] (T : MarkedTriple k) : (step3Family T).Realizes T.E (labelIso T.E)

Step 3's input family realizes the boundary T.E through the label isomorphism (ofDivisorFamily_realizes).

theorem Hironaka.BMO.monomial_exponentAt_step3Family {k : Type u} [Field k] (T : MarkedTriple k) : T.E.monomial (step3Family T).exponentAt = monomialPart T.I T.E

The marked monomial ideal of Step 3's input family is the monomial part M(I): monomial_exponentAt_ofDivisorFamily at the exponents (ord_η I).toNat (the exponent at a point is that of the piece through it, read at the generic points), and monomialPart I E = E.monomial (fun η => (ord_η I).toNat) by definition.

theorem Hironaka.BMO.step3Family_isValid {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) : (step3Family T).IsValid n m

For a marked triple of BMOClass n m the input family's data are valid (valid_of_realizes): 1 ≤ m and dim X ≤ n are the class's, the normal crossings are the triple's; so the state toState and its run are defined.

noncomputable def Hironaka.BMO.step3Seq {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) : T.X.left.BlowUpSequence

The geometric Step 3 of a marked triple ([Kol07, 111, Step 3], run for M(I) on X): PieceFamily.realize of the combinatorial run on Step 3's input family.

Equations

• Hironaka.BMO.step3Seq T hT = (Hironaka.BMO.step3Family T).realize n m ⋯

theorem Hironaka.BMO.step3Seq_isOrderGeSeq {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) : (step3Seq T hT).IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E

Step 3 is a smooth blow-up sequence of order ≥ m for (X, I, m, E) (conditions (2′)–(4′) of [Kol07, Definition 66] for (I, m)): it is one for (X, M(I), m, E) (realize_isOrderGeSeq through monomial_exponentAt_step3Family), and I ⊆ M(I) by the split I = M(I) · N(I), so the order at every centre is at least as large (isOrderGeSeq_of_le).

theorem Hironaka.BMO.step3Seq_noEmptyCenters {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) : (step3Seq T hT).NoEmptyCenters

Step 3 contains no empty blow-up ([Kol07, 32]; realize_noEmptyCenters).

theorem Hironaka.BMO.step3Seq_maxOrd_lt {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) : ((step3Seq T hT).markedTransformSeq (monomialPart T.I T.E) m (Fin.last (step3Seq T hT).length)).maxOrd < ↑m

At the end of Step 3 the marked transform of the monomial part has max-ord < m ([Kol07, 111, Step 3]: "at the end of Step 3.n we are done"; realize_maxOrd_lt).