Theorems 68 and 69: the functors BO_m and BMO_m

Kollár's Theorem 68 and Theorem 69 [Kol07, Theorems 68 and 69], the main technical theorems of the order-reduction part, as OBJECTS: for every mark m the smooth blow-up sequence functor BO_m of order m on the triples (X, I, E) with max-ord I ≤ m, and the marked functor BMO_m of order ≥ m on the marked triples (X, I, m, E). Both are the dimension-free functors of Hironaka.Resolution.Algebraic.Stage.DimFree over the canonical base of the tower, stage0 (Hironaka.Resolution.Algebraic.Stage.Base): BO_m(X, I, E) := BO_{dim X, m}(X, I, E) and likewise BMO_m, using the stage of the triple's own dimension. Their clauses (68.1)–(68.2), (69.1)–(69.2), Claim 71.1 and Claim 71.2 are proved in Hironaka.Resolution.Algebraic.Stage.DimFreeTheorems and Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingGeneral. These are the functors on which the principalization Hironaka.Sequence.BP (Theorem 35), the order reduction of Main Theorems II and II(N) and the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.Embedded) are built.

noncomputable def Hironaka.Stage.BO_m (m : ℕ) (k : Type u) [Field k] [CharZero k] : OrderSeqAssignment k m (AlgebraicGeometry.Triple.BOClassFree m)

BO_m, the functor of [Kol07, Theorem 68]: the dimension-free functor of the tower over the base stage stage0.

Equations

• Hironaka.Stage.BO_m m k = Hironaka.Stage.dimFreeBO Hironaka.Stage.stage0 m k

noncomputable def Hironaka.Stage.BMO_m (m : ℕ) (k : Type u) [Field k] [CharZero k] : OrderGeSeqAssignment k (MarkedTriple.BMOClassFree m)

BMO_m, the functor of [Kol07, Theorem 69]: the dimension-free marked functor of the tower over stage0.

Equations

• Hironaka.Stage.BMO_m m k = Hironaka.Stage.dimFreeBMO Hironaka.Stage.stage0 m k