Coherence and cross-dimensional functoriality of the tower

Kollár's induction [Kol07, 70] produces one pair of functors per dimension bound; the tower tower base n : OrderReductionStage n (Hironaka.Resolution.Algebraic.Stage.Tower) is that family. Coherence: for n' ≤ n, BO_{n,m} and BO_{n',m} of the tower agree on every triple of the stage-n' class, and likewise BMO — the fact that lets Hironaka.Resolution.Algebraic.Stage.DimFree define the single functors of Kol07, Theorems 68 and 69 without reference to n. It is ONE simultaneous induction on n, both halves together: at n = 0 the two stages coincide; at n + 1 with n' ≤ n, the BO half is the construction of Theorem 103 at stages n + 1 and n' fed the amalgams of the stage-n and stage-(n' − 1) marked functors, which agree on the marked triples of dimension ≤ n' − 1 by the BMO half of the induction hypothesis — the congruence Hironaka.BO.data_congr (Hironaka.Resolution.Algebraic.Stage.Congr); at n' = 0 both values are empty (the dimension-0 lemmas); the BMO half is the construction of Theorem 107 fed the two BO families just shown to agree at every order — the congruence Hironaka.BMO.data_congr (Hironaka.Resolution.Algebraic.Stage.CongrBMO); at n' = n + 1 there is nothing to show. Cross-dimensional functoriality: the two bullets of [Kol07, 34.1] for g : Y → X smooth with dim Y ≤ n and dim X ≤ n' ≤ n, the value at Y taken at stage n and the value at X at stage n' — coherence moves the stage-n' value at X to stage n, and the stage-n field (commutesWithSmooth) is 34.1 at that stage.

theorem Hironaka.Stage.tower_coherent_aux (base : OrderReductionStage 0) (n n' : ℕ) : n' ≤ n → (∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : AlgebraicGeometry.Triple k) (hT : AlgebraicGeometry.Triple.BOClass n m T) (hT' : AlgebraicGeometry.Triple.BOClass n' m T), (((tower base n).bo m).functor k).seq T hT = (((tower base n').bo m).functor k).seq T hT') ∧ ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : MarkedTriple k) (hT : MarkedTriple.BMOClass n m T) (hT' : MarkedTriple.BMOClass n' m T), (((tower base n).bmo m).functor k).seq T hT = (((tower base n').bmo m).functor k).seq T hT'

The simultaneous induction behind the coherence of the tower: for every n' ≤ n, both halves of coherence at (n, n') — the BO half from the BMO half at (n − 1, n' − 1) through the amalgams (BO.data_congr; dimension 0 at n' = 0), the BMO half from the BO half at (n, n') at every order (BMO.data_congr).

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

Coherence of the unmarked family: for n' ≤ n, BO_{n,m} and BO_{n',m} of the tower agree on every triple of the stage-n' class (Kollár's functors of [Kol07, Theorem 103] are indexed by dim X = n; the tower's stage n is defined on dimension ≤ n, and its values do not depend on the bound).

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

Coherence of the marked family: for n' ≤ n, BMO_{n,m} and BMO_{n',m} of the tower agree on every marked triple of the stage-n' class ([Kol07, Theorem 107]).

theorem Hironaka.Stage.tower_bo_pullback_of_surjective (base : OrderReductionStage 0) {n n' : ℕ} (m : ℕ) {k : Type u} [Field k] [CharZero k] (hle : n' ≤ n) (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (hs : Function.Surjective ⇑g) (hpb : T'.IsPullbackOf T g) (hT : AlgebraicGeometry.Triple.BOClass n' m T) (hT' : AlgebraicGeometry.Triple.BOClass n m T') : (((tower base n).bo m).functor k).seq T' hT' = ((((tower base n').bo m).functor k).seq T hT).pullback g

The first bullet of [Kol07, 34.1] across the stages: for a smooth SURJECTION g : Y → X with dim Y ≤ n, dim X ≤ n' ≤ n, the stage-n value of BO at Y is the pull-back of the stage-n' value at X — coherence moves the value at X to stage n, where it is the stage-n field.

theorem Hironaka.Stage.tower_bo_pullback_eraseEmpty (base : OrderReductionStage 0) {n n' : ℕ} (m : ℕ) {k : Type u} [Field k] [CharZero k] (hle : n' ≤ n) (T T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (hpb : T'.IsPullbackOf T g) (hT : AlgebraicGeometry.Triple.BOClass n' m T) (hT' : AlgebraicGeometry.Triple.BOClass n m T') : (((tower base n).bo m).functor k).seq T' hT' = (((((tower base n').bo m).functor k).seq T hT).pullback g).eraseEmpty

The second bullet of [Kol07, 34.1] across the stages: for a smooth g : Y → X with dim Y ≤ n, dim X ≤ n' ≤ n, the stage-n value of BO at Y is the pull-back of the stage-n' value at X with its empty blow-ups deleted.

theorem Hironaka.Stage.tower_bmo_pullback_of_surjective (base : OrderReductionStage 0) {n n' : ℕ} (m : ℕ) {k : Type u} [Field k] [CharZero k] (hle : n' ≤ n) (T T' : MarkedTriple k) (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (hs : Function.Surjective ⇑g) (hpb : T'.IsPullbackOf T g) (hT : MarkedTriple.BMOClass n' m T) (hT' : MarkedTriple.BMOClass n m T') : (((tower base n).bmo m).functor k).seq T' hT' = ((((tower base n').bmo m).functor k).seq T hT).pullback g

The first bullet of [Kol07, 34.1] across the stages, marked: the surjective form for BMO.

theorem Hironaka.Stage.tower_bmo_pullback_eraseEmpty (base : OrderReductionStage 0) {n n' : ℕ} (m : ℕ) {k : Type u} [Field k] [CharZero k] (hle : n' ≤ n) (T T' : MarkedTriple k) (g : T'.X.left ⟶ T.X.left) [AlgebraicGeometry.Smooth g] (hpb : T'.IsPullbackOf T g) (hT : MarkedTriple.BMOClass n' m T) (hT' : MarkedTriple.BMOClass n m T') : (((tower base n).bmo m).functor k).seq T' hT' = (((((tower base n').bmo m).functor k).seq T hT).pullback g).eraseEmpty

The second bullet of [Kol07, 34.1] across the stages, marked: the form with the empty blow-ups deleted, for BMO.