Completeness of homogeneous locally compact spaces

A transitive action by isometries moves a compact neighbourhood of one point to a compact neighbourhood of every point, with the same radius. A Cauchy filter eventually lies in one of these compact balls, and therefore converges. This proves completeness without assuming that the action depends continuously on the group parameter, or that distances are finite.

This metric argument is the completeness mechanism for homogeneous Riemannian model spaces. Compare W. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Proposition 3.4.15, conditions (b) and (e).

The Cauchy-filter argument follows Mathlib's complete_of_proper in Mathlib/Topology/MetricSpace/ProperSpace.lean, using compact balls of one uniform radius in place of properness.

theorem TauCeti.exists_pos_isCompact_closedEBall_of_isPretransitive (G : Type u_1) (X : Type u_2) [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] [MulAction.IsPretransitive G X] [WeaklyLocallyCompactSpace X] : ∃ (r : ENNReal), 0 < r ∧ ∀ (y : X), IsCompact (Metric.closedEBall y r)

In a weakly locally compact space with a transitive isometric action, there is a positive radius for which every closed ball is compact.

theorem TauCeti.completeSpace_of_isIsometricSMul_of_isPretransitive (G : Type u_1) (X : Type u_2) [PseudoEMetricSpace X] [Group G] [MulAction G X] [IsIsometricSMul G X] [MulAction.IsPretransitive G X] [WeaklyLocallyCompactSpace X] : CompleteSpace X

A weakly locally compact pseudoemetric space with a transitive action by isometries is complete. The action need not be jointly continuous.