Closed submanifolds of a disjoint-union cover

For a cover of M by pairwise disjoint analytic open embeddings ιᵢ : Nᵢ → M, the union of the images of closed submanifolds of the pieces is a closed submanifold of the same codimension (IsClosedSubmanifold.iUnion_image): closed as the complement of the open union of the images of the complements, with adapted charts transported along the open embeddings (transportChart of Hironaka/Manifold/BlowUp/Functor.lean). With the two set-theoretic lemmas iUnion_image_inter_range and compl_iUnion_image. This is the step of Kollár's proof of Theorem 103 in which the local hypersurfaces of maximal contact H^{(j)} ⊂ X^{(j)} are assembled into the smooth hypersurface H^* := ∐_j H^{(j)} of the disjoint union X^* := ∐_j X^{(j)} [Kol07, Theorem 103, proof, Step 3]; it is used in that role in Hironaka/Resolution/Analytic/OrderReduction/SigmaContact.lean.

theorem Manifold.iUnion_image_inter_range {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsAnalyticOpenEmbedding (ι i)) (hdisj : Pairwise fun (i j : σ) => Disjoint (Set.range ⇑(ι i)) (Set.range ⇑(ι j))) (Y : (i : σ) → Set (N i).carrier) (i : σ) : (⋃ (j : σ), ⇑(ι j) '' Y j) ∩ Set.range ⇑(ι i) = ⇑(ι i) '' Y i

The union of the images meets the range of ιᵢ in the image of the i-th piece.

theorem Manifold.compl_iUnion_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {σ : Type u} {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsAnalyticOpenEmbedding (ι i)) (hdisj : Pairwise fun (i j : σ) => Disjoint (Set.range ⇑(ι i)) (Set.range ⇑(ι j))) (hcov : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ) (Y : (i : σ) → Set (N i).carrier) : (⋃ (i : σ), ⇑(ι i) '' Y i)ᶜ = ⋃ (i : σ), ⇑(ι i) '' (Y i)ᶜ

The complement of the union of the images is the union of the images of the complements.

theorem Manifold.IsClosedSubmanifold.iUnion_image {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {σ : Type u} {N : σ → AnalyticManifold 𝕜 E} (ι : (i : σ) → AnalyticMap (N i) M) (hι : ∀ (i : σ), IsAnalyticOpenEmbedding (ι i)) (hdisj : Pairwise fun (i j : σ) => Disjoint (Set.range ⇑(ι i)) (Set.range ⇑(ι j))) (hcov : ⋃ (i : σ), Set.range ⇑(ι i) = Set.univ) (Y : (i : σ) → Set (N i).carrier) {c : ℕ} (hY : ∀ (i : σ), IsClosedSubmanifold ψ₀ (Y i) c) : IsClosedSubmanifold ψ₀ (⋃ (i : σ), ⇑(ι i) '' Y i) c

The union of the images of closed submanifolds of the pieces of a disjoint-union cover is a closed submanifold of the same codimension (Kollár's "the disjoint union H^* := ∐_j H^{(j)} is a smooth hypersurface", [Kol07, Theorem 103, proof, Step 3]): closed as the complement of the open union of the images of the complements, with adapted charts transported along the open embeddings.