The data of marked order reduction: reading the fields

The fields of BMOData n m, read the way Kollár prints [Kol07, Theorem 107] and the way the later constructions use them.

• bmoClass_iff: the domain unfolds (Iff.rfl, the class is an abbrev).
• BMOData.ord_markedTransformSeq_lt: clause (1) pointwise, ord_x I_r ≤ max-ord I_r < m.
• BMOData.markedCosupp_eq_empty: clause (1) as the proof of Theorem 107 reaches it, cosupp(I_r, m) = ∅ ([Kol07, 111]): no point has ord_x I_r ≥ m.
• BMOData.maxOrd_endTriple_lt: clause (1) in the form the boundary-clearing functor of [Kol07, Lemma 102] and the order-reduction data BO.data take: the end triple's ideal is the last marked transform by rfl, and the class fixes the mark, T.m = m.
• BMOData.seq_append_top: the indifference field along the order embedding i ↦ toLex (inl i) of E.ι into (E.append ⊤).ι = E.ι ⊕ₗ PUnit ([Kol07, 32]; the form needed for clause (3) of Lemma 102): the members are matched along the embedding and the one index outside its range, inr (), carries the unit ideal; the triple with the appended member is T with E := E.append ⊤ (normal crossings by isSnc_append_top), and the field's other triple is T itself by structure eta.

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

The domain of BMO_{n,m} unfolds: 1 ≤ m, dim X ≤ n and T.m = m.

theorem Hironaka.BMOData.ord_markedTransformSeq_lt {k : Type u} [Field k] [CharZero k] {n m : ℕ} (B : BMOData n m) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (x : ↥(((B.functor k).seq T hT).stage (Fin.last ((B.functor k).seq T hT).length))) : (((B.functor k).seq T hT).markedTransformSeq T.I T.m (Fin.last ((B.functor k).seq T hT).length)).ord x < ↑m

Clause (1) of [Kol07, Theorem 107] pointwise, through ord_x I_r ≤ max-ord I_r.

theorem Hironaka.BMOData.markedCosupp_eq_empty {k : Type u} [Field k] [CharZero k] {n m : ℕ} (B : BMOData n m) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) : {x : ↥(((B.functor k).seq T hT).stage (Fin.last ((B.functor k).seq T hT).length)) | ↑m ≤ (((B.functor k).seq T hT).markedTransformSeq T.I T.m (Fin.last ((B.functor k).seq T hT).length)).ord x} = ∅

Clause (1) of [Kol07, Theorem 107] as the emptiness of the cosupport, cosupp(I_r, m) = ∅ (the form reached at the end of [Kol07, 111]).

theorem Hironaka.BMOData.maxOrd_endTriple_lt {k : Type u} [Field k] [CharZero k] {n m : ℕ} (B : BMOData n m) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) : ((B.functor k).endTriple T hT).I.maxOrd < ↑T.m

Clause (1) of [Kol07, Theorem 107] for the end triple: its ideal has max-ord < T.m. The end triple's ideal is the last marked transform by rfl (induced_I), and the class fixes T.m = m.

theorem Hironaka.BMOData.seq_append_top {k : Type u} [Field k] [CharZero k] {n m : ℕ} (B : BMOData n m) (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n m { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := T.E.append ⊤, isSnc := ⋯, m := T.m }) : (B.functor k).seq T hT = (B.functor k).seq { X := T.X, smoothOfRelativeDimension := ⋯, I := T.I, isNonzeroEverywhere := ⋯, E := T.E.append ⊤, isSnc := ⋯, m := T.m } hT'

The indifference field in the appended-member form ([Kol07, 32]; the form needed for clause (3) of [Kol07, Lemma 102]): the value on T with the unit ideal appended to its boundary is the value on T. The embedding is i ↦ toLex (inl i); the index inr () outside its range carries ⊤.