Manifold structures from linear slice charts

Ambient charts flattening a subset of a manifold onto a fixed linear slice induce a manifold structure on the subset with its original topology. If the ambient charts and their inverses are C^n, the induced atlas and the inclusion into the ambient manifold are C^n. A subset of a normed space is the case of the space modelled on itself.

The construction requires neither finite dimension nor completeness. It reuses IsSliceChart.subtypeChart; the smooth-atlas argument follows the preferred-chart argument in TauCeti.Geometry.Lie.Subgroup.Manifold, without its group translations.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd edition (2013), Chapter 5.

noncomputable def TauCeti.linearSliceChart {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (x : ↑s) : OpenPartialHomeomorph (↑s) F

The induced chart at a point of the subset. The base point supplies the fallback value of the partial inverse outside the chart target, so no nonemptiness assumption is needed.

Equations

• TauCeti.linearSliceChart e he x = ⋯.subtypeChart

@[simp]

theorem TauCeti.linearSliceChart_source {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (x : ↑s) : (linearSliceChart e he x).source = Subtype.val ⁻¹' (e x).source

The induced chart source is the part of the subset in the ambient source.

@[simp]

theorem TauCeti.linearSliceChart_target {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (x : ↑s) : (linearSliceChart e he x).target = (fun (v : F) => (v, 0)) ⁻¹' (e x).target

The induced chart target is the zero-slice part of the ambient target.

@[simp]

theorem TauCeti.linearSliceChart_apply {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (x y : ↑s) : ↑(linearSliceChart e he x) y = (↑(e x) ↑y).1

The induced chart reads the tangential coordinate of the ambient chart.

@[simp]

theorem TauCeti.coe_linearSliceChart_symm_apply {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (x : ↑s) {v : F} (hv : (v, 0) ∈ (e x).target) : ↑(↑(linearSliceChart e he x).symm v) = ↑(e x).symm (v, 0)

On the target, the induced inverse is the ambient inverse evaluated on the zero slice.

@[instance_reducible]

noncomputable def TauCeti.linearSliceChartedSpace {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (hcover : ∀ (x : ↑s), ↑x ∈ (e x).source) : ChartedSpace F ↑s

A covering family of ambient linear-slice charts gives a charted-space structure on the subset, with its original topology and atlas exactly the induced charts.

Equations

• TauCeti.linearSliceChartedSpace e he hcover = { atlas := Set.range (TauCeti.linearSliceChart e he), chartAt := TauCeti.linearSliceChart e he, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }

@[simp]

theorem TauCeti.linearSliceChartedSpace_atlas {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (hcover : ∀ (x : ↑s), ↑x ∈ (e x).source) : atlas F ↑s = Set.range (linearSliceChart e he)

The atlas consists exactly of the induced linear-slice charts.

@[simp]

theorem TauCeti.linearSliceChartedSpace_chartAt {F : Type u_3} [NormedAddCommGroup F] {G : Type u_4} [NormedAddCommGroup G] {M : Type u_6} [TopologicalSpace M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) (hcover : ∀ (x : ↑s), ↑x ∈ (e x).source) (x : ↑s) : chartAt F x = linearSliceChart e he x

The chosen chart at a point is its induced linear-slice chart.

theorem TauCeti.contDiffOn_linearSliceChart_transition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) {n : WithTop ℕ∞} (hsmooth : ∀ (x : ↑s), ∀ z ∈ (e x).source, ContMDiffAt I (modelWithCornersSelf 𝕜 (F × G)) n (↑(e x)) z) (hinv : ∀ (x : ↑s), ∀ z ∈ (e x).target, ContMDiffAt (modelWithCornersSelf 𝕜 (F × G)) I n (↑(e x).symm) z) (x y : ↑s) : ContDiffOn 𝕜 n (↑((linearSliceChart e he x).symm.trans (linearSliceChart e he y))) ((linearSliceChart e he x).symm.trans (linearSliceChart e he y)).source

Transitions between induced charts insert the zero transverse coordinate, apply the ambient inverse and the other ambient chart, and read the tangential coordinate.

theorem TauCeti.isManifold_linearSliceChartedSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) {n : WithTop ℕ∞} (hsmooth : ∀ (x : ↑s), ∀ z ∈ (e x).source, ContMDiffAt I (modelWithCornersSelf 𝕜 (F × G)) n (↑(e x)) z) (hinv : ∀ (x : ↑s), ∀ z ∈ (e x).target, ContMDiffAt (modelWithCornersSelf 𝕜 (F × G)) I n (↑(e x).symm) z) (hcover : ∀ (x : ↑s), ↑x ∈ (e x).source) : IsManifold (modelWithCornersSelf 𝕜 F) n ↑s

Smooth ambient slice charts induce a C^n manifold structure on the subset.

theorem TauCeti.contMDiff_subtypeVal_linearSliceChartedSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} (e : ↑s → OpenPartialHomeomorph M (F × G)) (he : ∀ (x : ↑s), IsSliceChart (e x) (Set.univ ×ˢ {0}) s) {n : WithTop ℕ∞} (hinv : ∀ (x : ↑s), ∀ z ∈ (e x).target, ContMDiffAt (modelWithCornersSelf 𝕜 (F × G)) I n (↑(e x).symm) z) (hcover : ∀ (x : ↑s), ↑x ∈ (e x).source) : ContMDiff (modelWithCornersSelf 𝕜 F) I n Subtype.val

The inclusion of a subset equipped with its linear-slice atlas is C^n when the ambient inverse charts are C^n.

theorem TauCeti.exists_isManifold_of_linearSubspaceCharts {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {n : WithTop ℕ∞} {L N : Submodule 𝕜 E} (hcompl : Submodule.IsTopCompl L N) (hcharts : ∀ (y : ↑s), ∃ (q : OpenPartialHomeomorph M E), ↑y ∈ q.source ∧ (∀ z ∈ q.source, ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑q) z) ∧ (∀ z ∈ q.target, ContMDiffAt (modelWithCornersSelf 𝕜 E) I n (↑q.symm) z) ∧ ∀ z ∈ q.source, z ∈ s ↔ ↑q z ∈ L) : ∃ (C : ChartedSpace ↥L ↑s), IsManifold (modelWithCornersSelf 𝕜 ↥L) n ↑s ∧ ContMDiff (modelWithCornersSelf 𝕜 ↥L) I n Subtype.val

A subset of a manifold locally flattened onto a complemented linear subspace of the model is a C^n manifold modelled on that subspace, and its inclusion into the ambient manifold is C^n.