Riemannian isometries preserve distance

A smooth Riemannian isometry preserves the length of each curve. Applying this fact to curves in both directions shows that it preserves the infimum of their lengths, even when that infimum is infinite because the points lie in different components. When the ambient extended distances are the Riemannian distances, the smooth isometry is also an isometry of extended metric spaces.

The geometric fact is the invariance of Riemannian distance under isometries; see J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Chapter 2.

@[simp]

theorem TauCeti.RiemannianIsometry.riemannianEDist_eq {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 y : M) : Manifold.riemannianEDist J (Φ x) (Φ y) = Manifold.riemannianEDist I x y

A smooth Riemannian isometry preserves Riemannian extended distance, including between points in distinct connected components.

instance TauCeti.RiemannianIsometry.instIsometryClass {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [hM : IsRiemannianManifold I M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [PseudoEMetricSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [hN : IsRiemannianManifold J N] : IsometryClass (RiemannianIsometry I J M N) M N

A smooth Riemannian isometry between spaces equipped with their Riemannian extended distances is an isometry of extended metric spaces; in particular it coerces to M ≃ᵢ N.

@[simp]

theorem TauCeti.RiemannianIsometry.toIsometryEquiv_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [hM : IsRiemannianManifold I M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [PseudoEMetricSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [hN : IsRiemannianManifold J N] (Φ : RiemannianIsometry I J M N) : ↑Φ.symm = (↑Φ).symm

The metric equivalence of the inverse is the inverse metric equivalence.

@[simp]

theorem TauCeti.RiemannianIsometry.toIsometryEquiv_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [hM : IsRiemannianManifold I M] : ↑(RiemannianIsometry.refl I M) = IsometryEquiv.refl M

The identity Riemannian isometry induces the identity metric equivalence.

@[simp]

theorem TauCeti.RiemannianIsometry.toIsometryEquiv_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [hM : IsRiemannianManifold I M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [PseudoEMetricSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [hN : IsRiemannianManifold J N] {G : Type u_7} [NormedAddCommGroup G] [NormedSpace ℝ G] {H'' : Type u_8} [TopologicalSpace H''] {K : ModelWithCorners ℝ G H''} {P : Type u_9} [PseudoEMetricSpace P] [ChartedSpace H'' P] [Bundle.RiemannianBundle fun (z : P) => TangentSpace K z] [hP : IsRiemannianManifold K P] (Φ : RiemannianIsometry I J M N) (Ψ : RiemannianIsometry J K N P) : ↑(Φ.trans Ψ) = (↑Φ).trans ↑Ψ

The metric equivalence of a composite is the composite metric equivalence.