The monomial procedure as a family functor

The monomial procedure of [Kol07, 111, Step 3] on the marked class BMOClass m at the standard model, packaged as a family functor (monomialStep3Functor): on a triple of the class, the compatible family whose value on a relatively compact open U is monomialStep3SeqOn (BMO/Step3Monomial/Value.lean), with no empty centres and compatible under restriction up to empty blow-ups (monomialStep3SeqOn_compat, [Wlo09, Theorem 2.0.3 (4)]). The structure MonomialStep3Fam 𝕜 n m of Modified/MonomialStep3Fam.lean is then inhabited (monomialStep3Fam) by this functor together with its two order properties, its commutation with local analytic isomorphisms (monomialStep3SeqOn_pullback, [Kol07, 34.1]) and its indifference to empty boundary members (monomialStep3SeqOn_indiff). This inhabitant is the monomial step of the analytic marked order reduction (Modified/Step3Link.lean).

noncomputable def Hironaka.Manifold.BMO.monomialStep3Functor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (m : ℕ) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BMOClass m

The family functor of the monomial procedure on the marked class at the standard model: on each triple of the class, the compatible family of the values monomialStep3SeqOn, with no empty centres and compatible under restriction up to empty blow-ups.

Equations

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

@[simp]

theorem Hironaka.Manifold.BMO.monomialStep3Functor_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (m : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BMOClass m T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((monomialStep3Functor m).fam T hT).seqOn U hU = monomialStep3SeqOn T m hT U hU

noncomputable def Hironaka.Manifold.BMO.monomialStep3Fam (𝕜 : Type) [RCLike 𝕜] (n m : ℕ) : MonomialStep3Fam 𝕜 n m

The inhabitant of MonomialStep3Fam 𝕜 n m: the functor of the monomial procedure with the order clauses of [Kol07, Definition 66 (2′)–(4′)] for (M(𝓘|_U), m), the terminal bound of [Kol07, 111, Step 3], the commutation with local analytic isomorphisms of [Kol07, Theorem 107 (2)] and the indifference to empty boundary members.

Equations

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