Connected components of a closed submanifold

The connected components of a closed submanifold are closed submanifolds of the same codimension, and the family of components is locally finite. The one geometric input is that an adapted chart (φ, σ) at a point of Y gives Y connected open neighbourhoods, arbitrarily small: the inverse image under the induced chart IsAdaptedChart.chartOn of a small ball of 𝕜^{n-c} (a ball is convex, hence preconnected, and the inverse chart is continuous on it; exists_preconnected_mem_nhds). Hence Y is locally connected (locallyConnectedSpace'), each component is open in Y — so, shrinking an adapted chart to an open set of M meeting Y inside the component, adapted for the component — and closed in M (connectedComponent'), every point of M has a neighbourhood meeting at most one component (locallyFinite_connectedComponents'), and every point b ∈ Y has an adapted chart whose source meets Y only inside the component of b (exists_adaptedChart_source_inter_subset). Not in the sources; these are the topological facts behind the treatment of the components of a centre (Hironaka's centres are irreducible; the algorithm's centres are unions of components, blown up one at a time or together).

theorem Manifold.IsAdaptedChart.exists_preconnected_mem_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {φ : OpenPartialHomeomorph M E} {c : ℕ} {σ : Fin c ↪ Fin n} (h : IsAdaptedChart ψ Y φ σ) {a : M} (ha : a ∈ Y) (has : a ∈ φ.source) {U : Set ↑Y} (hU : U ∈ nhds ⟨a, ha⟩) : ∃ V ∈ nhds ⟨a, ha⟩, IsOpen V ∧ IsPreconnected V ∧ V ⊆ U

Inside any neighbourhood of a point of Y lying in the source of an adapted chart there is an open connected neighbourhood: the inverse image of a small ball under the induced chart.

theorem Manifold.IsClosedSubmanifold.locallyConnectedSpace' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : LocallyConnectedSpace ↑Y

A closed submanifold is locally connected.

theorem Manifold.IsClosedSubmanifold.connectedComponent' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : ↑Y) : IsClosedSubmanifold ψ (Subtype.val '' connectedComponent a) c

The connected components of a closed submanifold are closed submanifolds of the same codimension.

theorem Manifold.IsClosedSubmanifold.locallyFinite_connectedComponents' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) : LocallyFinite fun (C : ConnectedComponents ↑Y) => Subtype.val '' ConnectedComponents.mk ⁻¹' {C}

The family of connected components of a closed submanifold is locally finite in M: a point of Y has a connected neighbourhood in Y, a point off Y a neighbourhood missing Y.

Adapted charts inside a connected component

theorem Manifold.IsClosedSubmanifold.exists_adaptedChart_source_inter_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ₀ Y c) {b : M.carrier} (hb : b ∈ Y) : ∃ (φ : OpenPartialHomeomorph M.carrier E) (σ : Fin c ↪ Fin n), b ∈ φ.source ∧ IsAdaptedChart ψ₀ Y φ σ ∧ φ.source ∩ Y ⊆ connectedComponentIn Y b

Every point b of a closed submanifold Y has an adapted chart of Y whose source meets Y only inside the connected component of b in Y.