Smoothness of charts and local structomorphisms #
We show that the model with corners, charts, extended charts and their inverses are C^n,
and that local structomorphisms are C^n with C^n inverses.
Implementation notes #
This file uses the name writtenInExtend (in analogy to writtenInExtChart) to refer to a
composition ψ.extend J ∘ f ∘ φ.extend I of f : M → N with charts ψ and φ extended by the
appropriate models with corners. This is not a definition, so technically deviating from the naming
convention.
isLocalStructomorphOn is another made-up name.
Atlas members are C^n #
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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
:
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
(h : e ∈ IsManifold.maximalAtlas I n 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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
(h : e ∈ IsManifold.maximalAtlas I n 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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
{x : M}
(h : e ∈ IsManifold.maximalAtlas I n 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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
{x : H}
(h : e ∈ IsManifold.maximalAtlas I n 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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{x : M}
:
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{x : M}
:
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
{x : M}
(he : e ∈ IsManifold.maximalAtlas I n M)
(hx : x ∈ e.source)
:
ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(e.extend I)) x
theorem
contMDiffOn_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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
(he : e ∈ IsManifold.maximalAtlas I n M)
:
ContMDiffOn I (modelWithCornersSelf 𝕜 E) n (↑(e.extend I)) e.source
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{x 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]
{n : WithTop ℕ∞}
{x : M}
:
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{x : M}
:
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{e : OpenPartialHomeomorph M H}
(he : e ∈ IsManifold.maximalAtlas I n 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]
{n : WithTop ℕ∞}
[IsManifold I n M]
(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]
{n : WithTop ℕ∞}
[IsManifold I n M]
(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]
{n : WithTop ℕ∞}
[IsManifold I n M]
(x : M)
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (Set.range ↑I) y
theorem
contMDiffWithinAt_extChartAt_symm_target_self
{𝕜 : 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]
{n : WithTop ℕ∞}
(x : M)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (extChartAt I x).target (↑(extChartAt I x) x)
theorem
contMDiffWithinAt_extChartAt_symm_range_self
{𝕜 : 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]
{n : WithTop ℕ∞}
(x : M)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x)
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 : WithTop ℕ∞}
{e' : OpenPartialHomeomorph H H}
(h : e' ∈ contDiffGroupoid n I)
:
ContMDiffOn I I n (↑e') e'.source
An element of contDiffGroupoid n I is C^n.
(local) structomorphisms are C^n #
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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{M' : Type u_5}
[TopologicalSpace M']
[ChartedSpace H M']
[IsM' : IsManifold I n M']
{f : OpenPartialHomeomorph M M'}
(hf : ChartedSpace.LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source)
:
ContMDiffOn I I n (↑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]
{n : WithTop ℕ∞}
[IsManifold I n M]
{M' : Type u_5}
[TopologicalSpace M']
[ChartedSpace H M']
[IsM' : IsManifold I n M']
(f : OpenPartialHomeomorph M M')
:
ChartedSpace.LiftPropOn (contDiffGroupoid n I).IsLocalStructomorphWithinAt (↑f) f.source ↔ ContMDiffOn I I n (↑f) f.source ∧ ContMDiffOn I I n (↑f.symm) f.target
Let M and M' be 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-C^n on the domain of definition
in both directions.
theorem
OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_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]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_7}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
{f : M → N}
{s : Set M}
{φ : OpenPartialHomeomorph M H}
{ψ : OpenPartialHomeomorph N G}
{y : M}
(hφ : φ ∈ IsManifold.maximalAtlas I n M)
(hψ : ψ ∈ IsManifold.maximalAtlas J n N)
(hy : y ∈ φ.source)
(hgy : f y ∈ ψ.source)
(hmaps : Set.MapsTo f s ψ.source)
:
ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm)
(↑(φ.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(φ.extend I) y) ↔ ContMDiffWithinAt I J n f s y
This is a smooth analogue of OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff.
theorem
OpenPartialHomeomorph.contMDiffOn_writtenInExtend_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]
{F : Type u_6}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type u_7}
[TopologicalSpace G]
{J : ModelWithCorners 𝕜 F G}
{N : Type u_8}
[TopologicalSpace N]
[ChartedSpace G N]
{n : WithTop ℕ∞}
[IsManifold I n M]
[IsManifold J n N]
{f : M → N}
{s : Set M}
{φ : OpenPartialHomeomorph M H}
{ψ : OpenPartialHomeomorph N G}
(hφ : φ ∈ IsManifold.maximalAtlas I n M)
(hψ : ψ ∈ IsManifold.maximalAtlas J n N)
(hs : s ⊆ φ.source)
(hmaps : Set.MapsTo f s ψ.source)
:
ContMDiffOn (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm)
(↑(φ.extend I) '' s) ↔ ContMDiffOn I J n f s