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 a partial homeomorphism e is differentiable. This file shows
PartialHomeomorph.MDifferentiable.mfderiv: its derivative is a continuous linear equivalencePartialHomeomorph.MDifferentiable.mfderiv_bijective: its derivative is bijective; there are also spelling 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 (modelWithCornersSelf 𝕜 E) (↑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}
:
HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 E) (↑I) s 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}
:
MDifferentiableWithinAt I (modelWithCornersSelf 𝕜 E) (↑I) s 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}
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E) (↑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}
:
MDifferentiableOn I (modelWithCornersSelf 𝕜 E) (↑I) s
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)
:
MDifferentiable I (modelWithCornersSelf 𝕜 E) ↑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)
:
HasMFDerivWithinAt (modelWithCornersSelf 𝕜 E) I (↑I.symm) (Set.range ↑I) 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)
:
MDifferentiableOn (modelWithCornersSelf 𝕜 E) I (↑I.symm) (Set.range ↑I)
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)
:
MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) I (↑I.symm) (Set.range ↑I) z
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]
[IsManifold I 1 M]
{e : PartialHomeomorph M H}
(h : e ∈ atlas H M)
{x : M}
(hx : x ∈ e.source)
:
MDifferentiableAt I I (↑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]
[IsManifold I 1 M]
{e : PartialHomeomorph M H}
(h : e ∈ atlas H M)
:
MDifferentiableOn I I (↑e) e.source
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]
[IsManifold I 1 M]
{e : PartialHomeomorph M H}
(h : e ∈ atlas H M)
{x : H}
(hx : x ∈ e.target)
:
MDifferentiableAt I I (↑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]
[IsManifold I 1 M]
{e : PartialHomeomorph M H}
(h : e ∈ atlas H M)
:
MDifferentiableOn I I (↑e.symm) e.target
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]
[IsManifold I 1 M]
{e : PartialHomeomorph M H}
(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)
:
PartialHomeomorph.MDifferentiable I I (chartAt H x)
Differentiable partial homeomorphisms #
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
:
MDifferentiable I' I e.symm
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
MDifferentiableAt I I' (↑e) x
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M'}
(hx : x ∈ e.target)
:
MDifferentiableAt I' I (↑e.symm) x
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
(mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M'}
(hx : x ∈ e.target)
:
(mfderiv I I' (↑e) (↑e.symm x)).comp (mfderiv I' I (↑e.symm) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I' x)
def
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
The derivative of a differentiable partial homeomorphism, as a continuous linear equivalence
between the tangent spaces at x and e x.
Equations
Instances For
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
Function.Bijective ⇑(mfderiv I I' (↑e) x)
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
Function.Injective ⇑(mfderiv I I' (↑e) x)
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
Function.Surjective ⇑(mfderiv I I' (↑e) x)
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{x : M}
(hx : x ∈ e.source)
:
theorem
PartialHomeomorph.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 : PartialHomeomorph M M'}
(he : MDifferentiable I I' e)
{e' : PartialHomeomorph M' M''}
(he' : MDifferentiable I' I'' e')
:
MDifferentiable I I'' (e.trans e')
Differentiability of extChartAt #
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 I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) y (mfderiv I I (↑(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)
:
HasMFDerivWithinAt I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) s y (mfderiv I I (↑(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)
:
MDifferentiableAt I (modelWithCornersSelf 𝕜 E) (↑(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}
:
MDifferentiableOn I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) (chartAt H x).source
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)
:
MDifferentiableWithinAt (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) 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}
:
MDifferentiableOn (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (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 : M}
{y : E}
(hy : y ∈ (extChartAt I x).target)
:
(mfderiv I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)).comp
(mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) 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 I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) y).comp
(mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) (↑(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)
:
(mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) y).comp
(mfderiv I (modelWithCornersSelf 𝕜 E) (↑(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)
:
(mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) y)).comp
(mfderiv I (modelWithCornersSelf 𝕜 E) (↑(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)
:
(mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x).symm) (Set.range ↑I) 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 I (modelWithCornersSelf 𝕜 E) (↑(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)
:
Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x = mfderiv I (modelWithCornersSelf 𝕜 E) (↑(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)
:
Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x₀) x = mfderivWithin (modelWithCornersSelf 𝕜 E) I (↑(extChartAt I x₀).symm) (Set.range ↑I) (↑(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.