The geometric Step 3 as a blow-up sequence of order ≥ m

The fold PieceFamily.realize of the combinatorial run (Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean) is a smooth blow-up sequence of order ≥ m for the marked monomial ideal in the sense of [Kol07, Definition 66], and its marked transforms are the monomial ideals of the stage families. Not in the sources as statements; this is what Kollár's description of Step 3 in [Kol07, 111] amounts to once the blow-ups are performed on the piece families.

• markedTransformSeq_realizeAux, markedTransformSeq_realize: the marked transform at stage i is the monomial ideal of the stage-i family (markedTransform_monomial of Hironaka/Resolution/Algebraic/Monomial/Geometric/Transform.lean at each step, the centre being Kollár's choice on the stage state, of order ≥ m);
• isOrderGeSeq_realizeAux, realize_isOrderGeSeq: conditions (2′)–(4′) of [Kol07, Definition 66]. Every centre is smooth over k, has simple normal crossings with E_i, and the marked transform has order ≥ m along it, along an arbitrary run, each centre being Kollár's choice on the stage state;
• realize_maxOrd_lt: at the end of Step 3 the marked monomial ideal has max-ord < m, Kollár's "at the end of Step 3.n we are done". Every face of the final nerve has sum < m (step3_maxOrd_lt of Hironaka/Resolution/Algebraic/Monomial/Step3Phases.lean), and the order at a point is the sum over its face.

These are the properties of the third step of BMO_{n,m} that Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean packages.

The marked transforms along an arbitrary run

theorem Hironaka.Monomial.PieceFamily.markedTransformSeq_realizeAux {k : Type u} [Field k] [CharZero k] (L : List (Finset (Finset ℕ))) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} : E.IsSnc → Φ.Realizes E e → ∀ {n m : ℕ} (hV : Φ.IsValid n m), (∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) → ∀ {st' : MonomialState}, (Φ.toState n m hV).IsRun L st' → ∀ (i : Fin ((Φ.realizeAux m L).length + 1)), (Φ.realizeAux m L).markedTransformSeq (E.monomial Φ.exponentAt) m i = ((Φ.realizeAux m L).totalTransformSeq E i).monomial (Φ.stagePieces m L i).exponentAt

Along a run: the marked transform of the marked monomial ideal at stage i of the fold of a run is the monomial ideal of the stage-i piece family, by markedTransform_monomial at every step, each centre being Kollár's choice on the stage state, of order ≥ m.

The order sequence along an arbitrary run

theorem Hironaka.Monomial.PieceFamily.isOrderGeSeq_realizeAux {k : Type u} [Field k] [CharZero k] (L : List (Finset (Finset ℕ))) {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} : E.IsSnc → Φ.Realizes E e → ∀ {n m : ℕ} (hV : Φ.IsValid n m), (∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) → ∀ {st' : MonomialState}, (Φ.toState n m hV).IsRun L st' → (Φ.realizeAux m L).IsOrderGeSeq f (E.monomial Φ.exponentAt) m E

Along a run (conditions (2′)–(4′) of [Kol07, Definition 66]): the fold of a run is a smooth blow-up sequence of order ≥ m for the marked monomial ideal. Every centre is Kollár's choice on the stage state, so it is smooth over k (smooth_centerOf), has simple normal crossings with the stage boundary (hasSncWith_centerOf), and the stage monomial ideal has order ≥ m along it (leOrdAlong_centerOf), the stage monomial ideal being the marked transform (markedTransform_monomial).

The statements on realize

theorem Hironaka.Monomial.PieceFamily.markedTransformSeq_realize {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hV : Φ.IsValid n m) (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) (i : Fin ((Φ.realize n m hV).length + 1)) : (Φ.realize n m hV).markedTransformSeq (E.monomial Φ.exponentAt) m i = ((Φ.realize n m hV).totalTransformSeq E i).monomial (Φ.stagePieces m (Φ.toState n m hV).step3.2 i).exponentAt

The marked transform at stage i of the geometric Step 3 is the monomial ideal of the stage-i piece family, the recursion (1′) of [Kol07, Definition 66], I_{i+1} = (π_i)_*^{-1}(I_i, m), computed.

theorem Hironaka.Monomial.PieceFamily.realize_isOrderGeSeq {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hV : Φ.IsValid n m) (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) : (Φ.realize n m hV).IsOrderGeSeq f (E.monomial Φ.exponentAt) m E

The geometric Step 3 is a smooth blow-up sequence of order ≥ m starting with (X, 𝒪_X(−∑ a_D D), m, E) ([Kol07, Definition 66], for the run of [Kol07, 111, Step 3]): every centre is Kollár's choice at its stage, hence smooth with simple normal crossings with E_i and of order ≥ m for the induced marked ideal.

theorem Hironaka.Monomial.PieceFamily.realize_maxOrd_lt {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [AlgebraicGeometry.Smooth f] [AlgebraicGeometry.QuasiCompact f] (Φ : PieceFamily X) {E : X.DivisorFamily} {e : E.ι ≃o Fin Φ.nextLabel} {n m : ℕ} (hE : E.IsSnc) (hΦ : Φ.Realizes E e) (hV : Φ.IsValid n m) (hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) : ((Φ.realize n m hV).markedTransformSeq (E.monomial Φ.exponentAt) m (Fin.last (Φ.realize n m hV).length)).maxOrd < ↑m

At the end of Step 3 the induced marked monomial ideal has max-ord < m, the conclusion of [Kol07, 111, Step 3] ("at the end of Step 3.n we are done"): every face of the final nerve has sum < m (step3_maxOrd_lt), and the order at a point is the sum over its face (ord_monomial_eq_total); a point off the final boundary has the empty face.