Theorems 68 and 69 for the dimension-free functors over a base stage

[Kol07, Theorems 68 and 69] for dimFreeBO base m k and dimFreeBMO base m k (Hironaka.Resolution.Algebraic.Stage.DimFree), over an ARBITRARY base stage base : OrderReductionStage 0; Hironaka.Resolution.Algebraic.Stage.Theorem68 instantiates them at stage0 for BO_m and BMO_m, and the proofs of Main Theorems II and II(N), of Theorem 35 and of the embedded desingularization read the clauses from here. Every proof is one pattern:

• coherence at the maximum (dimFreeBO_seq_eq_tower, dimFreeBMO_seq_eq_tower): a triple T of the stage-n class and of the stage-T.dim class lies in the class of N := max T.dim n (Triple.boClass_mono), and tower_bo_coherent moves both values to stage N — so the dimension-free functor agrees with the tower at EVERY stage whose class contains T, and no relation between n and T.dim is needed (for X = ∅ the chosen dimension is arbitrary);
• a stage field: clause (1) is the stage functor's maxOrd_lt; the two bullets of [Kol07, 34.1] (commutesWithSmooth, of any relative dimension), [Kol07, 34.2] (commutesWithBaseChange) and the indifference to empty boundary members compare two triples, moved to the common stage max (dim T) (dim T') and read from that stage's field (BOData has no indifference field: tower_bo_indifferentToEmptyMembers is boOfBMO_indifferentToEmptyMembers at stages n + 1 and the dimension-0 lemma at stage 0);
• Claim 71.1 ([Kol07, Claim 71.1]; [Kol07, 108]: "(71.1) is the same as (107.3)"): at stage n + 1 the tower's marked functor IS BMO.functor (boOfBMO …) m and its unmarked one IS boOfBMO … m (tower_succ_bmo, tower_succ_bo, both rfl), so eq_BO_of_maxOrd (clause (3) of Theorem 107) applies; at stage 0 both values are nil (the dimension-0 lemmas).

Claim 71.2 is Hironaka.Resolution.Algebraic.Stage.ClosedEmbeddingGeneral.

Coherence at the maximum

theorem Hironaka.Stage.dimFreeBO_seq_eq_tower (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] (n : ℕ) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClassFree m T) (hT' : AlgebraicGeometry.Triple.BOClass n m T) : (dimFreeBO base m k).seq T hT = (((tower base n).bo m).functor k).seq T hT'

The dimension-free unmarked functor agrees with the tower's BO_{n, m} at every triple of the stage-n class — both stages meet at max T.dim n through tower_bo_coherent (any n ≥ dim X gives the same sequence).

theorem Hironaka.Stage.dimFreeBMO_seq_eq_tower (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] (n : ℕ) (T : MarkedTriple k) (hT : MarkedTriple.BMOClassFree m T) (hT' : MarkedTriple.BMOClass n m T) : (dimFreeBMO base m k).seq T hT = (((tower base n).bmo m).functor k).seq T hT'

The marked form: the dimension-free marked functor agrees with the tower's BMO_{n, m} at every marked triple of the stage-n class.

Clause (1) of Theorems 68 and 69

theorem Hironaka.Stage.dimFreeBO_maxOrd_lt (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).weakTransformSeq T.I (Fin.last ((dimFreeBO base m k).seq T hT).length)).maxOrd < ↑m

[Kol07, Theorem 68 (1)]: max-ord I_r < m — the stage functor's clause (1) (Theorem 103 (1)) at stage T.dim.

theorem Hironaka.Stage.dimFreeBMO_maxOrd_lt (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).markedTransformSeq T.I T.m (Fin.last ((dimFreeBMO base m k).seq T hT).length)).maxOrd < ↑m

[Kol07, Theorem 69 (1)]: max-ord I_r < m for the marked functor (Theorem 107 (1)).

Clause (2) of Theorems 68 and 69

theorem Hironaka.Stage.dimFreeBO_commutesWithSmooth (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] : (dimFreeBO base m k).CommutesWithSmooth

[Kol07, Theorem 68 (2)], functoriality for smooth morphisms [Kol07, 34.1] of ANY relative dimension: both triples of a pull-back situation T' → T lie in the class of N := max T.dim T'.dim; coherence moves both values to stage N, whose field is 34.1.

theorem Hironaka.Stage.dimFreeBO_commutesWithBaseChange (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (σ : k →+* L) : (dimFreeBO base m k).CommutesWithBaseChange (dimFreeBO base m L) σ

[Kol07, Theorem 68 (2)], change of fields [Kol07, 34.2]: the base-change triple T' over L and T over k lie in the class of N := max T.dim T'.dim; the stage-N field is 34.2.

theorem Hironaka.Stage.dimFreeBMO_commutesWithSmooth (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] : (dimFreeBMO base m k).CommutesWithSmooth

[Kol07, Theorem 69 (2)], functoriality for smooth morphisms [Kol07, 34.1], for the marked functor.

theorem Hironaka.Stage.dimFreeBMO_commutesWithBaseChange (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] {L : Type u} [Field L] [CharZero L] (σ : k →+* L) : (dimFreeBMO base m k).CommutesWithBaseChange (dimFreeBMO base m L) σ

[Kol07, Theorem 69 (2)], change of fields [Kol07, 34.2], for the marked functor.

theorem Hironaka.Stage.tower_bo_indifferentToEmptyMembers (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] (n : ℕ) : (((tower base n).bo m).functor k).IndifferentToEmptyMembers

Every stage of the tower's unmarked family is indifferent to empty boundary members — boOfBMO_indifferentToEmptyMembers at stages n + 1, and at stage 0 both values are nil (the dimension-0 lemma; BOData has no indifference field, so the base contributes nothing but its class).

theorem Hironaka.Stage.dimFreeBMO_indifferentToEmptyMembers (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] : (dimFreeBMO base m k).IndifferentToEmptyMembers

The dimension-free marked functor is indifferent to empty boundary members — the two triples share the ambient scheme, and both lie in the class of the common stage max, whose field is the indifference.

theorem Hironaka.Stage.dimFreeBO_indifferentToEmptyMembers (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] : (dimFreeBO base m k).IndifferentToEmptyMembers

The dimension-free unmarked functor is indifferent to empty boundary members, from tower_bo_indifferentToEmptyMembers at the common stage.

Claim 71.1

theorem Hironaka.Stage.tower_bmo_eq_bo_of_maxOrd (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] (n : ℕ) (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) (hE : IsEmpty T.E.ι) (hmax : T.I.maxOrd = ↑m) : (((tower base n).bmo m).functor k).seq { toTriple := T, m := m } ⋯ = (((tower base n).bo m).functor k).seq T hT

[Kol07, Claim 71.1] at every stage of the tower ([Kol07, 108]: "(71.1) is the same as (107.3)"): for E = ∅ and max-ord I = m, the marked functor at (X, I, m, ∅) equals the unmarked one at (X, I, ∅) — eq_BO_of_maxOrd at stages n + 1 (where the tower's functors ARE those of the assembly of Theorem 107, tower_succ_bmo/tower_succ_bo by rfl), and both nil at stage 0.

theorem Hironaka.Stage.dimFree_claim71_1 (base : OrderReductionStage 0) (m : ℕ) {k : Type u} [Field k] [CharZero k] (T : AlgebraicGeometry.Triple k) (hE : IsEmpty T.E.ι) (hm : 1 ≤ m) (hmax : T.I.maxOrd = ↑m) : (dimFreeBMO base m k).seq { toTriple := T, m := m } ⋯ = (dimFreeBO base m k).seq T ⋯

[Kol07, Claim 71.1], dimension-free: BMO_m(X, I, m, ∅) = BO_m(X, I, ∅) when max-ord I = m — tower_bmo_eq_bo_of_maxOrd at the stage T.dim both functors read.