Clause (3) of marked order reduction: agreement with order reduction for ideals

Clause (3) of [Kol07, Theorem 107]: BMO_{n,m}(X, I, m, ∅) = BO_{n,m}(X, I, ∅) when m = max-ord I. Kollár's proof, the last paragraph of [Kol07, 111]: for E = ∅ one has N(I) = I; if moreover m = max-ord I, Step 1 consists of the single round BO_{n,m}(X, I, ∅), each of whose blow-ups has order exactly m, so the birational transforms of I agree with those of (I, m); at the end of Step 1 the cosupport of (I_1, m) is empty and M(I_1) = 𝒪_{X¹}, so Steps 2 and 3 do nothing. In the assembled functor (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Assembly.lean):

• the round order of (X, I, m, ∅) is m (N(I) = I, max-ord I = m), so Step 1 unrolls to one round followed by the empty sequence (step1_of_le, step1_of_lt), the round being BO_{n,m} on (X, N(I), ∅) = (X, I, ∅) (step1Round);
• along that round, of order exactly m, the marked transform of (I, m) is the weak transform ([Kol07, Remark 67]; IsOrderSeq.markedTransformSeq_eq_weakTransformSeq), of max-ord < m at the end (clause (1) of [Kol07, Theorem 103]); so the induced marked triple has cosupp(I_1, m) = ∅, separation order 0 (Step 2 is empty, step2_of_eq_zero) and max-ord M(I_1) ≤ max-ord I_1 < m (Step 3 is empty, step3Seq_eq_nil_of_maxOrd_lt).

theorem Hironaka.BMO.step3Seq_eq_nil_of_maxOrd_lt {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) {n m : ℕ} (hT : MarkedTriple.BMOClass n m T) (h : (monomialPart T.I T.E).maxOrd < ↑m) : step3Seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

Below the mark, max-ord M(I) < m, Step 3 is the empty sequence (the last paragraph of [Kol07, 111]: "M(…) = 𝒪_{X¹} … Steps 2 and 3 do nothing"): every face of the input state has exponent sum < m (star_toState_of_maxOrd_lt through monomial_exponentAt_step3Family), so the combinatorial run is empty and its realization is nil (realize_eq_nil).

theorem Hironaka.BMO.concat_eq_nil_of_eq_nil {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} {R : S.last.BlowUpSequence} (hS : S = AlgebraicGeometry.Scheme.BlowUpSequence.nil X) (hR : R = AlgebraicGeometry.Scheme.BlowUpSequence.nil S.last) : S.concat R = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

A concatenation of two empty sequences is empty.

theorem Hironaka.BMO.functor_seq_heq {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {d d' : ℕ} (hdd : d = d') {T T' : AlgebraicGeometry.Triple k} (hTT : T = T') (hT : AlgebraicGeometry.Triple.BOClass n d T) (hT' : AlgebraicGeometry.Triple.BOClass n d' T') : ((bo d).functor k).seq T hT ≍ ((bo d').functor k).seq T' hT'

The value of BO_{n,d} on a triple depends only on the mark and the triple, not on the proof of membership in the class (proof irrelevance, through the equalities of marks and triples).

theorem Hironaka.BMO.nonmonomialTriple_eq_of_isEmpty {k : Type u} [Field k] {m : ℕ} (T : AlgebraicGeometry.Triple k) (hE : IsEmpty T.E.ι) : nonmonomialTriple { toTriple := T, m := m } = T

For the empty boundary the triple (X, N(I), E) of the round is the triple itself (the last paragraph of [Kol07, 111]: "if E = ∅ then N(I) = I").

theorem Hironaka.BMO.eq_BO_of_maxOrd {k : Type u} [Field k] [CharZero k] {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) (hE : IsEmpty T.E.ι) (hmax : T.I.maxOrd = ↑m) : (functor bo m).seq { toTriple := T, m := m } ⋯ = ((bo m).functor k).seq T hT

For E = ∅ and m = max-ord I, BMO_{n,m}(X, I, m, ∅) = BO_{n,m}(X, I, ∅) as blow-up sequences (clause (3) of [Kol07, Theorem 107]): Step 1 is the single round BO_{n,m}(X, N(I), ∅) = BO_{n,m}(X, I, ∅) (the round order is m, and after it the round order is < m); along it the marked and the birational transforms agree ([Kol07, Remark 67]), so cosupp((I_1, m)) = ∅, whence Step 2 is empty (separation order 0) and Step 3 is empty (max-ord M(I_1) ≤ max-ord I_1 < m).