A closed submanifold of a closed submanifold

The push-forward of a blow-up sequence of S to the ambient X regards the centres Z_i^S ⊆ S_i ⊆ X_i as closed submanifolds of X_i [Kol07, Definition 30.3], and conversely the restriction to S [Kol07, Definition 30.2] needs the centre Y ⊆ S as a closed submanifold of the bundled S, so that the restricted blow-down can be a blowing-up of S along Y in the sense of [BM88, Definition 4.1]. This module proves that a closed submanifold Y ⊆ S of M of codimension c is a closed submanifold of the bundled S (with its induced charts on 𝕜^{n-s}) of codimension c − s (IsClosedSubmanifold.preimage_val_of_subset); that a smooth subspace of a manifold is locally a coordinate subspace is [BM97, (3.8)(2)]. The adapted charts are the induced charts of the flag charts (exists_adaptedChart_flag, isAdaptedChart_chartOn_flag): in a flag chart Y = {z_σ = 0} and S = {z_{σ (τ j)} = 0}, so on S the remaining centre coordinates z_{σ k}, k ∉ range τ, cut out Y; read in the complementary coordinates of S's induced chart they are the coordinates of index restrictEmb σ τ (Model.lean). Not in the sources; the proof is a chart computation.

noncomputable def Manifold.IsClosedSubmanifold.inducedChart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ' : Fin s ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ') {a : M} (ha : a ∈ S) : OpenPartialHomeomorph hS.toAnalyticManifold.carrier (Fin (n - s) → 𝕜)

The induced chart of an adapted chart of S (IsAdaptedChart.chartOn), typed as a chart of the bundled S (so that statements about it elaborate on the bundled manifold).

Equations

• hS.inducedChart hφS ha = hφS.chartOn ha

theorem Manifold.IsClosedSubmanifold.inducedChart_apply {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ' : Fin s ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ') {a : M} (ha : a ∈ S) (x : hS.toAnalyticManifold.carrier) : ↑(hS.inducedChart hφS ha) x = projCompl σ' (ψ (↑φ ↑x))

theorem Manifold.IsClosedSubmanifold.mem_inducedChart_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ' : Fin s ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ') {a : M} (ha : a ∈ S) (x : hS.toAnalyticManifold.carrier) : x ∈ (hS.inducedChart hφS ha).source ↔ ↑x ∈ φ.source

theorem Manifold.IsClosedSubmanifold.mem_inducedChart_target {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ' : Fin s ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ') {a : M} (ha : a ∈ S) (w : Fin (n - s) → 𝕜) : w ∈ (hS.inducedChart hφS ha).target ↔ ψ.symm (embedCompl σ' w) ∈ φ.target

theorem Manifold.IsClosedSubmanifold.inducedChart_mem_maximalAtlas {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {S : Set M} {s : ℕ} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ' : Fin s ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ') {a : M} (ha : a ∈ S) : hS.inducedChart hφS ha ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) ⊤ hS.toAnalyticManifold.carrier

theorem Manifold.isAdaptedChart_chartOn_flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [T2Space M] [SecondCountableTopology M] {Y S : Set M} {c s : ℕ} (hS : IsClosedSubmanifold ψ S s) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {τ : Fin s ↪ Fin c} (hφ : IsAdaptedChart ψ Y φ σ) (hSflag : ∀ x ∈ φ.source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑φ x) (σ (τ j)) = 0) {a : M} (ha : a ∈ S) : IsAdaptedChart (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.preimageVal Y) (hS.inducedChart ⋯ ha) (restrictEmb σ τ)

The induced chart of a flag chart of Y ⊆ S is a chart of the bundled S adapted to Y, with the block embedding restrictEmb σ τ: on S the remaining centre coordinates z_{σ k}, k ∉ range τ, cut out Y.

theorem Manifold.IsClosedSubmanifold.preimage_val_of_subset {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {Y S : Set M} {c s : ℕ} (hS : IsClosedSubmanifold ψ S s) (hY : IsClosedSubmanifold ψ Y c) (hYS : Y ⊆ S) : IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin (n - s) → 𝕜)) (hS.preimageVal Y) (c - s)

A closed submanifold of a closed submanifold is a closed submanifold: a closed submanifold Y ⊆ S of codimension c is a closed submanifold of the bundled S of codimension c − s, in the induced charts — the adapted charts are the induced charts of the flag charts of Y ⊆ S.