The stage package and the recursion on the dimension bound

[Kol07, 70]: "(69) in dimensions ≤ n − 1 ⇒ (68) in dimension n ⇒ (69) in dimension n", a spiralling induction (the diagram of [Kol07, 49]). In the library the two theorems are data — BOData n m (Theorem 68 in dimension ≤ n, proved as Theorem 103) and BMOData n m (Theorem 69, proved as Theorem 107) — for EVERY mark m at once, the marks needed being data-dependent, and the induction is a plain recursion on the dimension bound n:

• OrderReductionStage n — the stage package: a BOData n m and a BMOData n m for every m, both on triples of dimension ≤ n (every irreducible component of dimension ≤ n, the reading of Kollár's "dim X = n" under which disjoint unions and restriction to E^j stay in the class);
• succ S — the step n → n + 1: BO.data (n+1) m (Theorem 103) fed with the AMALGAM of S.bmo (Hironaka.Resolution.Algebraic.Stage.Amalgam: the inductive hypothesis is exactly the stage-n marked family), then BMO.data (Theorem 107) fed with the stage-(n+1) bo — its hypothesis hboind (indifference to empty boundary members) discharged by BO.data_indifferentToEmptyMembers;
• tower base n — the recursion from a base stage base : OrderReductionStage 0 (stage0 of Hironaka.Resolution.Algebraic.Stage.Base), by Nat.rec.

The family produced is indexed by (n, m); the single functors of Theorems 68 and 69 are those of Hironaka.Resolution.Algebraic.Stage.DimFree and Hironaka.Resolution.Algebraic.Stage.Theorem68.

structure Hironaka.OrderReductionStage (n : ℕ) : Type (u + 1)

The stage-n package of the induction of [Kol07, 70]: the data BO_{n,m} of Theorem 103 and BMO_{n,m} of Theorem 107 for every mark m, on triples of dimension ≤ n.

• bo (m : ℕ) : BOData n m

  Theorem 103 (BOData) at every mark.

• bmo (m : ℕ) : BMOData n m

  Theorem 107 (BMOData) at every mark.

def Hironaka.Stage.amalgamDom (n : ℕ) (k : Type u) [Field k] [CharZero k] : MarkedTriple k → Prop

The amalgam's class as a domain Dom : ∀ k, MarkedTriple k → Prop over every field, the shape of the inductive input of bdData.

Equations

• Hironaka.Stage.amalgamDom n x✝² T = Hironaka.MarkedTriple.AmalgamClass n T

noncomputable def Hironaka.Stage.boOfBMO {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (m : ℕ) : BOData (n + 1) m

BO_{n+1,m} from the stage-n marked family ([Kol07, 70.1]: "(69) in dimensions ≤ n − 1 ⇒ (68) in dimension n", Theorem 103): BO.data at the amalgam of bmo, with the transports of Hironaka.Resolution.Algebraic.Stage.Amalgam as the hypotheses on the inductive input.

Equations

• Hironaka.Stage.boOfBMO bmo m = Hironaka.BO.data (n + 1) m (Hironaka.Stage.amalgamDom n) (fun (k : Type ?u.1) (x : Field k) (x_1 : CharZero k) => Hironaka.Stage.amalgam bmo k) ⋯ ⋯ ⋯ ⋯ ⋯

theorem Hironaka.Stage.boOfBMO_indifferentToEmptyMembers {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (d : ℕ) (k : Type u) [Field k] [CharZero k] : ((boOfBMO bmo d).functor k).IndifferentToEmptyMembers

Every BO_{n+1,d} of the step is indifferent to empty boundary members (BO.data_indifferentToEmptyMembers).

noncomputable def Hironaka.Stage.succOfBMO {n : ℕ} (bmo : (m : ℕ) → BMOData n m) : OrderReductionStage (n + 1)

The stage n + 1 from a stage-n marked family ([Kol07, 70.1–70.2]): bo is BO_{n+1,·} from the family (boOfBMO), bmo is Theorem 107's BMO.data from that bo, its hypothesis hboind discharged by boOfBMO_indifferentToEmptyMembers. Its TYPE says that the inductive hypothesis used is the marked family and nothing else.

Equations

• Hironaka.Stage.succOfBMO bmo = { bo := Hironaka.Stage.boOfBMO bmo, bmo := fun (m : ℕ) => Hironaka.BMO.data (Hironaka.Stage.boOfBMO bmo) ⋯ }

noncomputable def Hironaka.Stage.succ {n : ℕ} (S : OrderReductionStage n) : OrderReductionStage (n + 1)

The step n → n + 1 of the recursion ([Kol07, 70.1–70.2]): succOfBMO at the stage's marked family; the stage's bo is not consulted.

Equations

• Hironaka.Stage.succ S = Hironaka.Stage.succOfBMO S.bmo

noncomputable def Hironaka.Stage.tower (base : OrderReductionStage 0) (n : ℕ) : OrderReductionStage n

The tower of stages from a base stage ([Kol07, 70]: "we prove (68) and (69) together"; the diagram of [Kol07, 49]), by recursion on the dimension bound.

Equations

• Hironaka.Stage.tower base 0 = base
• Hironaka.Stage.tower base n.succ = Hironaka.Stage.succ (Hironaka.Stage.tower base n)

Unfolding lemmas and existential forms

theorem Hironaka.Stage.tower_zero (base : OrderReductionStage 0) : tower base 0 = base

The tower at stage 0 is the base.

theorem Hironaka.Stage.tower_succ (base : OrderReductionStage 0) (n : ℕ) : tower base (n + 1) = succ (tower base n)

The tower at stage n + 1 is the step applied to the tower at stage n.

theorem Hironaka.Stage.tower_succ_bo (base : OrderReductionStage 0) (n m : ℕ) : (tower base (n + 1)).bo m = boOfBMO (tower base n).bmo m

The unmarked family of the tower at stage n + 1 is Theorem 103's data at the amalgam of the stage-n marked family.

theorem Hironaka.Stage.tower_succ_bmo (base : OrderReductionStage 0) (n m : ℕ) (k : Type u) [Field k] [CharZero k] : ((tower base (n + 1)).bmo m).functor k = BMO.functor (boOfBMO (tower base n).bmo) m

The marked family of the tower at stage n + 1 is Theorem 107's functor at the stage-(n + 1) unmarked family.

theorem Hironaka.Stage.succ_eq_succOfBMO {n : ℕ} (S : OrderReductionStage n) : succ S = succOfBMO S.bmo

The step is succOfBMO at the stage's marked family.

theorem Hironaka.Stage.succ_bo {n : ℕ} (S : OrderReductionStage n) : (succ S).bo = boOfBMO S.bmo

The unmarked family of the step is Theorem 103's data at the amalgam of the marked family below.

theorem Hironaka.Stage.boOfBMO_functor {n : ℕ} (bmo : (m : ℕ) → BMOData n m) (m : ℕ) (k : Type u) [Field k] [CharZero k] : (boOfBMO bmo m).functor k = BO.functor (n + 1) m fun (m j : ℕ) => BD.bdData (n + 1) m j (amalgamDom n) (fun (k : Type u) (x : Field k) (x_1 : CharZero k) => amalgam bmo k) ⋯ ⋯ ⋯ ⋯

The functor of BO_{n+1,m} of the step is BO.functor at bdData fed with the amalgam and its transports.

theorem Hironaka.Stage.succ_bmo {n : ℕ} (S : OrderReductionStage n) (m : ℕ) (k : Type u) [Field k] [CharZero k] : ((succ S).bmo m).functor k = BMO.functor (succ S).bo m

The marked family of the step is Theorem 107's functor at the step's unmarked family ([Kol07, 70.2]).

theorem Hironaka.Stage.succ_congr {n : ℕ} (S S' : OrderReductionStage n) (h : S.bmo = S'.bmo) : succ S = succ S'

The step depends on the stage below only through its marked family (the inductive hypothesis of [Kol07, Lemma 102 and Theorem 103]).

theorem Hironaka.Stage.exists_succ {n : ℕ} (S : OrderReductionStage n) : ∃ (S' : OrderReductionStage (n + 1)), S'.bo = boOfBMO S.bmo ∧ ∀ (m : ℕ) (k : Type u) [inst : Field k] [inst_1 : CharZero k], (S'.bmo m).functor k = BMO.functor (boOfBMO S.bmo) m

The existential form of the step.

theorem Hironaka.Stage.exists_tower (base : OrderReductionStage 0) : ∃ (st : (n : ℕ) → OrderReductionStage n), st 0 = base ∧ ∀ (n : ℕ), st (n + 1) = succ (st n)

The existential form of the recursion ([Kol07, 70]).