Step 3 and the dimension bound

The combinatorial state MonomialState carries the dimension bound n as a data field. It is read by step3 for the number of phases (phases st.n 1 st _, Kollár's Steps 3.1, …, 3.n of [Kol07, 111]) and by the invariant nerve_card (every face has at most n components), and by nothing else: faces, Star, choice, total, labelTuple, blowUpNerve and blowUp never consult it (blowUp copies it). The geometric Step 3 PieceFamily.realize n m hV therefore depends on n only through the phase count, and the phases beyond the true bound are trivial: a face of size s > n' does not exist when every face has at most n' components, so (∗_s) holds vacuously (star_of_lt), Kollár's choice is empty (choice_eq_empty_iff) and the phase returns the state unchanged with an empty run (phase_of_not_nonempty, phases_eq_of_star). Hence the realised Step 3 of a piece family is the same for any two dimension bounds n' ≤ n for which the family's data are valid (realize_eq_of_le).

The proof is a lockstep induction along the well-founded recursion of phase (phase.induct, as in Hironaka/Resolution/Algebraic/Monomial/Restrict/Phase.lean): two states with the same data and possibly different bounds (EqUpToDim) make the same choice, blow up to states again equal up to the bound, and so run the same phase (phase_eqUpToDim); the phases r, r + 1, … of two such states agree as soon as both runs reach the smaller bound (phases_eqUpToDim_le, an induction on the phase counts carrying the invariant; the extra phases of the longer run are empty by phases_eq_of_star, the bound read from the state with the smaller n, whose nerve_card bounds the common nerve).

Not in the sources: Kollár's n = dim X is the dimension of the ambient variety, and the question does not arise for him. It arises here because BMO_{n,m} is defined for every n and the induction on the dimension in Hironaka/Resolution/Algebraic/Stage/ compares the functors at n and at n' ≤ n on the same triple (Hironaka/Resolution/Algebraic/Stage/CongrBMO.lean).

structure Hironaka.Monomial.MonomialState.EqUpToDim (st st' : MonomialState) : Prop

Two states with the same data (mark, counters, labels, exponents and nerve) and possibly different dimension bounds n.

• m_eq : st.m = st'.m
• nextComp_eq : st.nextComp = st'.nextComp
• nextLabel_eq : st.nextLabel = st'.nextLabel
• label_eq : st.label = st'.label
• a_eq : st.a = st'.a
• nerve_eq : st.nerve = st'.nerve

def Hironaka.Monomial.MonomialState.withN (st : MonomialState) (n₀ : ℕ) (hc : ∀ T ∈ st.nerve, T.card ≤ n₀) : MonomialState

The state st with its dimension bound replaced by n₀ (a bound for its nerve).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Monomial.MonomialState.EqUpToDim.eq_withN {st st' : MonomialState} (h : st.EqUpToDim st') : st' = st.withN st'.n ⋯

A state equal to st up to the dimension bound is st with the other state's bound.

theorem Hironaka.Monomial.MonomialState.EqUpToDim.star {st st' : MonomialState} (h : st.EqUpToDim st') (s : ℕ) : st.Star s ↔ st'.Star s

States equal up to the dimension bound satisfy the same (∗_s).

theorem Hironaka.Monomial.MonomialState.EqUpToDim.choice {st st' : MonomialState} (h : st.EqUpToDim st') (r : ℕ) : st.choice r = st'.choice r

States equal up to the dimension bound make the same choice at every phase.

theorem Hironaka.Monomial.MonomialState.EqUpToDim.blowUp {st st' : MonomialState} (h : st.EqUpToDim st') (S : Finset (Finset ℕ)) : (st.blowUp S).EqUpToDim (st'.blowUp S)

Blowing up two states equal up to the dimension bound along the same centre gives states equal up to the dimension bound.

theorem Hironaka.Monomial.MonomialState.phase_eqUpToDim (r : ℕ) (st : MonomialState) (hs : ∀ s < r, st.Star s) (st' : MonomialState) (hs' : ∀ s < r, st'.Star s) : st.EqUpToDim st' → (phase r st hs).1.EqUpToDim (phase r st' hs').1 ∧ (phase r st hs).2 = (phase r st' hs').2

Two states equal up to the dimension bound run the same phase: the same centres, and final states again equal up to the dimension bound.

theorem Hironaka.Monomial.MonomialState.phases_eqUpToDim_le (k k' r : ℕ) (st st' : MonomialState) (hs : ∀ s < r, st.Star s) (hs' : ∀ s < r, st'.Star s) : st.EqUpToDim st' → st'.n < r + k → st'.n < r + k' → (phases k r st hs).2 = (phases k' r st' hs').2

The runs of the phases r, … of two states equal up to the dimension bound agree as soon as both runs reach the smaller dimension bound: the phases beyond it are empty (phases_eq_of_star, the bound read from the state with the smaller n).

theorem Hironaka.Monomial.MonomialState.step3_eqUpToDim_le {st st' : MonomialState} (h : st.EqUpToDim st') (hle : st'.n ≤ st.n) : st.step3.2 = st'.step3.2

The run of Step 3 of a state (Kollár's Steps 3.1, …, 3.n of [Kol07, 111]) is that of any state equal to it up to the dimension bound with a smaller bound: the phases n' + 1, …, n are empty.

theorem Hironaka.Monomial.PieceFamily.realize_eq_of_le {X : AlgebraicGeometry.Scheme} (Φ : PieceFamily X) {n n' m : ℕ} (hV : Φ.IsValid n m) (hV' : Φ.IsValid n' m) (h : n' ≤ n) : Φ.realize n m hV = Φ.realize n' m hV'

The realised Step 3 of a piece family does not depend on the dimension bound: for n' ≤ n and the family's data valid for both, the geometric Step 3 at n is the one at n'. The two combinatorial states are equal up to the dimension bound (toState's data fields are the family's), so their Step 3 runs agree (step3_eqUpToDim_le), and realizeAux reads the run only.