The modified first step: the modified core as the data of the maximal-contact step

The structure HFamData (with HFData) collects the four properties of the family data of [Kol07, Lemma 102] which the link of [Kol07, Theorem 103, Step 2.2] uses: the family, its order clause, its commutation with local analytic isomorphisms, and its indifference to empty boundary members indexed by the member. The assembly of the second step of the order reduction is stated over it. This module gives the modified core as such data at the mark 1: BMOmod.hFamDataMod R hRo hRc hRi : HFamData (refl) 1, from the modified functor R one dimension down with its three properties hRo, hRc, hRi (hypotheses here), through coreModFam, coreModOn_isOfOrderGe, coreModOn_commutesWithLocalIsos and coreModOn_indifferentToEmptyMembers. The exact-order clause and the disjointness of cosupports of [Kol07, Lemma 102] are not part of the structure: the modified core does not satisfy them, the stopped components keeping order 1 ("the algorithm is stopped", [Wlo09, Theorem 7.4.1]).

noncomputable def Hironaka.Manifold.BMOmod.hFamDataMod {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) : HFamData (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) 1

The modified core as the data of the maximal-contact step at the mark 1 ([Wlo09, Theorem 7.4.1]): at a triple of the class of BO_{n,1} and a member j, the modified core coreModFam R T j, with the order clause (coreModOn_isOfOrderGe), the commutation (coreModOn_commutesWithLocalIsos) and the indifference (coreModOn_indifferentToEmptyMembers) from the three properties hRo, hRc, hRi of the functor one dimension down.

Equations

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

theorem Hironaka.Manifold.BMOmod.hFamDataMod_fam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (R : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} => Manifold.AnalyticTriple.BMOClass 1) (hRo : ∀ {N : AnalyticManifold 𝕜 (Fin (n - 1) → 𝕜)} (T' : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin (n - 1) → 𝕜)) N) (hT' : Manifold.AnalyticTriple.BMOClass 1 T') (U' : TopologicalSpace.Opens N.carrier) (hU' : IsCompact (closure ↑U')), ((R.fam T' hT').seqOn U' hU').toSuccession.IsOfOrderGe (T'.pullback (N.inclusion U') ⋯).I 1 (T'.pullback (N.inclusion U') ⋯).F.idealSheaf) (hRc : R.CommutesWithLocalIsos) (hRi : R.IndifferentToEmptyMembers) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : Manifold.AnalyticTriple.BOClass 1 T) (j : T.F.ι) : (hFamDataMod R ⋯ ⋯ ⋯).fam T hT j = coreModFam R T j ⋯