Marked order reduction as data

[Kol07, Theorem 107] as the structure BMOData n m: the functor BMO_{n,m} over every field of characteristic zero (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Assembly.lean), clause (1), max-ord I_r < m (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Clause1.lean), clause (2) for smooth morphisms (Hironaka/Resolution/Algebraic/MarkedOrderReduction/Smooth.lean, both clauses of [Kol07, 34.1]) and for change of fields (Hironaka/Resolution/Algebraic/MarkedOrderReduction/BaseChangeLoop.lean), and the indifference to empty boundary members, all under the hypothesis hboind that every input functor bo d, order reduction for ideals in dimension n at the order d, is indifferent to empty boundary members; that hypothesis is discharged for the order-reduction data in Hironaka/Resolution/Algebraic/OrderReduction/EmptyIndifferentGlobal.lean. The existence statement exists_data records that such data exist with the assembled functor as their functor. Clause (3) of Theorem 107 is Hironaka/Resolution/Algebraic/MarkedOrderReduction/Clause3.lean; the readings of the fields are in Hironaka/Resolution/Algebraic/MarkedOrderReduction/Data.lean. The data feed the induction on the dimension in Hironaka/Resolution/Algebraic/Stage/.

noncomputable def Hironaka.BMO.data {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) : BMOData n m

[Kol07, Theorem 107] as data: BMO_{n,m} as a BMOData n m, the functor of the assembly over every field of characteristic zero, clause (1) (maxOrd_lt), clause (2) (commutesWithSmooth under hboind, and commutesWithBaseChange), and the indifference to empty boundary members (under hboind).

Equations

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

theorem Hironaka.BMO.exists_data {n : ℕ} (bo : (d : ℕ) → BOData n d) {m : ℕ} (hboind : ∀ (d : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], ((bo d).functor k).IndifferentToEmptyMembers) : ∃ (D : BMOData n m), ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], D.functor k = functor bo m

There are marked order-reduction data BMOData n m whose functor over every field of characteristic zero is the assembled BMO_{n,m}, under the indifference hboind of every input functor bo d to empty boundary members: BMO.data bo hboind.