Documentation

Mathlib.Geometry.Manifold.MFDeriv.Atlas

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

Suppose a partial homeomorphism e is differentiable. This file shows

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} :
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} :
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} :
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} :
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} :
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) :
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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I 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] [SmoothManifoldWithCorners I M] {e : PartialHomeomorph M H} (h : e atlas H M) :
MDifferentiableOn I I (↑e.symm) e.target
theorem tangentMap_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] {p : TangentBundle I M} {q : TangentBundle I M} (h : q.proj (chartAt H p.proj).source) :
tangentMap I I (↑(chartAt H p.proj)) q = (Bundle.TotalSpace.toProd H E).symm ((chartAt (ModelProd H E) p) q)

The derivative of the chart at a base point is the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.

theorem tangentMap_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] {p : TangentBundle I M} {q : TangentBundle I H} (h : q.proj (chartAt H p.proj).target) :
tangentMap I I (↑(chartAt H p.proj).symm) q = (chartAt (ModelProd H E) p).symm ((Bundle.TotalSpace.toProd H E) q)

The derivative of the inverse of the chart at a base point is the inverse of the chart of the tangent bundle, composed with the identification between the tangent bundle of the model space and the product space.

theorem mfderiv_chartAt_eq_tangentCoordChange {𝕜 : 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} {y : M} (hsrc : x (chartAt H y).source) :
mfderiv I I (↑(chartAt H y)) x = tangentCoordChange I x y 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 : PartialHomeomorph.MDifferentiable I I' e) :
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 : PartialHomeomorph.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 : PartialHomeomorph.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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {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'} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] (he : PartialHomeomorph.MDifferentiable I I' e) {x : M} (hx : x e.source) :
TangentSpace I x ≃L[𝕜] TangentSpace I' (e x)

The derivative of a differentiable partial homeomorphism, as a continuous linear equivalence between the tangent spaces at x and e x.

Equations
  • he.mfderiv hx = { toLinearMap := (mfderiv I I' (↑e) x), invFun := (mfderiv I' I (↑e.symm) (e x)), left_inv := , right_inv := , continuous_toFun := , continuous_invFun := }
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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} (hx : x e.source) :
    LinearMap.ker (mfderiv I I' (↑e) x) =
    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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} (hx : x e.source) :
    LinearMap.range (mfderiv I I' (↑e) x) =
    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 : PartialHomeomorph.MDifferentiable I I' e) [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] {x : M} (hx : x e.source) :
    Set.range (mfderiv I I' (↑e) x) = Set.univ
    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 : PartialHomeomorph.MDifferentiable I I' e) {e' : PartialHomeomorph M' M''} [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] [SmoothManifoldWithCorners I'' M''] (he' : PartialHomeomorph.MDifferentiable I' I'' e') :

    Differentiability of extChartAt #

    theorem hasMFDerivAt_extChartAt {𝕜 : Type u_11} [NontriviallyNormedField 𝕜] {E : Type u_12} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_13} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {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_11} [NontriviallyNormedField 𝕜] {E : Type u_12} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_13} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {s : Set M} {x : M} {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_11} [NontriviallyNormedField 𝕜] {E : Type u_12} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_13} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} {y : M} (h : y (chartAt H x).source) :
    theorem mdifferentiableOn_extChartAt {𝕜 : Type u_11} [NontriviallyNormedField 𝕜] {E : Type u_12} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_13} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_14} [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] {x : M} :
    MDifferentiableOn I (modelWithCornersSelf 𝕜 E) (↑(extChartAt I x)) (chartAt H x).source