Hyperbolic metrics of finite volume

A complete hyperbolic manifold need not be compact: the complement of a hyperbolic knot in S³, and more generally the interior of every non-Seifert-fibred piece of the geometric (JSJ) decomposition of a closed orientable irreducible 3-manifold, carries a complete hyperbolic metric of finite volume, with cusps at its ends. This is the notion of hyperbolicity in the geometrization theorem. This file records it, for the Riemannian volume measure TauCeti.riemannianVolume of the bundled metric.

On a compact manifold the Riemannian volume is a finite measure, so there the condition is automatic, and a compact manifold is hyperbolic of finite volume exactly when it is hyperbolic.

Main definitions

• TauCeti.HyperbolicMetric.HasFiniteVolume: the Riemannian volume of a hyperbolic metric is a finite measure.
• TauCeti.IsFiniteVolumeHyperbolic: a manifold carries a hyperbolic metric of finite volume.

Main results

• TauCeti.isFiniteVolumeHyperbolic_iff: the definition, for any Borel measurable structure.
• TauCeti.HyperbolicMetric.hasFiniteVolume_of_compactSpace: on a compact manifold every hyperbolic metric has finite volume.
• TauCeti.isFiniteVolumeHyperbolic_iff_isHyperbolic: so a compact manifold is hyperbolic of finite volume exactly when it is hyperbolic.

References

• W. P. Thurston, Three-dimensional manifolds, Kleinian groups and hyperbolic geometry, Bull. Amer. Math. Soc. (N.S.) 6 (1982), 357–381.
• J. G. Ratcliffe, Foundations of Hyperbolic Manifolds, 3rd ed., Graduate Texts in Mathematics 149, Springer (2019), Chapter 10 (hyperbolic 3-manifolds).

def TauCeti.HyperbolicMetric.HasFiniteVolume {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] [MeasurableSpace M] [BorelSpace M] (g : HyperbolicMetric) : Prop

A hyperbolic metric has finite volume when its Riemannian volume measure is finite.

theorem TauCeti.HyperbolicMetric.hasFiniteVolume_iff {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] [MeasurableSpace M] [BorelSpace M] (g : HyperbolicMetric) : g.HasFiniteVolume ↔ MeasureTheory.IsFiniteMeasure (riemannianVolume I M)

The defining property of TauCeti.HyperbolicMetric.HasFiniteVolume.

theorem TauCeti.HyperbolicMetric.hasFiniteVolume_of_compactSpace {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] [MeasurableSpace M] [BorelSpace M] [CompactSpace M] (g : HyperbolicMetric) : g.HasFiniteVolume

On a compact manifold every hyperbolic metric has finite volume, since the Riemannian volume is locally finite.

def TauCeti.IsFiniteVolumeHyperbolic {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] : Prop

A manifold is hyperbolic of finite volume when it carries a complete smooth metric of constant curvature -1 whose Riemannian volume is finite. The volume is taken for the Borel σ-algebra; TauCeti.isFiniteVolumeHyperbolic_iff restates this for any Borel measurable structure on M.

theorem TauCeti.isFiniteVolumeHyperbolic_iff {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] [MeasurableSpace M] [BorelSpace M] : IsFiniteVolumeHyperbolic I M ↔ ∃ (g : HyperbolicMetric), g.HasFiniteVolume

A manifold is hyperbolic of finite volume exactly when it carries a hyperbolic metric of finite volume, computed for any Borel measurable structure.

theorem TauCeti.IsFiniteVolumeHyperbolic.isHyperbolic {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] (h : IsFiniteVolumeHyperbolic I M) : IsHyperbolic

A manifold that is hyperbolic of finite volume is hyperbolic.

theorem TauCeti.isFiniteVolumeHyperbolic_iff_isHyperbolic {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] [T3Space M] [PreconnectedSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [LindelofSpace M] [CompactSpace M] : IsFiniteVolumeHyperbolic I M ↔ IsHyperbolic

A compact manifold is hyperbolic of finite volume exactly when it is hyperbolic: on a compact manifold every hyperbolic metric has finite volume.