Order reduction as data: BO.dataOfBD and BO.data

[Kol07, Theorem 103] assumes order reduction for marked ideals ([Kol07, Theorem 69]) in dimensions < n and produces, for every mark m, the functor BO_{n,m} with its clauses (1)–(2). The structure BOData n m bundles the functor over every field of characteristic zero with those two clauses; this module assembles it twice:

• BO.dataOfBD bd hind, from boundary-clearing data bd : ∀ m j, BDData n m j of [Kol07, Lemma 102] at every mark and position, indifferent to empty boundary members (hind): its functor is BO.functor n m bd and its clause fields are the theorems of Hironaka/Resolution/Algebraic/OrderReduction/Step3Clauses.lean. This is the form used by the recursion on the dimension in Hironaka/Resolution/Algebraic/Stage/.
• BO.data Dom B hDom hB hsm hbc hBind, from Theorem 103's own hypothesis, the marked order-reduction functor B in dimensions ≤ n − 1 with its clauses: the boundary-clearing data are Hironaka.BD.bdData at every mark and position, and their indifference is Hironaka.BD.bdData_indifferentToEmptyMembers, from the indifference hBind of the input.

The existence statements exists_dataOfBD and exists_data hold by rfl on these definitions.

noncomputable def Hironaka.BO.dataOfBD (n m : ℕ) (bd : (m j : ℕ) → BDData n m j) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) : BOData n m

Clauses (1)–(2) of [Kol07, Theorem 103] as data, from boundary-clearing data at every mark and position: the functor is BO.functor n m bd over each field of characteristic zero, clause (1) is functor_maxOrd_lt, and clause (2) is functor_commutesWithSmooth (under the indifference hind) together with functor_commutesWithBaseChange.

Equations

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

theorem Hironaka.BO.exists_dataOfBD (n m : ℕ) (bd : (m j : ℕ) → BDData n m j) (hind : ∀ (m : ℕ), BDFamily.IndifferentToEmptyMembers (bd m)) : ∃ (D : BOData n m), ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], D.functor k = functor n m bd

There are order-reduction data whose functor is BO.functor n m bd: dataOfBD.

noncomputable def Hironaka.BO.data (n m : ℕ) (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (hBind : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).IndifferentToEmptyMembers) : BOData n m

Clauses (1)–(2) of [Kol07, Theorem 103] as data from the inductive hypothesis ("assume that (69) holds in dimensions < n"): dataOfBD at the boundary-clearing data Hironaka.BD.bdData built from the marked functor B, with the indifference discharged by Hironaka.BD.bdData_indifferentToEmptyMembers from hBind.

Equations

• Hironaka.BO.data n m Dom B hDom hB hsm hbc hBind = Hironaka.BO.dataOfBD n m (fun (m j : ℕ) => Hironaka.BD.bdData n m j Dom B ⋯ hB hsm hbc) ⋯

theorem Hironaka.BO.exists_data (n m : ℕ) (Dom : (k : Type u) → [inst : Field k] → [CharZero k] → MarkedTriple k → Prop) (B : (k : Type u) → [inst : Field k] → [inst_1 : CharZero k] → OrderGeSeqAssignment k (Dom k)) (hDom : ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k), T'.HasDimLE (n - 1) → T'.m = IsLocalRing.tuningParam m → Dom k T') (hB : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T' : MarkedTriple k) (hT' : Dom k T'), ((B k).endTriple T' hT').I.maxOrd < ↑T'.m) (hsm : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).CommutesWithSmooth) (hbc : ∀ (k L : Type u) [inst : Field k] [inst_1 : CharZero k] [inst_2 : Field L] [inst_3 : CharZero L] (σ : k →+* L), (B k).CommutesWithBaseChange (B L) σ) (hBind : ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], (B k).IndifferentToEmptyMembers) : ∃ (D : BOData n m), ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], D.functor k = functor n m fun (m j : ℕ) => BD.bdData n m j Dom B ⋯ hB hsm hbc

There are order-reduction data whose functor is BO.functor at the boundary-clearing data built from B: data.