Hypersurfaces of maximal contact on disjoint unions

Step 2 of the proof of [Kol07, Theorem 103] notes that the existence of a hypersurface of maximal contact "is also preserved under disjoint unions", and Step 3 uses it: the disjoint union H^* := ∐_j H^{(j)} ⊂ ∐_j X^{(j)} =: X^* "is a smooth hypersurface of maximal contact". On manifolds: a triple which is the disjoint union of triples each carrying a global hypersurface of maximal contact carries one, namely the union H := ⋃ᵢ ιᵢ(Hᵢ) of the images of the pieces' hypersurfaces along the open embeddings ιᵢ with pairwise disjoint ranges covering M. H is closed (its complement is the open union of the images ιᵢ(Hᵢᶜ)), it is a closed submanifold of codimension one (the adapted charts of Hᵢ transported along ιᵢ), and its ideal sheaf lies in MC(𝓘): at a point ιᵢ y both stalks are read on the piece, the pull-back of the ideal sheaf of H along ιᵢ being the ideal sheaf of Hᵢ, the pull-back of MC(𝓘) being MC(ιᵢ^* 𝓘), and the germ map of a local isomorphism being bijective.

• AnalyticTriple.closedUnderSigma_hasMaximalContact — the class of triples with a global hypersurface of maximal contact is closed under countable disjoint unions (Kollár's disjoint unions of triples, [Kol07, Warning 38]);
• AnalyticTriple.localMCClass_pullback_sigmaDescMap — the pull-back of a triple of BOClass m along the coproduct ∐ᵢ ιᵢ of countably many open embeddings whose pulled-back triples have maximal contact lies in LocalMCClass m; this is the class statement of Step 3 of the proof of Theorem 103, that BO_{n,m} "is defined on (X^*, g^* I, g^{-1} E)" by Step 2.

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

"This condition is also preserved under disjoint unions" (Step 2 of the proof of [Kol07, Theorem 103]; Step 3: the disjoint union H^* := ∐_j H^{(j)} "is a smooth hypersurface of maximal contact"): the class of triples with a global hypersurface of maximal contact is closed under countable disjoint unions. H := ⋃ᵢ ιᵢ(Hᵢ) is a closed hypersurface (IsClosedSubmanifold.iUnion_image) and its ideal sheaf lies in MC(𝓘) stalkwise at ιᵢ y, both stalks read on the i-th piece through the bijective germ map of ιᵢ.

theorem Manifold.AnalyticTriple.localMCClass_pullback_sigmaDescMap {𝕜 : 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) {σ : Type u} [Countable σ] {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsAnalyticOpenEmbedding (ι i)) (hmc : ∀ (i : σ), HasMaximalContact m (T.pullback (ι i) ⋯)) : LocalMCClass m (T.pullback (sigmaDescMap ι) ⋯)

Step 3 of the proof of [Kol07, Theorem 103] (H^* is a hypersurface of maximal contact, so BO_{n,m} "is defined on (X^*, g^* I, g^{-1} E)" by Step 2): the pull-back of a triple of the class BOClass m along the coproduct ∐ᵢ ιᵢ of countably many open embeddings whose pulled-back triples have maximal contact lies in LocalMCClass m; it is in BOClass m by pull-back along a local isomorphism, and has maximal contact by the closure under disjoint unions applied to the disjoint-union decomposition of the pull-back (isSigmaOf_pullback_sigmaDescMap).