The order-reduction tower on the compatible-family structures

The recursion on the dimension of [Kol07, 70], stated over arbitrary families of structures in Stage/Generic.lean, instantiated at the compatible-family structures BOanFam 𝕜 n m and BMOanFam 𝕜 n m of Functor/Family.lean. These are the order-reduction functors of [Kol07, Theorem 103] and [Kol07, Theorem 107] in the form suited to non-compact analytic manifolds ([Wlo09, Theorem 2.0.3 (1), (4)]): the value on a triple is a finite blow-up sequence on every relatively compact open subset, the sequence on a smaller open being the restriction of the sequence on a larger one once empty blow-ups are deleted.

• OrderReductionStageAnFam 𝕜 n, BOanFamStep 𝕜, BMOanFamStep 𝕜 — the stage and the two reduction steps at the compatible-family structures (abbreviations of the generic ones);
• boZeroAnFam m, bmoZeroAnFam m, stage0AnFam — the base stage in dimension 0 ([Kol07, 70]: everything is resolved without blow-ups), on the trivial family functor (Functor/FamilyNil.lean): the order clause holds on every relatively compact open because the restricted triple lives on a manifold modelled on 𝕜⁰, where the ideal sheaf is the unit ideal sheaf (AnalyticTriple.ord_lt_of_dim_zero); the unfolding lemmas are stage0AnFam_bo, stage0AnFam_bmo, boZeroAnFam_seqOn, bmoZeroAnFam_seqOn;
• succOfBMOanFam, succAnFam — the successor stage ([Kol07, 70.1] then [Kol07, 70.2]), with succAnFam_eq_succOfBMOanFam, succAnFam_bo, succAnFam_bmo, succAnFam_congr, exists_succAnFam;
• orderReductionTowerAnFam h103 h107 — the recursion, with orderReductionTowerAnFam_zero, orderReductionTowerAnFam_succ, orderReductionTowerAnFam_succ_bo, orderReductionTowerAnFam_succ_bmo, exists_orderReductionTowerAnFam, nonempty_boanFam, nonempty_bmoanFam — each the generic statement at the compatible-family structures.

The two steps are constructed in Stage/InstancesFam.lean (Theorem 103) and Stage/InstancesFamTheorem107.lean (Theorem 107); the tower at those steps, Stage/Concrete.lean, provides the order-reduction functors used by the analytic main theorems.

@[reducible, inline]

abbrev Hironaka.Manifold.OrderReductionStageAnFam (𝕜 : Type) [RCLike 𝕜] (n : ℕ) : Type (u + 1)

A stage of the recursion on the dimension at the compatible-family structures: order reduction for ideals (BOanFam) and for marked ideals (BMOanFam) at every mark.

Equations

• Hironaka.Manifold.OrderReductionStageAnFam 𝕜 n = Hironaka.Manifold.StageOf (Hironaka.Manifold.BOanFam 𝕜) (Hironaka.Manifold.BMOanFam 𝕜) n

@[reducible, inline]

abbrev Hironaka.Manifold.BOanFamStep (𝕜 : Type) [RCLike 𝕜] : Type (u + 1)

The first reduction step of [Kol07, 70] at the compatible-family structures: order reduction for ideals in dimension n + 1 from order reduction for marked ideals in dimension n ([Kol07, Theorem 103]).

Equations

• Hironaka.Manifold.BOanFamStep 𝕜 = Hironaka.Manifold.StepBOOf (Hironaka.Manifold.BOanFam 𝕜) (Hironaka.Manifold.BMOanFam 𝕜)

@[reducible, inline]

abbrev Hironaka.Manifold.BMOanFamStep (𝕜 : Type) [RCLike 𝕜] : Type (u + 1)

The second reduction step of [Kol07, 70] at the compatible-family structures: order reduction for marked ideals in dimension n from order reduction for ideals in dimension n ([Kol07, Theorem 107]).

Equations

• Hironaka.Manifold.BMOanFamStep 𝕜 = Hironaka.Manifold.StepBMOOf (Hironaka.Manifold.BOanFam 𝕜) (Hironaka.Manifold.BMOanFam 𝕜)

The base stage

noncomputable def Hironaka.Manifold.boZeroAnFam {𝕜 : Type} [RCLike 𝕜] (m : ℕ) : BOanFam 𝕜 0 m

Order reduction for ideals in dimension zero at the compatible-family structures ([Kol07, 70]): the trivial family functor on the class BOClass m. On every relatively compact open U the restricted triple lives on a manifold modelled on 𝕜⁰, where the ideal sheaf is the unit ideal sheaf and has order 0 < m (AnalyticTriple.ord_lt_of_dim_zero, with 1 ≤ m from the class); the other clauses are those of the trivial family functor (Functor/FamilyNil.lean).

Equations

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

noncomputable def Hironaka.Manifold.bmoZeroAnFam {𝕜 : Type} [RCLike 𝕜] (m : ℕ) : BMOanFam 𝕜 0 m

Order reduction for marked ideals in dimension zero at the compatible-family structures ([Kol07, 70]): the trivial family functor on the class BMOClass m, with the same clauses as boZeroAnFam.

Equations

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

noncomputable def Hironaka.Manifold.stage0AnFam {𝕜 : Type} [RCLike 𝕜] : OrderReductionStageAnFam 𝕜 0

The base stage of the tower on the compatible-family structures, in dimension zero.

Equations

• Hironaka.Manifold.stage0AnFam = { bo := Hironaka.Manifold.boZeroAnFam, bmo := Hironaka.Manifold.bmoZeroAnFam }

theorem Hironaka.Manifold.stage0AnFam_bo (𝕜 : Type) [RCLike 𝕜] (m : ℕ) : stage0AnFam.bo m = boZeroAnFam m

theorem Hironaka.Manifold.stage0AnFam_bmo (𝕜 : Type) [RCLike 𝕜] (m : ℕ) : stage0AnFam.bmo m = bmoZeroAnFam m

theorem Hironaka.Manifold.boZeroAnFam_seqOn {𝕜 : Type} [RCLike 𝕜] (m : ℕ) {M : AnalyticManifold 𝕜 (Fin 0 → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin 0 → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((boZeroAnFam m).functor.fam T hT).seqOn U hU = AnalyticManifold.BlowUpSequence.nil (M.restrict U)

The value of boZeroAnFam on every triple and every relatively compact open is the empty sequence of centres.

theorem Hironaka.Manifold.bmoZeroAnFam_seqOn {𝕜 : Type} [RCLike 𝕜] (m : ℕ) {M : AnalyticManifold 𝕜 (Fin 0 → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin 0 → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((bmoZeroAnFam m).functor.fam T hT).seqOn U hU = AnalyticManifold.BlowUpSequence.nil (M.restrict U)

The value of bmoZeroAnFam on every triple and every relatively compact open is the empty sequence of centres.

The successor stage

def Hironaka.Manifold.succOfBMOanFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (bmo : (s : ℕ) → BMOanFam 𝕜 n s) : OrderReductionStageAnFam 𝕜 (n + 1)

The stage n + 1 from the marked families of the stage n ([Kol07, 70]): the first reduction step applied to the marked families, then the second applied to the result.

Equations

• Hironaka.Manifold.succOfBMOanFam h103 h107 bmo = Hironaka.Manifold.succOfBMOOf h103 h107 bmo

def Hironaka.Manifold.succAnFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (S : OrderReductionStageAnFam 𝕜 n) : OrderReductionStageAnFam 𝕜 (n + 1)

The successor stage: succOfBMOanFam at the marked families of the given stage.

Equations

• Hironaka.Manifold.succAnFam h103 h107 S = Hironaka.Manifold.succOf h103 h107 S

theorem Hironaka.Manifold.succAnFam_eq_succOfBMOanFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (S : OrderReductionStageAnFam 𝕜 n) : succAnFam h103 h107 S = succOfBMOanFam h103 h107 S.bmo

theorem Hironaka.Manifold.succAnFam_bo {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (S : OrderReductionStageAnFam 𝕜 n) : (succAnFam h103 h107 S).bo = h103.bo n S.bmo

theorem Hironaka.Manifold.succAnFam_bmo {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (S : OrderReductionStageAnFam 𝕜 n) : (succAnFam h103 h107 S).bmo = h107.bmo (n + 1) (succAnFam h103 h107 S).bo

theorem Hironaka.Manifold.succAnFam_congr {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (S S' : OrderReductionStageAnFam 𝕜 n) (h : S.bmo = S'.bmo) : succAnFam h103 h107 S = succAnFam h103 h107 S'

The successor stage depends on the stage below only through its marked families, as in the hypothesis "assume that (69) holds in dimensions < n" of [Kol07, Theorem 103].

theorem Hironaka.Manifold.exists_succAnFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) {n : ℕ} (S : OrderReductionStageAnFam 𝕜 n) : ∃ (S' : OrderReductionStageAnFam 𝕜 (n + 1)), S'.bo = h103.bo n S.bmo ∧ S'.bmo = h107.bmo (n + 1) S'.bo

The recursion

noncomputable def Hironaka.Manifold.orderReductionTowerAnFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) (n : ℕ) : OrderReductionStageAnFam 𝕜 n

The order-reduction tower on the compatible-family structures ([Kol07, 70]): the stage in every dimension, by recursion from stage0AnFam along the two reduction steps.

Equations

• Hironaka.Manifold.orderReductionTowerAnFam h103 h107 = Hironaka.Manifold.towerOf Hironaka.Manifold.stage0AnFam h103 h107

theorem Hironaka.Manifold.orderReductionTowerAnFam_zero {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) : orderReductionTowerAnFam h103 h107 0 = stage0AnFam

theorem Hironaka.Manifold.orderReductionTowerAnFam_succ {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) (n : ℕ) : orderReductionTowerAnFam h103 h107 (n + 1) = succAnFam h103 h107 (orderReductionTowerAnFam h103 h107 n)

theorem Hironaka.Manifold.orderReductionTowerAnFam_succ_bo {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) (n m : ℕ) : (orderReductionTowerAnFam h103 h107 (n + 1)).bo m = h103.bo n (orderReductionTowerAnFam h103 h107 n).bmo m

theorem Hironaka.Manifold.orderReductionTowerAnFam_succ_bmo {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) (n m : ℕ) : (orderReductionTowerAnFam h103 h107 (n + 1)).bmo m = h107.bmo (n + 1) (orderReductionTowerAnFam h103 h107 (n + 1)).bo m

theorem Hironaka.Manifold.exists_orderReductionTowerAnFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) : ∃ (st : (n : ℕ) → OrderReductionStageAnFam 𝕜 n), st 0 = stage0AnFam ∧ ∀ (n : ℕ), st (n + 1) = succAnFam h103 h107 (st n)

theorem Hironaka.Manifold.nonempty_boanFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) (n m : ℕ) : Nonempty (BOanFam 𝕜 n m)

Given the two reduction steps, order reduction for ideals exists in every dimension and at every mark, in the compatible-family form.

theorem Hironaka.Manifold.nonempty_bmoanFam {𝕜 : Type} [RCLike 𝕜] (h103 : BOanFamStep 𝕜) (h107 : BMOanFamStep 𝕜) (n m : ℕ) : Nonempty (BMOanFam 𝕜 n m)

Given the two reduction steps, order reduction for marked ideals exists in every dimension and at every mark, in the compatible-family form.