The dimension-free functors of Theorems 68 and 69

[Kol07, Theorem 68]: for every m there is a smooth blow-up sequence functor BO_m of order m, "defined on triples (X, I, E) with max-ord I ≤ m"; [Kol07, Theorem 69] is the marked counterpart, "defined on triples (X, I, m, E)". Kollár's Theorems 103 and 107 carry a dimension bound: BOData n m and BMOData n m live on triples of dimension ≤ n, and the tower Hironaka.Stage.tower base n produces both for every n from a base stage. The bound is removed by BO_m(X, I, E) := BO_{dim X, m}(X, I, E), the stage of the triple's own dimension; by the coherence of the tower any n ≥ dim X gives the same sequence.

This module holds that construction over an arbitrary base stage base : OrderReductionStage 0 (the tower's parameter); Hironaka.Resolution.Algebraic.Stage.Theorem68 instantiates it at stage0 to define BO_m and BMO_m.

• the dimension of a triple is AlgebraicGeometry.Triple.dim T (Hironaka.Resolution.Algebraic.Stage.Dim), the relative dimension read off the triple's own equidimensionality field T.smoothOfRelativeDimension ([Kol07, Notation 64 (1)]), with T.HasDimLE T.dim. For X = ∅ every n qualifies and the choice is arbitrary; coherence makes the functors' values independent of it.
• Triple.BOClassFree m, MarkedTriple.BMOClassFree m — the domains of Theorems 68 and 69: the stage classes BOClass n m, BMOClass n m without the dimension bound.
• dimFreeBO base m k : OrderSeqFunctor k m (Triple.BOClassFree m) — the value at T is the value of the tower's BO_{T.dim, m} at T; dimFreeBMO base m k likewise.

@[reducible, inline]

abbrev AlgebraicGeometry.Triple.BOClassFree {k : Type u} [Field k] (m : ℕ) (T : Triple k) : Prop

The domain of BO_m ([Kol07, Theorem 68]: "triples (X, I, E) with max-ord I ≤ m"): the stage class BOClass n m without its dimension bound (1 ≤ m: Kollár's marks are ≥ 1). Reducible, as BOClass is.

Equations

• AlgebraicGeometry.Triple.BOClassFree m T = (1 ≤ m ∧ T.I.maxOrd ≤ ↑m)

theorem AlgebraicGeometry.Triple.boClass_of_boClassFree {k : Type u} [Field k] {m : ℕ} {T : Triple k} (hT : BOClassFree m T) : BOClass T.dim m T

A triple of Theorem 68's domain lies in the stage class of its own dimension.

@[reducible, inline]

abbrev Hironaka.MarkedTriple.BMOClassFree {k : Type u} [Field k] (m : ℕ) (T : MarkedTriple k) : Prop

The domain of BMO_m ([Kol07, Theorem 69]: "defined on triples (X, I, m, E)"): the stage class BMOClass n m without its dimension bound: the marked triples of mark m ≥ 1. Reducible, as BMOClass is.

Equations

• Hironaka.MarkedTriple.BMOClassFree m T = (1 ≤ m ∧ T.m = m)

theorem Hironaka.MarkedTriple.bmoClass_of_bmoClassFree {k : Type u} [Field k] {m : ℕ} {T : MarkedTriple k} (hT : BMOClassFree m T) : BMOClass T.dim m T

A marked triple of Theorem 69's domain lies in the stage class of its own dimension.

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

The dimension-free functor of [Kol07, Theorem 68] over a base stage: its value at a triple T with max-ord I ≤ m is the value of the tower's BO_{T.dim, m} at T (BO_m(X, I, E) := BO_{dim X, m}(X, I, E)); the order-m and no-empty-blow-up clauses are the stage functor's.

Equations

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

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

The dimension-free functor of [Kol07, Theorem 69] over a base stage, on the marked triples of mark m (BMO_m := BMO_{dim X, m}).

Equations

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

theorem Hironaka.Stage.dimFreeBO_seq (base : OrderReductionStage 0) (m : ℕ) (k : Type u) [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClassFree m T) : (dimFreeBO base m k).seq T hT = (((tower base T.dim).bo m).functor k).seq T ⋯

The value of dimFreeBO unfolded: the stage-T.dim value (by rfl).

theorem Hironaka.Stage.dimFreeBMO_seq (base : OrderReductionStage 0) (m : ℕ) (k : Type u) [Field k] [CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.BMOClassFree m T) : (dimFreeBMO base m k).seq T hT = (((tower base T.dim).bmo m).functor k).seq T ⋯

The value of dimFreeBMO unfolded: the stage-T.dim value.