Every point has a neighbourhood with a hypersurface of maximal contact

Step 2 of the proof of [Kol07, Theorem 103] assumes a smooth hypersurface of maximal contact, a condition "always satisfied in a suitable open neighborhood of any point" by Theorem 80 (2): [Kol07, Theorem 80 (2)] states that every point has an open neighbourhood on which a section of MC(I) has a smooth zero divisor. Step 3 covers X by such open subsets X^{(j)}.

AnalyticTriple.exists_isPullbackOf_localMCClass is the analytic form: for a triple of the class BOClass m and a point x, the triple restricted to a suitable open neighbourhood V of x lies in the class LocalMCClass m: it is in BOClass m (ClassPullback.lean) and carries a global hypersurface of maximal contact. At a point of maximal order m, a section h of MC(𝓘) of order 1 at x exists (exists_mem_carrier_iteratedDeriv_ordElem_eq_one), and the analytic implicit function theorem gives an adapted chart e with h as one of its coordinates on its source (exists_adapted_chart_of_ord_eq_one'); take V := e.source and H := {h = 0} ⊆ V, read on the bundled manifold V. Then the ideal sheaf of H lies in MC(h^* 𝓘) stalkwise: at a point of H the stalk of the ideal sheaf of H is generated by the coordinate h, a section of MC(𝓘); off H the germ of h is a unit of MC(h^* 𝓘). At a point of order < m, MC(𝓘) is the unit ideal sheaf near x and the empty hypersurface serves.

This is the local existence that Step 3 of the proof of Theorem 103 globalizes (GlobalizeCover.lean, GlobalizeFamCover.lean).

theorem Manifold.AnalyticTriple.exists_isPullbackOf_localMCClass {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [hfd : FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {m : ℕ} {M : AnalyticManifold 𝕜 E} {T : AnalyticTriple ψ₀ M} (hT : BOClass m T) (x : M.carrier) : ∃ (N : AnalyticManifold 𝕜 E) (T' : AnalyticTriple ψ₀ N) (g : AnalyticMap N M), IsAnalyticOpenEmbedding g ∧ x ∈ Set.range ⇑g ∧ T'.IsPullbackOf T g ∧ LocalMCClass m T'

Every point of a triple of the class BOClass m has an open neighbourhood, embedded by the inclusion, whose pulled-back triple lies in LocalMCClass m (Step 2 of the proof of [Kol07, Theorem 103] with [Kol07, Theorem 80 (2)]; the cover of Step 3): at a point of order m the hypersurface {h = 0} cut out by a section h of MC(𝓘) of order 1, an adapted coordinate by the implicit function theorem; at a point of order < m the empty hypersurface, MC(𝓘) being the unit ideal sheaf there.