Geodesics under Riemannian isometries

A local Riemannian isometry carries geodesics to geodesics. This holds on an arbitrary parameter set with unique derivatives, and the tangent map carries the initial velocity to the initial velocity of the image geodesic. For a global isometry, applying the result to its inverse gives equivalences for interval-aware geodesics, all-time geodesics, and geodesics with initial data.

This is the geodesic form of naturality of the Levi-Civita connection; see do Carmo, Riemannian Geometry, Chapter 2, Theorem 3.6, and Chapter 3, Section 2. The equivalence for geodesics with prescribed initial data is the input for showing that an isometry preserves maximal geodesic intervals and intertwines the exponential maps, Φ ∘ exp_p = exp_{Φ p} ∘ dΦ_p.

Main results

• IsLocalRiemannianIsometry.isGeodesicCurveOn_comp: local isometries preserve geodesics.
• IsLocalRiemannianIsometry.isGeodesicCurveOn_comp_iff: reflection for C² source curves.
• RiemannianIsometry.isGeodesicCurveOn_comp_iff: an isometry preserves the geodesic equation on a parameter set.
• RiemannianIsometry.isGeodesicCurve_comp_iff: the all-time specialization.
• RiemannianIsometry.isGeodesicCurveOnFrom_comp_iff: the initial point and velocity are carried by the isometry and its differential.

theorem TauCeti.IsLocalRiemannianIsometry.isGeodesicCurveOn_comp {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] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] {f : M → N} (hf : IsLocalRiemannianIsometry I J f) {γ : ℝ → M} {s : Set ℝ} (h : Manifold.IsGeodesicCurveOn I γ s) : Manifold.IsGeodesicCurveOn J (f ∘ γ) s

A local Riemannian isometry carries geodesics to geodesics on the same parameter set.

theorem TauCeti.IsLocalRiemannianIsometry.isGeodesicCurveOn_comp_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] [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] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] {f : M → N} (hf : IsLocalRiemannianIsometry I J f) {γ : ℝ → M} {s : Set ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s) : Manifold.IsGeodesicCurveOn J (f ∘ γ) s ↔ Manifold.IsGeodesicCurveOn I γ s

A C² curve is a geodesic exactly when its image under a local Riemannian isometry is. The source regularity prevents discontinuous changes between different local sheets.

@[simp]

theorem TauCeti.RiemannianIsometry.isGeodesicCurveOn_comp_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] [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] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) {γ : ℝ → M} {s : Set ℝ} : Manifold.IsGeodesicCurveOn J (⇑Φ ∘ γ) s ↔ Manifold.IsGeodesicCurveOn I γ s

A smooth Riemannian isometry preserves the geodesic equation on every parameter set with unique derivatives.

@[simp]

theorem TauCeti.RiemannianIsometry.isGeodesicCurve_comp_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] [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] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) {γ : ℝ → M} : Manifold.IsGeodesicCurve J (⇑Φ ∘ γ) ↔ Manifold.IsGeodesicCurve I γ

A smooth Riemannian isometry preserves all-time geodesics.

@[simp]

theorem TauCeti.RiemannianIsometry.isGeodesicCurveOnFrom_comp_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] [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] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) {γ : ℝ → M} {s : Set ℝ} {p : M} {v : TangentSpace I p} : Manifold.IsGeodesicCurveOnFrom J (⇑Φ ∘ γ) s (Φ p) ((mfderiv% ⇑Φ p) v) ↔ Manifold.IsGeodesicCurveOnFrom I γ s p v

A smooth Riemannian isometry carries the initial point of a geodesic to its image and the initial velocity through its differential.