Theorem 103, Step 3: the local cover by triples with maximal contact

Step 3 of the proof of [Kol07, Theorem 103] (the global case) covers X by open subsets X^{(j)} each carrying a smooth hypersurface of maximal contact H^{(j)}; the disjoint union H^* := ∐_j H^{(j)} ⊂ ∐_j X^{(j)} =: X^* is then a smooth hypersurface of maximal contact, and for g : X^* → X the coproduct of the inclusions, Step 2 defines BO_{n,m} on (X^*, g^* I, g^{-1} E). On manifolds this is the local cover data of the globalization theorem [Kol07, Theorem 105] (OrderReduction/GlobalizeFam.lean, AnalyticTriple.LocalCoverData) for the pair of classes (BOClass m, LocalMCClass m): every triple of BOClass m is covered by a triple with a global hypersurface of maximal contact, the disjoint union of countably many of the neighbourhoods with maximal contact given by [Kol07, Theorem 80 (2)] (exists_isPullbackOf_localMCClass; countably many by second countability), which lies in LocalMCClass m (localMCClass_pullback_sigmaDescMap).

The hypothesis (2)(ii) of Theorem 105, that the local class is closed under disjoint unions, is not available here: a countable disjoint union of triples of BOClass m need not have finitely many nonempty boundary members. The construction is therefore run from the cover data directly. The class LocalMCClass m is closed under pull-back along every local analytic isomorphism (localMCClass_of_isPullbackOf), hence under fibre products of local covers (localCoversFibreClosed_localMCClass), the form in which Theorem 105's proof applies the functor to X' ×_X X'.

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

Step 3 of the proof of [Kol07, Theorem 103] (the cover of X by open subsets X^{(j)}, the coproduct g : X^* → X of the inclusions, and BO_{n,m} "defined on (X^*, g^* I, g^{-1} E)"): every triple of BOClass m has a local cover by a triple of LocalMCClass m, the disjoint union of countably many of the neighbourhoods with a hypersurface of maximal contact of [Kol07, Theorem 80 (2)] (second countability), which lies in LocalMCClass m.

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

The class LocalMCClass m is closed under pull-back along every local analytic isomorphism: BOClass m is (boClass_of_isPullbackOf) and a hypersurface of maximal contact pulls back (hasMaximalContact_of_isPullbackOf). Kollár remarks in Step 2 of the proof of [Kol07, Theorem 103] that the condition "is also preserved under disjoint unions"; the closure under pull-backs is the library's form, used without statement in his Step 3.

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

LocalMCClass m is closed under fibre products of local covers, the hypothesis under which the proof of [Kol07, Theorem 105] applies the functor to X' ×_X X': a triple carrying the pull-back data of a member along the first projection, a local analytic isomorphism, is a member.