The order reduction read at the nonmonomial triple

"Apply order reduction (68) to N(I)" [Kol07, 111, Step 1]: a round of the rounds on the nonmonomial part reads the order reduction BO_{n,d} at the nonmonomial triple (M, N(𝓘), E). Packaged as a family functor in its own right, nonmonomialFunctor bo on the class NonmonomialClass d of triples whose nonmonomial triple lies in the domain of BO_{n,d}, it inherits the two naturality properties from bo:

• it commutes with local analytic isomorphisms (the analogue of [Kol07, Theorem 103 (2)]), because the nonmonomial part commutes with pull-back (NonmonomialComap);
• it is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]), because the nonmonomial part is (nonmonomialTriple_eq_of_isEmptyExtension).

The value of the round in StepALink.lean is the value of this functor at the induced triple (BState.roundValue_eq_nonmonomialFunctor, a rfl), so the transport lemmas for values at induced triples (InducedValueFunctor.lean) apply to the link of the descent.

@[reducible, inline]

abbrev Hironaka.Manifold.BMOmod.NonmonomialClass {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (d : ℕ) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) : Prop

The class of triples whose nonmonomial triple lies in the domain of BO_{n,d} (1 ≤ d, ord N(𝓘) ≤ d everywhere, finitely many nonempty members): the domain of the round on the nonmonomial part [Kol07, 111, Step 1].

Equations

• Hironaka.Manifold.BMOmod.NonmonomialClass d T = Manifold.AnalyticTriple.BOClass d (Hironaka.Manifold.BMO.nonmonomialTriple T)

noncomputable def Hironaka.Manifold.BMOmod.nonmonomialFunctor {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} (bo : BOanFam 𝕜 n d) : AnalyticFamilyFunctor (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) fun {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} => NonmonomialClass d

The order reduction read at the nonmonomial triple, as a family functor on NonmonomialClass d [Kol07, 111, Step 1]: the value of bo at (M, N(𝓘), E), re-typed as a family for (M, 𝓘, E) (CompatibleFamily.changeTriple; the triple is not part of the data of a compatible family).

Equations

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

@[simp]

theorem Hironaka.Manifold.BMOmod.nonmonomialFunctor_fam_seqOn {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} (bo : BOanFam 𝕜 n d) {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (hT : NonmonomialClass d T) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : ((nonmonomialFunctor bo).fam T hT).seqOn U hU = (bo.functor.fam (BMO.nonmonomialTriple T) hT).seqOn U hU

theorem Hironaka.Manifold.BMOmod.nonmonomialClass_pullback {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) {M N : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (hT : NonmonomialClass d T) (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) : NonmonomialClass d (T.pullback g hg)

The class is closed under pull-back along local analytic isomorphisms (NonmonomialComap and boClass_of_isPullbackOf).

theorem Hironaka.Manifold.BMOmod.nonmonomialClass_of_isEmptyExtension {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} (hT : NonmonomialClass d T) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') {e : F'.ι ↪o T.F.ι} (he : Manifold.HypersurfaceFamily.IsEmptyExtension e) : NonmonomialClass d { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }

The class is indifferent to empty boundary members: deleting or adding empty members keeps the nonmonomial triple's ideal (nonmonomialTriple_eq_of_isEmptyExtension) and the finiteness of the nonempty members.

theorem Hironaka.Manifold.BMOmod.nonmonomialClass_of_isEmptyExtension' {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) F') {e : F'.ι ↪o T.F.ι} (he : Manifold.HypersurfaceFamily.IsEmptyExtension e) (hT' : NonmonomialClass d { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) : NonmonomialClass d T

The converse: a triple whose boundary is an empty extension of the boundary of a triple of the class (same ideal) lies in the class.

theorem Hironaka.Manifold.BMOmod.nonmonomialFunctor_commutesWithLocalIsos {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} (bo : BOanFam 𝕜 n d) (hcomp : NonmonomialComap (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜))) : (nonmonomialFunctor bo).CommutesWithLocalIsos

The family read at the nonmonomial triple commutes with local analytic isomorphisms (the analogue of [Kol07, Theorem 103 (2)] for the composite), since the nonmonomial triple of a pull-back is the pull-back of the nonmonomial triple (NonmonomialComap).

theorem Hironaka.Manifold.AnalyticFamilyFunctor.IndifferentToEmptyMembers.seqOn_eq_of_eq_F {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {Dom : {M : AnalyticManifold 𝕜 E} → Manifold.AnalyticTriple ψ₀ M → Prop} {B : AnalyticFamilyFunctor ψ₀ fun {M : AnalyticManifold 𝕜 E} => Dom} (hB : B.IndifferentToEmptyMembers) {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) {G : Manifold.HypersurfaceFamily M.carrier} (hG : T.F = G) (F' : Manifold.HypersurfaceFamily M.carrier) (hsnc' : Manifold.HypersurfaceFamily.IsSnc ψ₀ F') (e : F'.ι ↪o G.ι) (h1 : ∀ (i : F'.ι), G.hyp (e i) = F'.hyp i) (h2 : ∀ b ∉ Set.range ⇑e, G.hyp b = ∅) (hT : Dom T) (hT' : Dom { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' }) (U : TopologicalSpace.Opens M.carrier) (hU : IsCompact (closure ↑U)) : (B.fam T hT).seqOn U hU = (B.fam { I := T.I, isNonzeroEverywhere := ⋯, F := F', isSnc := hsnc' } hT').seqOn U hU

The indifference property with the boundary of the triple named by an equation (substituted), the shape in which the property applies at nonmonomialTriple T, whose boundary is T.F only up to the projection lemma nonmonomialTriple_F.

theorem Hironaka.Manifold.BMOmod.nonmonomialFunctor_indifferentToEmptyMembers {𝕜 : Type} [RCLike 𝕜] {n d : ℕ} (bo : BOanFam 𝕜 n d) : (nonmonomialFunctor bo).IndifferentToEmptyMembers

The family read at the nonmonomial triple is indifferent to empty boundary members (the counterpart, for boundary members, of [Kol07, 32]): the nonmonomial triple of the triple with the replaced boundary is the nonmonomial triple with the boundary replaced (nonmonomialTriple_eq_of_isEmptyExtension), and bo is indifferent.

The round's value

theorem Hironaka.Manifold.BMOmod.BState.nonmonomialClass {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) {W : TopologicalSpace.Opens M.carrier} {d : ℕ} (st : BState T m W d) (hd : 1 ≤ d) : NonmonomialClass d (ChainState.inducedTriple T m st.toChainState)

The invariant of the descent puts the induced triple in NonmonomialClass d.

theorem Hironaka.Manifold.BMOmod.BState.roundValue_eq_nonmonomialFunctor {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} {T : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M} {m : ℕ} (hT : Manifold.AnalyticTriple.BMOClass m T) (bo' : (d : ℕ) → BOanFam 𝕜 n d) {W : TopologicalSpace.Opens M.carrier} {d : ℕ} (st : BState T m W d) {V : TopologicalSpace.Opens M.carrier} (hV : IsCompact (closure ↑V)) (hVW : closure ↑V ⊆ ↑W) (hd : 1 ≤ d) : roundValue bo' st hV hVW hT hd = ((nonmonomialFunctor (bo' d)).fam (ChainState.inducedTriple T m st.toChainState) ⋯).seqOn (st.liftOpen hVW) ⋯

The value of the round is the value of the functor read at the nonmonomial triple, at the induced triple.