The functor BMO_{n,m} assembled #
[Kol07, Theorem 107] asserts, assuming order reduction for ideals in dimensions ≤ n, a smooth
blow-up sequence functor BMO_{n,m} on marked triples (X, I, m, E) with dim X = n such that
(1) max-ord I_r < m at the end, (2) BMO_{n,m} commutes with smooth morphisms and with change of
fields, and (3) BMO_{n,m}(X, I, m, ∅) = BO_{n,m}(X, I, ∅) when m = max-ord I. Its proof
([Kol07, 111]) is the concatenation of three steps, each run on the marked triple induced at the
end of the previous one: Step 1 reduces max-ord N(I) below m
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step1NonmonomialPart.lean, step1), Step 2
separates cosupp(I, m) from cosupp N(I)
(Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step2Separation.lean, step2), and Step 3
reduces the order of the monomial part M(I) below m (the geometric Step 3 of
Hironaka/Resolution/Algebraic/Monomial/Geometric/, run on X for (M(I), m, E);
Hironaka/Resolution/Algebraic/MarkedOrderReduction/Step3Input.lean). Empty blow-ups are to be
deleted ([Kol07, 32]); none occur, each step being without empty blow-ups, so the concatenation is
the functor's value as it stands.
afterStep1 bo T hT,afterStep2 bo T hT: the marked triples induced at the ends of Steps 1 and 2 (MarkedTriple.induced), again ofBMOClass n m(MarkedTriple.bmoClass_induced).bmoSeq bo T hT:BMO_{n,m}(X, I, m, E), Step 1, then Step 2 ofafterStep1, then Step 3 ofafterStep2(concat); a smooth blow-up sequence of order≥ mfor(X, I, m, E)(bmoSeq_isOrderGeSeq) without empty blow-ups (bmoSeq_noEmptyCenters;eraseEmpty_bmoSeq: the deletion of [Kol07, 32] is the identity).functor bo: the functorBMO_{n,m}on the classBMOClass n m, anOrderGeSeqFunctor(the sequence, the order condition of [Kol07, Definition 66], no empty blow-ups).
The input is bo : ∀ d, BOData n d, order reduction for ideals in dimension n at every order,
since the orders that Steps 1–2 call are not bounded in terms of m. Clause (1)
(BMO.maxOrd_lt), clause (2) (BMO.commutesWithSmooth, BMO.commutesWithBaseChange, with
BMO.indifferentToEmptyMembers) and clause (3) (BMO.eq_BO_of_maxOrd) are the theorems of
Clause1.lean, Smooth.lean, BaseChangeLoop.lean and Clause3.lean; the data
BMO.data : BMOData n m are assembled from them in Theorem107.lean.
The marked triple induced at the end of Step 1 ([Kol07, 111]: "instead of
(X^1, (Π_1)^{-1}_*(I, m), (Π_1)^{-1}_{tot}(E)), write (X, I, m, E)").
Equations
- Hironaka.BMO.afterStep1 bo T hT = T.induced ↑(Hironaka.BMO.step1 bo T hT) ⋯ (Fin.last (↑(Hironaka.BMO.step1 bo T hT)).length)
Instances For
The end of Step 1 is again a marked triple of BMOClass n m
(MarkedTriple.bmoClass_induced).
After Step 1, max-ord N(I) < m ([Kol07, 111]: "we may assume that max-ord N(I) < m";
roundOrder_induced_step1_lt read on the induced triple).
The marked triple induced at the end of Step 2 of afterStep1, with
cosupp(I, m) ∩ cosupp N(I) = ∅ ([Kol07, 111, Step 2]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The end of Step 2 is again a marked triple of BMOClass n m.
After Step 2 the separation order is 0 ([Kol07, 111, Step 2]:
"cosupp(I, m) ∩ cosupp N(I) = ∅"; sepOrder_induced_step2_eq_zero read on the induced triple).
The smooth blow-up sequence BMO_{n,m}(X, I, m, E) ([Kol07, Theorem 107] and
[Kol07, 111]): Step 1, then Step 2 of the induced marked triple, then the geometric Step 3 (on X
for (M(I), m, E)) of the induced marked triple, concatenated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
BMO_{n,m}(X, I, m, E) is a smooth blow-up sequence of order ≥ m for (X, I, m, E)
(conditions (2′)–(4′) of [Kol07, Definition 66]): each step is one for the marked triple induced
at the end of the previous step, and the order condition concatenates (isOrderGeSeq_concat).
BMO_{n,m}(X, I, m, E) contains no empty blow-up ([Kol07, 32]): none of the three steps
does.
The deletion of empty blow-ups ([Kol07, 32]) leaves BMO_{n,m}(X, I, m, E) unchanged: there
are none (eraseEmpty_eq_self_iff).
The functor BMO_{n,m} of [Kol07, Theorem 107] on the class BMOClass n m: the sequence
bmoSeq, of order ≥ m for its marked triple, without empty blow-ups (OrderGeSeqFunctor).
Clauses (1)–(3) are the theorems BMO.maxOrd_lt, BMO.commutesWithSmooth,
BMO.commutesWithBaseChange, BMO.indifferentToEmptyMembers and BMO.eq_BO_of_maxOrd. The mark
m is explicit, since it is not determined by the input bo: BMO.functor m bo.
Equations
- Hironaka.BMO.functor bo m = { seq := fun (T : Hironaka.MarkedTriple k) (hT : Hironaka.MarkedTriple.BMOClass n m T) => Hironaka.BMO.bmoSeq bo T hT, isOrderGeSeq := ⋯, noEmptyCenters := ⋯ }
Instances For
The value of the functor BMO_{n,m} is the assembled sequence.