Documentation

TauCeti.Geometry.Manifold.Riemannian.Isometry.Tangent

Tangent maps of Riemannian isometries #

The differential of a smooth Riemannian isometry at each point is a linear isometric equivalence of tangent spaces. Its inverse is the differential of the inverse Riemannian isometry. Together with the tangent-bundle diffeomorphism Diffeomorph.tangent, this is the tangent-level transport used for initial velocities and velocity lifts of curves.

Main definitions and results #

source
noncomputable def TauCeti.RiemannianIsometry.mfderivToLinearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (x : M) :
TangentSpace I x ≃ₗᵢ[ℝ] TangentSpace J (Φ x)

The differential of a smooth Riemannian isometry at a point, as a linear isometric equivalence of tangent spaces. Its underlying linear equivalence is Mathlib's Diffeomorph.mfderivToContinuousLinearEquiv, bundled isometrically with Mathlib's LinearEquiv.isometryOfInner.

Instances For
    source
    @[simp]
    theorem TauCeti.RiemannianIsometry.coe_mfderivToLinearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (x : M) :
    ⇑(Φ.mfderivToLinearIsometryEquiv x) = fun (v : TangentSpace I x) => (mfderiv% ⇑Φ x) v

    The underlying function of mfderivToLinearIsometryEquiv is the manifold differential.

    source
    @[simp]
    theorem TauCeti.RiemannianIsometry.mfderivToLinearIsometryEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (x : M) (v : TangentSpace I x) :
    (Φ.mfderivToLinearIsometryEquiv x) v = (mfderiv% ⇑Φ x) v

    Applying mfderivToLinearIsometryEquiv is the same as applying the manifold differential.

    source
    theorem TauCeti.RiemannianIsometry.mfderiv_injective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (x : M) :
    Function.Injective ⇑(mfderiv% ⇑Φ x)

    The differential of a Riemannian isometry at a point is injective.

    source
    theorem TauCeti.RiemannianIsometry.mfderiv_surjective {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (x : M) :
    Function.Surjective ⇑(mfderiv% ⇑Φ x)

    The differential of a Riemannian isometry at a point is surjective onto the tangent space at the image point.

    source
    @[simp]
    theorem TauCeti.RiemannianIsometry.mfderivToLinearIsometryEquiv_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (x : M) (v : TangentSpace J (Φ x)) :
    (Φ.mfderivToLinearIsometryEquiv x).symm v = (mfderiv% ⇑Φ.symm (Φ x)) v

    The inverse of the differential equivalence is the differential of the inverse Riemannian isometry at Φ x.

    source
    theorem TauCeti.RiemannianIsometry.toDiffeomorph_tangent_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold I 1 M] [IsManifold J 1 N] (Φ : RiemannianIsometry I J M N) (z : TangentBundle I M) :
    Φ.tangent z = ⟨Φ z.proj, (Φ.mfderivToLinearIsometryEquiv z.proj) z.snd⟩

    The tangent-bundle lift of a Riemannian isometry uses its fibrewise linear isometric equivalence on tangent vectors.