Adapted charts: basic lemmas and locality

On the source of an adapted chart (φ, σ) for Y (IsAdaptedChart), Y is the zero set of the adapted coordinates ψ_{σ i} ∘ φ (IsAdaptedChart.mem_iff'), so φ(Y ∩ U) = φ(U) ∩ {z_σ = 0} (image_inter'), the form of Bierstone–Milman's blowing-up charts [BM88, Definition 4.1 (2)]; adapted charts restrict to open sets (restrOpen', through Mathlib's restr_mem_maximalAtlas); the zero set of c coordinates of any chart of the maximal atlas is adapted to that chart (isAdaptedChart_zeroSet', the entry point for the charts produced by the chart-extension theorem); a nonempty closed submanifold has codimension at most n; the empty set is a closed submanifold of every codimension; and on a manifold the closed submanifolds of codimension 0 are the clopen sets. Locality: a closed submanifold of M is one of every open subset (isClosedSubmanifoldOn'), the zero set of adapted coordinates is a closed submanifold of the chart domain (IsAdaptedChart.isClosedSubmanifoldOn'), and closed submanifolds of the members of an open cover glue (of_cover'; Bierstone–Milman: a set which is locally the support of a smooth subspace "is globally the support of a smooth subspace" [BM97, §3]). These are the lemmas every later use of closed submanifolds (centres, hypersurfaces of maximal contact, components of the boundary) rests on.

theorem OpenPartialHomeomorph.restrOpen_eq_restr {X : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Z] (e : OpenPartialHomeomorph X Z) {s : Set X} (hs : IsOpen s) : e.restrOpen s hs = e.restr s

restrOpen is restr for an open set.

theorem Manifold.IsAdaptedChart.mem_iff' {𝕜 : 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 φ σ) {x : M} (hx : x ∈ φ.source) : x ∈ Y ↔ ∀ (i : Fin c), ψ (↑φ x) (σ i) = 0

On the source of an adapted chart, Y is the zero set of the adapted coordinates.

theorem Manifold.IsAdaptedChart.image_inter' {𝕜 : 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 φ σ) : ↑φ '' (Y ∩ φ.source) = φ.target ∩ {y : E | ∀ (i : Fin c), ψ y (σ i) = 0}

φ(Y ∩ U) = φ(U) ∩ {z_σ = 0} [BM88, Definition 4.1 (2)].

theorem Manifold.IsAdaptedChart.restrOpen' {𝕜 : 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 φ σ) (s : Set M) (hs : IsOpen s) : IsAdaptedChart ψ Y (φ.restrOpen s hs) σ

The restriction of an adapted chart to an open set is adapted.

theorem Manifold.isAdaptedChart_zeroSet' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {φ : OpenPartialHomeomorph M E} {c : ℕ} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (σ : Fin c ↪ Fin n) : IsAdaptedChart ψ (φ.source ∩ {x : M | ∀ (i : Fin c), ψ (↑φ x) (σ i) = 0}) φ σ

The zero set of c coordinates of a chart of the maximal atlas, on its source, has that chart as an adapted chart (the entry point for the charts produced by the chart-extension theorem).

theorem Manifold.IsClosedSubmanifold.codim_le' {𝕜 : 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) (hne : Y.Nonempty) : c ≤ n

A nonempty closed submanifold has codimension at most n.

theorem Manifold.isClosedSubmanifold_empty' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (c : ℕ) : IsClosedSubmanifold ψ ∅ c

The empty set is a closed submanifold of every codimension.

theorem Manifold.isClosedSubmanifold_zero_iff' {𝕜 : 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} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] : IsClosedSubmanifold ψ Y 0 ↔ IsClopen Y

On a manifold, the closed submanifolds of codimension 0 are the clopen sets.

Locality

theorem Manifold.IsClosedSubmanifold.isClosedSubmanifoldOn' {𝕜 : 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) {U : Set M} (hU : IsOpen U) : IsClosedSubmanifoldOn ψ U Y c

A closed submanifold of M is a closed submanifold of every open subset.

theorem Manifold.isClosed_zeroSet_coords {𝕜 : Type} [RCLike 𝕜] {n c : ℕ} (σ : Fin c ↪ Fin n) : IsClosed {y : Fin n → 𝕜 | ∀ (i : Fin c), y (σ i) = 0}

The coordinate subspace {y | ∀ i, y (σ i) = 0} is closed.

theorem Manifold.IsAdaptedChart.isClosedSubmanifoldOn' {𝕜 : 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 φ σ) : IsClosedSubmanifoldOn ψ φ.source Y c

On the source of an adapted chart, Y is a closed submanifold.

theorem Manifold.IsClosedSubmanifold.of_cover' {𝕜 : 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 : ℕ} {ι : Type u_2} {U : ι → Set M} (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ (i : ι), U i = Set.univ) (h : ∀ (i : ι), IsClosedSubmanifoldOn ψ (U i) Y c) : IsClosedSubmanifold ψ Y c

A set that is a closed submanifold of every member of an open cover is a closed submanifold of M [BM97, §3].