Differentiability of models with corners and (extended) charts #
In this file, we analyse the differentiability of charts, models with corners and extended charts. We show that
- models with corners are differentiable
- charts are differentiable on their source
mdifferentiableOn_extChartAt:extChartAtis differentiable on its source
Suppose an open partial homeomorphism e is differentiable. This file shows
OpenPartialHomeomorph.MDifferentiable.mfderiv: its derivative is a continuous linear equivalenceOpenPartialHomeomorph.MDifferentiable.mfderiv_bijective: its derivative is bijective; there are also spellings with trivial kernel and full range
In particular, (extended) charts have bijective differential.
Tags #
charts, differentiable, bijective
Model with corners #
theorem
ModelWithCorners.hasMFDerivAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{x : H}
:
HasMFDerivAt% (↑I) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
theorem
ModelWithCorners.hasMFDerivWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{s : Set H}
{x : H}
:
HasMFDerivAt[s] (↑I) x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
theorem
ModelWithCorners.mdifferentiableWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{s : Set H}
{x : H}
:
MDiffAt[s] ↑I x
theorem
ModelWithCorners.mdifferentiableAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{x : H}
:
MDiffAt ↑I x
theorem
ModelWithCorners.mdifferentiableOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{s : Set H}
:
MDiff[s] ↑I
theorem
ModelWithCorners.mdifferentiable
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
:
MDiff ↑I
theorem
ModelWithCorners.hasMFDerivWithinAt_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{x : E}
(hx : x ∈ Set.range ↑I)
:
HasMFDerivAt[Set.range ↑I] (↑I.symm) x (ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) x))
theorem
ModelWithCorners.mdifferentiableOn_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
:
theorem
ModelWithCorners.mdifferentiableWithinAt_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{H : Type u_3}
[TopologicalSpace H]
(I : ModelWithCorners 𝕜 E H)
{z : E}
(hz : z ∈ Set.range ↑I)
:
theorem
mdifferentiableAt_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]
{e : OpenPartialHomeomorph M H}
(h : e ∈ IsManifold.maximalAtlas I 1 M)
{x : M}
(hx : x ∈ e.source)
:
MDiffAt ↑e x
theorem
mdifferentiableAt_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]
{e : OpenPartialHomeomorph M H}
(h : e ∈ IsManifold.maximalAtlas I 1 M)
{x : H}
(hx : x ∈ e.target)
:
MDiffAt ↑e.symm x
theorem
mdifferentiableAt_atlas
{𝕜 : 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]
{e : OpenPartialHomeomorph M H}
[IsManifold I 1 M]
(h : e ∈ atlas H M)
{x : M}
(hx : x ∈ e.source)
:
MDiffAt ↑e x
theorem
mdifferentiableOn_atlas
{𝕜 : 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]
{e : OpenPartialHomeomorph M H}
[IsManifold I 1 M]
(h : e ∈ atlas H M)
:
MDiff[e.source] ↑e
theorem
mdifferentiableAt_atlas_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]
{e : OpenPartialHomeomorph M H}
[IsManifold I 1 M]
(h : e ∈ atlas H M)
{x : H}
(hx : x ∈ e.target)
:
MDiffAt ↑e.symm x
theorem
mdifferentiableOn_atlas_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]
{e : OpenPartialHomeomorph M H}
[IsManifold I 1 M]
(h : e ∈ atlas H M)
:
theorem
mdifferentiable_of_mem_atlas
{𝕜 : 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]
{e : OpenPartialHomeomorph M H}
[IsManifold I 1 M]
(h : e ∈ atlas H M)
:
theorem
mdifferentiable_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]
[IsManifold I 1 M]
(x : M)
:
OpenPartialHomeomorph.MDifferentiable I I (chartAt H x)
Differentiable open partial homeomorphisms #
theorem
OpenPartialHomeomorph.MDifferentiable.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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
:
MDifferentiable I' I e.symm
theorem
OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
MDiffAt ↑e x
theorem
OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt_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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M'}
(hx : x ∈ e.target)
:
MDiffAt ↑e.symm x
theorem
OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M'}
(hx : x ∈ e.target)
:
noncomputable def
OpenPartialHomeomorph.MDifferentiable.mfderiv
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
The derivative of a differentiable open partial homeomorphism, as a continuous linear
equivalence between the tangent spaces at x and e x.
Equations
Instances For
theorem
OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
Function.Bijective ⇑(mfderiv% ↑e x)
theorem
OpenPartialHomeomorph.MDifferentiable.mfderiv_injective
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
Function.Injective ⇑(mfderiv% ↑e x)
theorem
OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
Function.Surjective ⇑(mfderiv% ↑e x)
theorem
OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
OpenPartialHomeomorph.MDifferentiable.trans
{𝕜 : 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]
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{H' : Type u_6}
[TopologicalSpace H']
{I' : ModelWithCorners 𝕜 E' H'}
{M' : Type u_7}
[TopologicalSpace M']
[ChartedSpace H' M']
{E'' : Type u_8}
[NormedAddCommGroup E'']
[NormedSpace 𝕜 E'']
{H'' : Type u_9}
[TopologicalSpace H'']
{I'' : ModelWithCorners 𝕜 E'' H''}
{M'' : Type u_10}
[TopologicalSpace M'']
[ChartedSpace H'' M'']
{e : OpenPartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{e' : OpenPartialHomeomorph M' M''}
(he' : MDifferentiable I' I'' e')
:
MDifferentiable I I'' (e.trans e')
Differentiability of extChartAt #
theorem
OpenPartialHomeomorph.mdifferentiableAt_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]
{e : OpenPartialHomeomorph M H}
{x : M}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hx : x ∈ e.source)
:
MDiffAt ↑(e.extend I) x
theorem
OpenPartialHomeomorph.mdifferentiableOn_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]
{e : OpenPartialHomeomorph M H}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
:
theorem
mdifferentiableWithinAt_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]
{e : OpenPartialHomeomorph M H}
{z : E}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(h : z ∈ (e.extend I).target)
:
theorem
mdifferentiableOn_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]
{e : OpenPartialHomeomorph M H}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
:
theorem
mfderiv_extend_comp_mfderivWithin_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]
{e : OpenPartialHomeomorph M H}
{y : E}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hy : y ∈ (e.extend I).target)
:
mfderiv% ↑(e.extend I) (↑(e.extend I).symm y) ∘SL mfderiv[Set.range ↑I] ↑(e.extend I).symm y = ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) y)
The composition of the derivative of an extended chart e.extend I with the derivative of its
inverse (e.extend I).symm gives the identity.
Version where the basepoint belongs to (e.extend I).target.
theorem
mfderiv_extend_comp_mfderivWithin_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]
{e : OpenPartialHomeomorph M H}
{y : M}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hy : y ∈ (e.extend I).source)
:
mfderiv% ↑(e.extend I) y ∘SL mfderiv[Set.range ↑I] ↑(e.extend I).symm (↑(e.extend I) y) = ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) (↑(e.extend I) y))
The composition of the derivative of an extended chart e.extend I with the derivative of its
inverse (e.extend I).symm gives the identity.
Version where the basepoint belongs to (e.extend).source.
theorem
mfderivWithin_extend_symm_comp_mfderiv_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]
{e : OpenPartialHomeomorph M H}
{y : E}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hy : y ∈ (e.extend I).target)
:
The composition of the derivative of the inverse of an extended chart e.extend I with the
derivative of e.extend I gives the identity.
Version where the basepoint belongs to (extChartAt I x).target.
theorem
mfderivWithin_extend_symm_comp_mfderiv_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]
{e : OpenPartialHomeomorph M H}
{y : M}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hy : y ∈ e.source)
:
mfderiv[Set.range ↑I] ↑(e.extend I).symm (↑(e.extend I) y) ∘SL mfderiv% ↑(e.extend I) y = ContinuousLinearMap.id 𝕜 (TangentSpace I y)
The composition of the derivative of the inverse of an extended chart e.extend I with the
derivative of e.extend I gives the identity.
Version where the basepoint belongs to e.source.
theorem
isInvertible_mfderivWithin_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]
{e : OpenPartialHomeomorph M H}
{y : E}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hy : y ∈ (e.extend I).target)
:
(mfderiv[Set.range ↑I] ↑(e.extend I).symm y).IsInvertible
theorem
isInvertible_mfderiv_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]
{e : OpenPartialHomeomorph M H}
{y : M}
(he : e ∈ IsManifold.maximalAtlas I 1 M)
(hy : y ∈ e.source)
:
(mfderiv% ↑(e.extend I) y).IsInvertible
theorem
hasMFDerivAt_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]
[IsManifold I 1 M]
{x y : M}
(h : y ∈ (chartAt H x).source)
:
HasMFDerivAt% (↑(extChartAt I x)) y (mfderiv% ↑(chartAt H x) y)
theorem
hasMFDerivWithinAt_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]
[IsManifold I 1 M]
{s : Set M}
{x y : M}
(h : y ∈ (chartAt H x).source)
:
HasMFDerivAt[s] (↑(extChartAt I x)) y (mfderiv% ↑(chartAt H x) y)
theorem
mdifferentiableAt_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]
[IsManifold I 1 M]
{x y : M}
(h : y ∈ (chartAt H x).source)
:
MDiffAt ↑(extChartAt I x) y
theorem
mdifferentiableOn_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]
[IsManifold I 1 M]
{x : M}
:
MDiff[(chartAt H x).source] ↑(extChartAt I x)
theorem
mdifferentiableWithinAt_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]
[IsManifold I 1 M]
{x : M}
{z : E}
(h : z ∈ (extChartAt I x).target)
:
MDiffAt[Set.range ↑I] ↑(extChartAt I x).symm z
theorem
mdifferentiableOn_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]
[IsManifold I 1 M]
{x : M}
:
MDiff[(extChartAt I x).target] ↑(extChartAt I x).symm
theorem
mfderiv_extChartAt_comp_mfderivWithin_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]
[IsManifold I 1 M]
{x : M}
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y = ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) y)
The composition of the derivative of extChartAt with the derivative of the inverse of
extChartAt gives the identity.
Version where the basepoint belongs to (extChartAt I x).target.
theorem
mfderiv_extChartAt_comp_mfderivWithin_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]
[IsManifold I 1 M]
{x y : M}
(hy : y ∈ (extChartAt I x).source)
:
mfderiv% ↑(extChartAt I x) y ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) = ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x) y))
The composition of the derivative of extChartAt with the derivative of the inverse of
extChartAt gives the identity.
Version where the basepoint belongs to (extChartAt I x).source.
theorem
mfderivWithin_extChartAt_symm_comp_mfderiv_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]
[IsManifold I 1 M]
{x : M}
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y ∘SL mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) = ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))
The composition of the derivative of the inverse of extChartAt with the derivative of
extChartAt gives the identity.
Version where the basepoint belongs to (extChartAt I x).target.
theorem
mfderivWithin_extChartAt_symm_comp_mfderiv_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]
[IsManifold I 1 M]
{x y : M}
(hy : y ∈ (extChartAt I x).source)
:
mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y) ∘SL mfderiv% ↑(extChartAt I x) y = ContinuousLinearMap.id 𝕜 (TangentSpace I y)
The composition of the derivative of the inverse of extChartAt with the derivative of
extChartAt gives the identity.
Version where the basepoint belongs to (extChartAt I x).source.
theorem
isInvertible_mfderivWithin_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]
[IsManifold I 1 M]
{x : M}
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
(mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y).IsInvertible
theorem
isInvertible_mfderiv_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]
[IsManifold I 1 M]
{x y : M}
(hy : y ∈ (extChartAt I x).source)
:
(mfderiv% ↑(extChartAt I x) y).IsInvertible
theorem
TangentBundle.continuousLinearMapAt_trivializationAt
{𝕜 : 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]
[IsManifold I 1 M]
{x₀ x : M}
(hx : x ∈ (chartAt H x₀).source)
:
Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x = mfderiv% ↑(extChartAt I x₀) x
The trivialization of the tangent bundle at a point is the manifold derivative of the
extended chart.
Use with care as this abuses the defeq TangentSpace 𝓘(𝕜, E) y = E for y : E.
theorem
TangentBundle.symmL_trivializationAt
{𝕜 : 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]
[IsManifold I 1 M]
{x₀ x : M}
(hx : x ∈ (chartAt H x₀).source)
:
Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x₀) x = mfderiv[Set.range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x)
The inverse trivialization of the tangent bundle at a point is the manifold derivative of the
inverse of the extended chart.
Use with care as this abuses the defeq TangentSpace 𝓘(𝕜, E) y = E for y : E.
theorem
fderivWithin_extChartAt_comp_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]
{x : M}
:
fderivWithin 𝕜 (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) x) = ContinuousLinearMap.id 𝕜 E
The fderivWithin of the round-trip composition (extChartAt I x) ∘ (extChartAt I x).symm
at the chart point in range I equals the identity.
theorem
mfderiv_extChartAt_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]
[IsManifold I 1 M]
{x : M}
:
The manifold derivative of extChartAt at the basepoint is the identity.
theorem
mfderivWithin_range_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]
[IsManifold I 1 M]
{x : M}
:
mfderiv[Set.range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) x) = ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x) x))
The manifold derivative within range I of (extChartAt I x).symm at the chart point is
the identity.
theorem
mfderivWithin_extChartAt_symm_inverse_apply
{𝕜 : 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]
[IsManifold I 1 M]
{x : M}
(v : TangentSpace I x)
:
The inverse of the derivative of (extChartAt I x).symm at the chart point,
applied to a tangent vector, gives back the tangent vector.