The marked order-reduction record BMO^{an}_{n,m} from the input family

The packaging of [Kol07, Theorem 107] on manifolds in the family form: the marked order-reduction functor BMO_{n,m} on the class BMOClass m at the standard model 𝕜ⁿ, from the input family bo : ∀ d, BOanFam 𝕜 n d (the order-reduction records at every order), as the structure BMOanFam 𝕜 n m (Hironaka.Resolution.Analytic.Functor.Family). The per-open value is bmoSeqOn (Hironaka.Resolution.Analytic.OrderReduction.Modified.BmoSeqOn: the chain of the three steps of the proof, [Kol07, 111], over a relatively compact open, restricted to it and with its empty blow-ups erased), and the fields of the structure are its exports read one each, as for stepAFunctor (Hironaka.Resolution.Analytic.OrderReduction.Modified.StepAComm):

• bmoFunctor: the family functor, bmoSeqOn on every relatively compact open, without empty centres (bmoSeqOn_noEmptyCenters), compatible under restriction up to empty blow-ups (bmoSeqOn_compat; [Wlo09, Theorem 2.0.3, (4)], [Wlo09, Definition 3.2.6]);
• bmoFunctor_commutesWithLocalIsos ([Kol07, Theorem 107, (2)]; [Kol07, 34.1] per open) from bmoSeqOn_pullback, and bmoFunctor_indifferentToEmptyMembers from bmoSeqOn_indiff;
• BMOanFamOfInput_of_hid: the structure, with the order clause bmoSeqOn_isOfOrderGe ([Kol07, Definition 66, (2′)–(4′)]), the output clause ord_lt_bmoSeqOn ([Kol07, Theorem 107, (1)]) and the two clauses above.

The four interfaces of the assembly, hcomp : NonmonomialComap (the non-monomial part commutes with pull-back), hid : NonmonomialTransformIdentity, hidN : NonmonomialTransformIdentityMod (the identity modulo N) and st3 : MonomialStep3Fam 𝕜 n m (the third step as a datum), are binders here, at the fixed n; nothing in this module depends on their inhabitants. theorem107FamStarOf (Hironaka.Resolution.Analytic.OrderReduction.Stage.InstancesFamTheorem107) and concreteTheorem107FamStar (Hironaka.Resolution.Analytic.OrderReduction.Stage.Concrete) discharge them.

noncomputable def Hironaka.Manifold.BMO.bmoFunctor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (m : ℕ) (st3 : MonomialStep3Fam 𝕜 n m) (bo : (d : ℕ) → BOanFam 𝕜 n d) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => Manifold.AnalyticTriple.BMOClass m

The family functor of BMO_{n,m} on the marked class at the standard model — bmoSeqOn on every relatively compact open, without empty centres, compatible under restriction up to empty blow-ups (as stepAFunctor, Hironaka.Resolution.Analytic.OrderReduction.Modified.StepAComm).

Equations

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

@[simp]

theorem Hironaka.Manifold.BMO.bmoFunctor_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (m : ℕ) (st3 : MonomialStep3Fam 𝕜 n m) (bo : (d : ℕ) → BOanFam 𝕜 n d) {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)) : ((bmoFunctor ⋯ ⋯ ⋯ m st3 bo).fam T hT).seqOn U hU = bmoSeqOn T m hT bo ⋯ ⋯ ⋯ st3 U hU

The value of the family functor on an open is bmoSeqOn.

theorem Hironaka.Manifold.BMO.bmoFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (m : ℕ) (st3 : MonomialStep3Fam 𝕜 n m) (bo : (d : ℕ) → BOanFam 𝕜 n d) : (bmoFunctor ⋯ ⋯ ⋯ m st3 bo).CommutesWithLocalIsos

The family functor commutes with local analytic isomorphisms — bmoSeqOn_pullback at the functor's value (as stepAFunctor_commutesWithLocalIsos).

theorem Hironaka.Manifold.BMO.bmoFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (m : ℕ) (st3 : MonomialStep3Fam 𝕜 n m) (bo : (d : ℕ) → BOanFam 𝕜 n d) : (bmoFunctor ⋯ ⋯ ⋯ m st3 bo).IndifferentToEmptyMembers

The family functor is indifferent to empty boundary members — bmoSeqOn_indiff at the functor's value (as stepAFunctor_indifferentToEmptyMembers).

noncomputable def Hironaka.Manifold.BMO.BMOanFamOfInput_of_hid {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (m : ℕ) (st3 : MonomialStep3Fam 𝕜 n m) (bo : (d : ℕ) → BOanFam 𝕜 n d) : BMOanFam 𝕜 n m

The structure BMO^{an}_{n,m} from the input family, the four interfaces of the assembly as binders: the family functor bmoFunctor with the clauses of [Kol07, Theorem 107] read per relatively compact open: order ≥ m (bmoSeqOn_isOfOrderGe), the last marked transform of order < m pointwise (ord_lt_bmoSeqOn, [Kol07, Theorem 107, (1)]), commutation with local analytic isomorphisms ([Kol07, Theorem 107, (2)]) and indifference to empty members. theorem107FamStarOf and concreteTheorem107FamStar (Stage/InstancesFamTheorem107.lean, Stage/Concrete.lean) discharge the binders.

Equations

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

theorem Hironaka.Manifold.BMO.BMOanFamOfInput_of_hid_functor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (hcomp : BMOmod.NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hid : BMOmod.NonmonomialTransformIdentity (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (hidN : NonmonomialTransformIdentityMod (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) (m : ℕ) (st3 : MonomialStep3Fam 𝕜 n m) (bo : (d : ℕ) → BOanFam 𝕜 n d) : (BMOanFamOfInput_of_hid ⋯ ⋯ ⋯ m st3 bo).functor = bmoFunctor ⋯ ⋯ ⋯ m st3 bo

The functor of the structure is bmoFunctor.