Isometries are determined by their first-order data

Two Riemannian isometries agreeing in value and differential at a point agree on a neighbourhood of that point and on its whole connected component. On a connected source they agree everywhere. Neither completeness nor compactness is needed.

This uniqueness theorem allows an isometry of a homogeneous space to be identified with a candidate constructed from its value and linear action on one tangent space. In particular it is the uniqueness input to identifying the full isometry groups of the round sphere and the other homogeneous Riemannian models.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Proposition 5.22 (an isometry is determined by its value and differential at one point).

theorem TauCeti.RiemannianIsometry.eventuallyEq_of_mfderiv_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] [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] [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] [J.Boundaryless] [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} (hp : Φ p = Ψ p) (hd : mfderiv% ⇑Φ p = mfderiv% ⇑Ψ p) : ⇑Φ =ᶠ[nhds p] ⇑Ψ

Isometries with the same value and differential at a point agree near that point.

theorem TauCeti.RiemannianIsometry.eqOn_connectedComponent_of_mfderiv_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] [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] [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] [J.Boundaryless] [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} (hp : Φ p = Ψ p) (hd : mfderiv% ⇑Φ p = mfderiv% ⇑Ψ p) : Set.EqOn (⇑Φ) (⇑Ψ) (connectedComponent p)

Isometries with the same value and differential at a point agree on its connected component, even when the source manifold is disconnected.

theorem TauCeti.RiemannianIsometry.ext_of_mfderiv_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] [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] [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] [J.Boundaryless] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsManifold J (↑⊤) N] [IsContMDiffRiemannianBundle J (↑⊤) F fun (y : N) => TangentSpace J y] [PreconnectedSpace M] (Φ Ψ : RiemannianIsometry I J M N) {p : M} (hp : Φ p = Ψ p) (hd : mfderiv% ⇑Φ p = mfderiv% ⇑Ψ p) : Φ = Ψ

Riemannian isometries of a connected manifold are determined by their value and differential at a single point.