Completeness of homogeneous Riemannian manifolds

If the Riemannian isometry group acts transitively on a locally compact Riemannian manifold, its Riemannian distance is complete. In particular this applies to finite-dimensional homogeneous Riemannian manifolds, including the homogeneous models of three-dimensional geometries. The conclusion concerns the Riemannian distance, rather than an arbitrary metric compatible with the manifold topology.

The argument uses the distance-preserving action and completeness of homogeneous locally compact pseudoemetric spaces. It also applies when different components are at infinite distance and does not require a boundaryless model.

References

• W. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Proposition 3.4.15.
• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983), Sections 4–5.

theorem TauCeti.completeSpace_of_isPretransitive_isom {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] [IsRiemannianManifold I M] [MulAction.IsPretransitive (Isom I M) M] [WeaklyLocallyCompactSpace M] : CompleteSpace M

A homogeneous Riemannian manifold whose topology is weakly locally compact is complete for its Riemannian extended distance.

theorem TauCeti.completeSpace_of_isPretransitive_isom_of_finiteDimensional {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] [IsRiemannianManifold I M] [MulAction.IsPretransitive (Isom I M) M] [FiniteDimensional ℝ E] : CompleteSpace M

Every finite-dimensional homogeneous Riemannian manifold is complete for its Riemannian extended distance.

theorem TauCeti.completeSpace_ofRiemannianMetric_of_isPretransitive_isom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [T3Space M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [MulAction.IsPretransitive (Isom I M) M] : CompleteSpace M

The extended metric constructed from a finite-dimensional homogeneous Riemannian manifold is complete. This installs the Riemannian distance on a manifold that initially carries only a topology.