Hyperbolic metrics

This file packages the data used by a hyperbolic structure: a smooth Riemannian metric, metric completeness, and the standard constant-curvature tensor with parameter -1 (the tensor form of constant curvature). The metric is bundled so that later volume and Mostow statements can quantify over a chosen metric.

The curvature convention follows Lee, Introduction to Riemannian Manifolds, 2nd edition, Chapter 7.

The curvature predicate is stated for an arbitrary connection and then specialized to the Levi-Civita connection of a bundled metric. This keeps the curvature equation explicit and makes the convention visible: R(w,u)v = κ (⟪u,v⟫ w - ⟪w,v⟫ u).

On a compact manifold completeness is automatic, so there a hyperbolic metric is just a smooth metric of constant curvature -1 (TauCeti.HyperbolicMetric.ofCompactSpace, TauCeti.isHyperbolic_iff_exists_isConstantCurvatureTensor).

structure TauCeti.HyperbolicMetric {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] : Type (max u_1 u_3)

A complete smooth Riemannian metric of constant curvature -1 on M.

• metric : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x

  The smooth Riemannian metric.

• complete : CompleteSpace M

  The metric's own Riemannian distance is metrically complete.

• curvature : self.metric.IsConstantCurvatureTensor (-1)

  The Levi-Civita connection has the constant-curvature tensor with parameter -1.

theorem TauCeti.HyperbolicMetric.ext {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {inst✝² : FiniteDimensional ℝ E} {H : Type u_2} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type u_3} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : T3Space M} {inst✝⁶ : PreconnectedSpace M} {inst✝⁷ : ChartedSpace H M} {inst✝⁸ : IsManifold I (↑⊤) M} {x y : HyperbolicMetric} (metric : x.metric = y.metric) : x = y

theorem TauCeti.HyperbolicMetric.ext_iff {E : Type u_1} {inst✝ : NormedAddCommGroup E} {inst✝¹ : NormedSpace ℝ E} {inst✝² : FiniteDimensional ℝ E} {H : Type u_2} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners ℝ E H} {M : Type u_3} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : T3Space M} {inst✝⁶ : PreconnectedSpace M} {inst✝⁷ : ChartedSpace H M} {inst✝⁸ : IsManifold I (↑⊤) M} {x y : HyperbolicMetric} : x = y ↔ x.metric = y.metric

def TauCeti.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] : Prop

A manifold is hyperbolic when it admits a complete smooth metric of constant curvature -1.

This is the existence predicate used by later hyperbolic-volume and Mostow-rigidity statements; the chosen metric remains available through HyperbolicMetric when a proof is needed.

theorem TauCeti.isHyperbolic_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] : IsHyperbolic ↔ Nonempty HyperbolicMetric

A manifold is hyperbolic exactly when it carries a hyperbolic metric.

def TauCeti.HyperbolicMetric.ofCompactSpace {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] [CompactSpace M] {g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hg : g.IsConstantCurvatureTensor (-1)) : HyperbolicMetric

On a compact manifold every smooth metric of constant curvature -1 is a hyperbolic metric: a compact metric space is complete, so completeness of the Riemannian distance is automatic.

@[simp]

theorem TauCeti.HyperbolicMetric.metric_ofCompactSpace {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] [CompactSpace M] {g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (hg : g.IsConstantCurvatureTensor (-1)) : (ofCompactSpace hg).metric = g

@[simp]

theorem TauCeti.HyperbolicMetric.curvatureTensor_eq {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] (g : HyperbolicMetric) (x : M) (w u v : TangentSpace I x) : ((((CovariantDerivative.leviCivitaConnection I M).curvatureTensor x) w) u) v = -1 • (inner ℝ u v • w - inner ℝ w v • u)

The curvature equation carried by a hyperbolic metric, evaluated at one tangent triple.

@[simp]

theorem TauCeti.HyperbolicMetric.scalarCurvature_metric {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] (g : HyperbolicMetric) (x : M) : g.metric.scalarCurvature x = -(↑(Module.finrank ℝ E) * (↑(Module.finrank ℝ E) - 1))

A hyperbolic metric on a manifold of real dimension n has scalar curvature -n (n - 1).

theorem TauCeti.HyperbolicMetric.scalarCurvature_metric_of_finrank_eq_two {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] (g : HyperbolicMetric) (hE : Module.finrank ℝ E = 2) (x : M) : g.metric.scalarCurvature x = -2

A hyperbolic metric on a surface has scalar curvature -2.

theorem TauCeti.HyperbolicMetric.hasConstantSectionalCurvature {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] (g : HyperbolicMetric) : (CovariantDerivative.leviCivitaConnection I M).HasConstantSectionalCurvature ⋯ (-1)

A hyperbolic metric has constant sectional curvature -1.

theorem TauCeti.isHyperbolic_iff_exists_isConstantCurvatureTensor {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] [CompactSpace M] : IsHyperbolic ↔ ∃ (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x), g.IsConstantCurvatureTensor (-1)

A compact manifold is hyperbolic exactly when it carries a smooth metric of constant curvature -1; completeness is automatic.

theorem TauCeti.IsHyperbolic.exists_scalarCurvature_eq {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] (h : IsHyperbolic) : ∃ (g : HyperbolicMetric), ∀ (x : M), (CovariantDerivative.leviCivitaConnection I M).scalarCurvature x = ↑(Module.finrank ℝ (TangentSpace I x)) * (↑(Module.finrank ℝ (TangentSpace I x)) - 1) * -1

An IsHyperbolic witness has scalar curvature n (n - 1) (-1) in real tangent-space dimension n.

theorem TauCeti.IsHyperbolic.exists_hasConstantSectionalCurvature {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] (h : IsHyperbolic) : ∃ (g : HyperbolicMetric), (CovariantDerivative.leviCivitaConnection I M).HasConstantSectionalCurvature ⋯ (-1)

An IsHyperbolic witness has constant sectional curvature -1.