Canonicity of the base stage and the dimension bookkeeping

[Kol07, 70] starts the induction on n = dim X with the case dim X = 0, where I = 𝒪_X since I is nonzero on every irreducible component and "everything is resolved without blow-ups". The step n → n + 1 is Hironaka.Stage.tower base, a tower over an arbitrary base base : OrderReductionStage 0, and Hironaka.Resolution.Algebraic.Stage.Base supplies the base stage0, whose functors are the empty sequence nil. This module proves that the base is FORCED, at two levels:

• Sequence level. Every stage-0 package S is nil on its class: a triple of dimension ≤ 0 has I = 𝒪_X (Triple.I_eq_top_of_hasDimLE_zero), so any smooth blow-up sequence of order m ≥ 1 on it has no centre of order ≥ m to blow up — OrderSeqAssignment.seq_eq_nil_of_hasDimLE_zero and its marked form, applied to the functor fields of S.bo m and S.bmo m (bo_seq_eq_nil, bmo_seq_eq_nil).
• Structure level. Two stage-0 packages are EQUAL (OrderReductionStage.zero_subsingleton, a Subsingleton instance): a BOData/BMOData is its functor plus propositions, a functor is its seq plus propositions (OrderSeqAssignment.ext, OrderGeSeqAssignment.ext), and the two seqs agree by the sequence-level fact. Hence tower base = tower stage0 for every base by congrArg, the form used when a statement about the tower is proved over an arbitrary base. exists_stage0 is the existential form.

The dimension bookkeeping: Triple.dim (Hironaka.Resolution.Algebraic.Stage.Dim) is a relative dimension of the structure morphism; on a nonempty scheme it is THE relative dimension (SmoothOfRelativeDimension.eq_of_nonempty), so HasDim n ↔ dim = n and HasDimLE n ↔ dim ≤ n ([Nonempty T.X.left] is needed: on X = ∅ every n is a relative dimension). The classes at the canonical stage dim X lose their dimension clause (boClass_dim, bmoClass_dim), and "stage (dim X) is the canonical stage" is the coherence of Hironaka.Resolution.Algebraic.Stage.Coherence at n' := dim X (tower_bo_dim, tower_bmo_dim): every stage n ≥ dim X of the tower takes the same value at X.

theorem Hironaka.Stage.bo_seq_eq_nil (S : OrderReductionStage 0) (m : ℕ) (k : Type u) [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass 0 m T) : ((S.bo m).functor k).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

"Everything is resolved without blow-ups" [Kol07, 70]: EVERY stage-0 package is nil on the unmarked class — the dimension-0 lemma at the functor field of S.bo m (the class gives 1 ≤ m and HasDimLE 0).

theorem Hironaka.Stage.bmo_seq_eq_nil (S : OrderReductionStage 0) (m : ℕ) (k : Type u) [Field k] [CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.BMOClass 0 m T) : ((S.bmo m).functor k).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

EVERY stage-0 package is nil on the marked class — the marked dimension-0 lemma at the functor field of S.bmo m (the class gives T.m = m ≥ 1 and HasDimLE 0).

theorem Hironaka.OrderReductionStage.zero_subsingleton (S S' : OrderReductionStage 0) : S = S'

The base is unique: two stage-0 packages are equal, because their functors take the same value nil on every triple of the class (bo_seq_eq_nil, bmo_seq_eq_nil) and the remaining fields are propositions (BOData.ext, BMOData.ext). Consequently tower base = tower stage0 for every base, by congrArg.

instance Hironaka.OrderReductionStage.instSubsingletonZero : Subsingleton (OrderReductionStage 0)

The base stage as a Subsingleton instance (tower base = tower stage0 by Subsingleton.elim).

theorem Hironaka.Stage.exists_stage0 : ∃ (S : OrderReductionStage 0), (∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass 0 m T), ((S.bo m).functor k).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left) ∧ ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.BMOClass 0 m T), ((S.bmo m).functor k).seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

The existential form of stage0: a stage-0 package with nil-valued functors exists.

theorem AlgebraicGeometry.Triple.hasDim_iff_dim_eq {k : Type u} [Field k] (T : Triple k) [Nonempty ↥T.X.left] (n : ℕ) : T.HasDim n ↔ T.dim = n

On a nonempty scheme the chosen dimension is THE relative dimension: n is a relative dimension of the structure morphism iff n = dim (uniqueness of the relative dimension of a smooth morphism with nonempty source, SmoothOfRelativeDimension.eq_of_nonempty).

theorem AlgebraicGeometry.Triple.hasDimLE_iff_dim_le {k : Type u} [Field k] (T : Triple k) [Nonempty ↥T.X.left] (n : ℕ) : T.HasDimLE n ↔ T.dim ≤ n

On a nonempty scheme, "dimension ≤ n" is dim ≤ n.

theorem AlgebraicGeometry.Triple.boClass_dim {k : Type u} [Field k] (T : Triple k) (m : ℕ) : BOClass T.dim m T ↔ 1 ≤ m ∧ T.I.maxOrd ≤ ↑m

At the canonical stage dim X the unmarked class loses its dimension clause: BOClass (dim X) m is 1 ≤ m ∧ max-ord I ≤ m, the domain of [Kol07, Theorem 68].

theorem Hironaka.MarkedTriple.bmoClass_dim {k : Type u} [Field k] (T : MarkedTriple k) (m : ℕ) : BMOClass T.dim m T ↔ 1 ≤ m ∧ T.m = m

At the canonical stage dim X the marked class loses its dimension clause: BMOClass (dim X) m is 1 ≤ m ∧ T.m = m, the domain of [Kol07, Theorem 69].

theorem Hironaka.Stage.tower_bo_dim (base : OrderReductionStage 0) {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : AlgebraicGeometry.Triple k) (hle : T.dim ≤ n) (hT : AlgebraicGeometry.Triple.BOClass n m T) (hT' : AlgebraicGeometry.Triple.BOClass T.dim m T) : (((tower base n).bo m).functor k).seq T hT = (((tower base T.dim).bo m).functor k).seq T hT'

stage (dim X) is the canonical stage ([Kol07, 70]): every stage n ≥ dim X of the tower takes at X the value of stage dim X (tower_bo_coherent at n' := dim X).

theorem Hironaka.Stage.tower_bmo_dim (base : OrderReductionStage 0) {k : Type u} [Field k] [CharZero k] {n m : ℕ} (T : MarkedTriple k) (hle : T.dim ≤ n) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass T.dim m T) : (((tower base n).bmo m).functor k).seq T hT = (((tower base T.dim).bmo m).functor k).seq T hT'

The marked form of tower_bo_dim (tower_bmo_coherent at n' := dim X).