Theorem 103 as the first reduction step

The order-reduction tower on the compatible-family structures (Stage/Family.lean) takes the two reduction steps of [Kol07, 70] as parameters. This module supplies the first one, order reduction for ideals from order reduction for marked ideals one dimension down ([Kol07, Theorem 103]), and the tower along it:

• theorem103FamStar 𝕜 : BOanFamStep 𝕜 — the construction BO.BOanFamOfInput of BOanFamOfInput.lean, which assembles the order-reduction family in dimension n from the marked families in dimension n - 1 following the three steps of the proof of Theorem 103, taken in dimension n + 1 (so that the input dimension (n + 1) - 1 = n holds by definition);
• orderReductionTowerAnFamStarOf 𝕜 h107 — the tower along theorem103FamStar 𝕜 and an arbitrary second reduction step h107 : BMOanFamStep 𝕜.

The second reduction step is constructed in Stage/InstancesFamTheorem107.lean; the tower at both, Stage/Concrete.lean, provides the order-reduction functors used by the analytic main theorems. Stage/AllNFam.lean reads the families in every dimension off the tower along theorem103FamStar and an arbitrary second step.

noncomputable def Hironaka.Manifold.theorem103FamStar (𝕜 : Type) [RCLike 𝕜] : BOanFamStep 𝕜

Order reduction for ideals from order reduction for marked ideals one dimension down ([Kol07, Theorem 103]), as the first reduction step of the tower on the compatible-family structures: BO.BOanFamOfInput in dimension n + 1.

Equations

• Hironaka.Manifold.theorem103FamStar 𝕜 = { bo := fun (n : ℕ) (bmo : (s : ℕ) → Hironaka.Manifold.BMOanFam 𝕜 n s) (m : ℕ) => Hironaka.Manifold.BO.BOanFamOfInput 𝕜 (n + 1) bmo m }

noncomputable def Hironaka.Manifold.orderReductionTowerAnFamStarOf (𝕜 : Type) [RCLike 𝕜] (h107 : BMOanFamStep 𝕜) (n : ℕ) : OrderReductionStageAnFam 𝕜 n

The order-reduction tower on the compatible-family structures along Theorem 103 (theorem103FamStar) and a given second reduction step h107.

Equations

• Hironaka.Manifold.orderReductionTowerAnFamStarOf 𝕜 h107 = Hironaka.Manifold.orderReductionTowerAnFam (Hironaka.Manifold.theorem103FamStar 𝕜) h107

theorem Hironaka.Manifold.orderReductionTowerAnFamStarOf_eq (𝕜 : Type) [RCLike 𝕜] (h107 : BMOanFamStep 𝕜) : orderReductionTowerAnFamStarOf 𝕜 h107 = orderReductionTowerAnFam (theorem103FamStar 𝕜) h107

The tower along theorem103FamStar unfolds to orderReductionTowerAnFam at that step.