The realisation invariant along the fold

The geometric Step 3 is the fold of the combinatorial run (step3 st).2 into a blow-up sequence (PieceFamily.realize of Hironaka/Resolution/Algebraic/Monomial/Geometric/Pieces.lean), carrying the piece family along. This module proves the realisation invariant: at every stage i the stage family is Valid, its state is the fold of the first i centres into the initial state, it realises the total transform E_i, and the stage is smooth over k of relative dimension ≤ n with E_i snc. The proof is an induction along the list of centres, each step being the nerve transition of Hironaka/Resolution/Algebraic/Monomial/Geometric/Kernel.lean (toState_blowUpPieces, valid_blowUpPieces, realizes_blowUpPieces) together with the facts that the total transform of an snc boundary under a blow-up with simple normal crossings is snc (AlgebraicGeometry.totalTransform_isSnc of Hironaka/Scheme/BlowUpSequence/Triple.lean) and that the blow-up of a smooth centre of a smooth scheme is smooth. Not in the sources as a statement; it is the bookkeeping that lets Kollár's blow-up by blow-up description of [Kol07, 111, Step 3] be iterated.

• realizeAux_invariant: the invariant along an arbitrary run;
• valid_stagePieces, realize_invariant, realizes_stagePieces, isSnc_totalTransformSeq_realize, exists_smoothOfRelativeDimension_stageMap_realize: the same on realize;
• exists_center_realize_eq: the i-th centre of the geometric Step 3 is Kollár's choice on the stage state;
• realize_noEmptyCenters: no centre of the geometric Step 3 is empty, so no deletion of empty blow-ups in the sense of [Kol07, 32] is ever needed for Step 3 itself.

The invariant is what Hironaka/Resolution/Algebraic/Monomial/Geometric/OrderSeq.lean and Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean read at every stage.

The invariant along an arbitrary run

theorem Hironaka.Monomial.PieceFamily.realizeAux_invariant {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} (_hE : E.IsSnc) (_hΦ : Φ.Realizes E e) {n m : ℕ} (hV : Φ.IsValid n m) (_hn : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' f) {st' : MonomialState} (_hrun : (Φ.toState n m hV).IsRun L st') (i : Fin ((Φ.realizeAux m L).length + 1)) : ((Φ.realizeAux m L).totalTransformSeq E i).IsSnc ∧ (∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' (CategoryTheory.CategoryStruct.comp ((Φ.realizeAux m L).stageMap i) f)) ∧ ∃ (hV' : (Φ.stagePieces m L i).IsValid n m), (Φ.stagePieces m L i).toState n m hV' = List.foldl MonomialState.blowUp (Φ.toState n m hV) (List.take (↑i) L) ∧ (Φ.stagePieces m L i).Realizes ((Φ.realizeAux m L).totalTransformSeq E i) (Φ.stageIso m E e L i)

The realisation invariant along a run of the combinatorial state: at every stage the total transform is snc, the stage is smooth over k of relative dimension ≤ n, the stage family is Valid, its state is the fold of the centres so far, and it realises the total transform through the stage label isomorphism.

The statements on realize

theorem Hironaka.Monomial.PieceFamily.valid_stagePieces {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)) : (Φ.stagePieces m (Φ.toState n m hV).step3.2 i).IsValid n m

The stage-i piece family's data are Valid.

theorem Hironaka.Monomial.PieceFamily.realize_invariant {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)) (hV' : (Φ.stagePieces m (Φ.toState n m hV).step3.2 i).IsValid n m) : (Φ.stagePieces m (Φ.toState n m hV).step3.2 i).toState n m hV' = List.foldl MonomialState.blowUp (Φ.toState n m hV) (List.take (↑i) (Φ.toState n m hV).step3.2)

The realisation invariant: the state of the stage-i piece family of the fold of the combinatorial run is the fold of the first i centres into the initial state.

theorem Hironaka.Monomial.PieceFamily.realizes_stagePieces {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)) : (Φ.stagePieces m (Φ.toState n m hV).step3.2 i).Realizes ((Φ.realize n m hV).totalTransformSeq E i) (Φ.stageIso m E e (Φ.toState n m hV).step3.2 i)

The stage-i piece family realises the total transform E_i ([Kol07, Definition 65] iterated) through the stage label isomorphism.

theorem Hironaka.Monomial.PieceFamily.isSnc_totalTransformSeq_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).totalTransformSeq E i).IsSnc

The total transform at every stage of the geometric Step 3 is snc.

theorem Hironaka.Monomial.PieceFamily.exists_smoothOfRelativeDimension_stageMap_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)) : ∃ n' ≤ n, AlgebraicGeometry.SmoothOfRelativeDimension n' (CategoryTheory.CategoryStruct.comp ((Φ.realize n m hV).stageMap i) f)

Every stage of the geometric Step 3 is smooth over k of relative dimension ≤ n.

theorem Hironaka.Monomial.PieceFamily.exists_center_realize_eq {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n m : ℕ} (hV : Φ.IsValid n m) (i : Fin (Φ.realize n m hV).length) : ∃ (r : ℕ), 1 ≤ r ∧ ((List.foldl MonomialState.blowUp (Φ.toState n m hV) (List.take (↑i) (Φ.toState n m hV).step3.2)).choice r).Nonempty ∧ (Φ.toState n m hV).step3.2.get (Fin.cast ⋯ i) = (List.foldl MonomialState.blowUp (Φ.toState n m hV) (List.take (↑i) (Φ.toState n m hV).step3.2)).choice r

The i-th centre of the geometric Step 3, read on the stage family: Kollár's choice on the stage state, a centre with faces of sum ≥ m.

theorem Hironaka.Monomial.PieceFamily.realize_noEmptyCenters {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).NoEmptyCenters

The geometric Step 3 has no empty blow-ups ([Kol07, 32]): each centre is a nonempty set of faces of the nerve of the stage family.