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 : ℕ∞}
:
ContMDiff I (modelWithCornersSelf 𝕜 E) n ↑I
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
contMDiffWithinAt_extChartAt_symm_target
{𝕜 : 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)
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (extChartAt I x).target y
theorem
contMDiffWithinAt_extChartAt_symm_range
{𝕜 : 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)
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (Set.range ↑I) y
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_5}
[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_5}
[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.