Maximal geodesics and the exponential map under Riemannian isometries

A smooth Riemannian isometry Φ : M → N carries geodesics with initial data (p, v) to geodesics with initial data (Φ p, dΦ_p v). Consequently it preserves the maximal geodesic interval, intertwines the maximal geodesics, Φ ∘ γ_{p, v} = γ_{Φ p, dΦ_p v}, carries the natural domain of the exponential map at p onto the one at Φ p, and intertwines the exponential maps, Φ ∘ exp_p = exp_{Φ p} ∘ dΦ_p. The identities for the maximal geodesic and the exponential map hold for every time and every tangent vector, since both sides take the same junk value off the natural domains.

This is the naturality of the exponential map under isometries; see J. Lee, Introduction to Riemannian Manifolds, 2nd ed., Chapter 5 (naturality of the exponential map), and do Carmo, Riemannian Geometry, Chapter 3, Section 2, for the exponential map itself.

Main results

• RiemannianIsometry.geodesicInterval_mfderiv: an isometry preserves maximal geodesic intervals.
• RiemannianIsometry.maximalGeodesic_mfderiv: an isometry intertwines maximal geodesics.
• RiemannianIsometry.mfderiv_image_expDomain: the differential of an isometry maps the domain of the exponential map onto the domain at the image point.
• RiemannianIsometry.riemannianExp_mfderiv: an isometry intertwines the exponential maps.

Maximal intervals

@[simp]

theorem TauCeti.RiemannianIsometry.geodesicInterval_mfderiv {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] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E 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] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold J (↑⊤) N] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (p : M) (v : TangentSpace I p) : Manifold.geodesicInterval J N (Φ p) ((mfderiv% ⇑Φ p) v) = Manifold.geodesicInterval I M p v

A smooth Riemannian isometry preserves the maximal geodesic interval: the maximal interval of the geodesic with initial data (Φ p, dΦ_p v) is that of the geodesic with initial data (p, v).

@[simp]

theorem TauCeti.RiemannianIsometry.maximalGeodesic_mfderiv {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] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E 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] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold J (↑⊤) N] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] [I.Boundaryless] [J.Boundaryless] [T2Space M] [T2Space N] (Φ : RiemannianIsometry I J M N) (p : M) (v : TangentSpace I p) (t : ℝ) : Manifold.maximalGeodesic J N (Φ p) ((mfderiv% ⇑Φ p) v) t = Φ (Manifold.maximalGeodesic I M p v t)

A smooth Riemannian isometry intertwines the maximal geodesics with corresponding initial data, at every time t: the identity holds on the common maximal interval, and off it both sides take the junk value Φ p.

The exponential map

theorem TauCeti.RiemannianIsometry.mfderiv_mem_expDomain_iff {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] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E 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] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold J (↑⊤) N] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) {p : M} {v : TangentSpace I p} : (mfderiv% ⇑Φ p) v ∈ Manifold.expDomain J N (Φ p) ↔ v ∈ Manifold.expDomain I M p

A tangent vector at Φ p of the form dΦ_p v lies in the domain of the exponential map at Φ p exactly when v lies in the domain of the exponential map at p.

theorem TauCeti.RiemannianIsometry.mfderiv_image_expDomain {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] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E 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] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold J (↑⊤) N] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) (p : M) : ⇑(mfderiv% ⇑Φ p) '' Manifold.expDomain I M p = Manifold.expDomain J N (Φ p)

The differential of a smooth Riemannian isometry maps the domain of the exponential map at p onto the domain of the exponential map at Φ p.

@[simp]

theorem TauCeti.RiemannianIsometry.riemannianExp_mfderiv {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] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E 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] [FiniteDimensional ℝ F] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold J (↑⊤) N] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] [I.Boundaryless] [J.Boundaryless] [T2Space M] [T2Space N] (Φ : RiemannianIsometry I J M N) (p : M) (v : TangentSpace I p) : Manifold.riemannianExp J N (Φ p) ((mfderiv% ⇑Φ p) v) = Φ (Manifold.riemannianExp I M p v)

A smooth Riemannian isometry intertwines the exponential maps, Φ ∘ exp_p = exp_{Φ p} ∘ dΦ_p, on every tangent vector: the identity holds on the natural domain, and off it both sides take the junk value Φ p.