Documentation

Mathlib.Geometry.Manifold.ContMDiff.Atlas

Smoothness of charts and local structomorphisms #

We show that the model with corners, charts, extended charts and their inverses are smooth, and that local structomorphisms are smooth with smooth inverses.

Atlas members are smooth #

theorem contMDiff_model {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ∞} :
theorem contMDiffOn_model_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ∞} :
ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑I.symm) (Set.range I)
theorem contMDiffOn_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} {n : ℕ∞} (h : e SmoothManifoldWithCorners.maximalAtlas I M) :
ContMDiffOn I I n (↑e) e.source

An atlas member is C^n for any n.

theorem contMDiffOn_symm_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} {n : ℕ∞} (h : e SmoothManifoldWithCorners.maximalAtlas I M) :
ContMDiffOn I I n (↑e.symm) e.target

The inverse of an atlas member is C^n for any n.

theorem contMDiffAt_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} {x : M} {n : ℕ∞} (h : e SmoothManifoldWithCorners.maximalAtlas I M) (hx : x e.source) :
ContMDiffAt I I n (↑e) x
theorem contMDiffAt_symm_of_mem_maximalAtlas {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} {n : ℕ∞} {x : H} (h : e SmoothManifoldWithCorners.maximalAtlas I M) (hx : x e.target) :
ContMDiffAt I I n (↑e.symm) x
theorem contMDiffOn_chart {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {n : ℕ∞} :
ContMDiffOn I I n (↑(chartAt H x)) (chartAt H x).source
theorem contMDiffOn_chart_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {n : ℕ∞} :
ContMDiffOn I I n (↑(chartAt H x).symm) (chartAt H x).target
theorem contMDiffAt_extend {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} {n : ℕ∞} {x : M} (he : e SmoothManifoldWithCorners.maximalAtlas I M) (hx : x e.source) :
ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(e.extend I)) x
theorem contMDiffAt_extChartAt' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {n : ℕ∞} {x' : M} (h : x' (chartAt H x).source) :
ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(extChartAt I x)) x'
theorem contMDiffAt_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {n : ℕ∞} :
ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(extChartAt I x)) x
theorem contMDiffOn_extChartAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {n : ℕ∞} :
ContMDiffOn I (modelWithCornersSelf 𝕜 E) n (↑(extChartAt I x)) (chartAt H x).source
theorem contMDiffOn_extend_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} {n : ℕ∞} (he : e SmoothManifoldWithCorners.maximalAtlas I M) :
ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑(e.extend I).symm) (I '' e.target)
theorem contMDiffOn_extChartAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {n : ℕ∞} (x : M) :
ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (extChartAt I x).target
theorem contMDiffOn_of_mem_contDiffGroupoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : ℕ∞} {e' : PartialHomeomorph H H} (h : e' contDiffGroupoid I) :
ContMDiffOn I I n (↑e') e'.source

An element of contDiffGroupoid ⊤ I is C^n for any n.

Smoothness of (local) structomorphisms #

theorem isLocalStructomorphOn_contDiffGroupoid_iff_aux {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] [IsM' : SmoothManifoldWithCorners I M'] {f : PartialHomeomorph M M'} (hf : ChartedSpace.LiftPropOn (contDiffGroupoid I).IsLocalStructomorphWithinAt (↑f) f.source) :
SmoothOn I I (↑f) f.source
theorem isLocalStructomorphOn_contDiffGroupoid_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H M'] [IsM' : SmoothManifoldWithCorners I M'] (f : PartialHomeomorph M M') :
ChartedSpace.LiftPropOn (contDiffGroupoid I).IsLocalStructomorphWithinAt (↑f) f.source SmoothOn I I (↑f) f.source SmoothOn I I (↑f.symm) f.target

Let M and M' be smooth manifolds with the same model-with-corners, I. Then f : M → M' is a local structomorphism for I, if and only if it is manifold-smooth on the domain of definition in both directions.