The classes of Theorem 103 under pull-back along local analytic isomorphisms

The proof of [Kol07, Theorem 103] uses, without stating them, that its classes are stable under pull-back: the hypothesis of Step 2 is local, and in Step 3 BO_{n,m} "is defined on (X^*, g^* I, g^{-1} E)" by Step 2. Here: the class BOClass m and the class of triples with a global hypersurface of maximal contact are closed under pull-back along local analytic isomorphisms g : N → M. The order of the pulled-back ideal sheaf at y is the order of 𝓘 at g y, a nonempty preimage g⁻¹(E^j) comes from a nonempty E^j, and the preimage g⁻¹(H) of a hypersurface of maximal contact is one, its ideal sheaf being the pull-back of the ideal sheaf of H and the derivative ideal sheaves pulling back. In particular both classes are closed under pull-back along local isomorphisms covering cosupp(𝓘, m), the hypothesis ClosedUnderLocalIsoPullbackOverCosupp under which the value of a functor is independent of the hypersurface of maximal contact (FamilyIndependence.lean).

• AnalyticTriple.boClass_of_isPullbackOf, AnalyticTriple.hasMaximalContact_of_isPullbackOf;
• AnalyticTriple.boClass_closedUnderLocalIsoPullbackOverCosupp, AnalyticTriple.localMCClass_closedUnderLocalIsoPullbackOverCosupp.

theorem Manifold.AnalyticTriple.boClass_of_isPullbackOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} {M N : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} (hT : BOClass m T) {T' : AnalyticTriple ψ₀ N} {g : AnalyticMap N M} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT' : T'.IsPullbackOf T g) : BOClass m T'

The class BOClass m is closed under pull-back along local analytic isomorphisms (used implicitly in Step 3 of the proof of [Kol07, Theorem 103], "BO_{n,m} is defined on (X^*, g^* I, g^{-1} E)"): the order pulls back pointwise and the nonempty members of the pulled-back family are among the nonempty members.

theorem Manifold.AnalyticTriple.hasMaximalContact_of_isPullbackOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} {M N : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} (hT : HasMaximalContact m T) {T' : AnalyticTriple ψ₀ N} {g : AnalyticMap N M} (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑g) (hT' : T'.IsPullbackOf T g) : HasMaximalContact m T'

The class of triples with a global hypersurface of maximal contact is closed under pull-back along local analytic isomorphisms (the hypersurfaces H^{(j)} on the pieces X^{(j)} of Step 3 of the proof of [Kol07, Theorem 103]): the preimage of the hypersurface is one, its ideal sheaf being the pull-back of the ideal sheaf of H (comap_idealSheaf_of_isLocalDiffeomorph) and the derivative ideal sheaves pulling back.

theorem Manifold.AnalyticTriple.boClass_closedUnderLocalIsoPullbackOverCosupp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} : ClosedUnderLocalIsoPullbackOverCosupp (fun {M : AnalyticManifold 𝕜 E} => BOClass m) m

The class BOClass m is closed under pull-back along local analytic isomorphisms covering the cosupport.

theorem Manifold.AnalyticTriple.localMCClass_closedUnderLocalIsoPullbackOverCosupp {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} : ClosedUnderLocalIsoPullbackOverCosupp (fun {M : AnalyticManifold 𝕜 E} => LocalMCClass m) m

The class LocalMCClass m of triples with a global hypersurface of maximal contact is closed under pull-back along local analytic isomorphisms covering the cosupport.