Hyperbolic metrics in a conformal class of a closed surface

Let g be a smooth Riemannian metric on a closed connected surface M. A hyperbolic metric conformal to g is a TauCeti.HyperbolicMetric whose metric is f g for a smooth positive function f. This file identifies these hyperbolic metrics with the smooth solutions of the curvature equation

Δ⁺φ + K + e^(2φ) = 0,

where Δ⁺ = -div grad is the nonnegative Laplacian of g and K = Scal^g / 2 its Gaussian curvature, the hyperbolic metric being e^(2φ) g. The only property of a hyperbolic metric beyond its curvature, completeness, holds automatically on a closed surface, since the Riemannian distance of a compact manifold is complete (TauCeti.HyperbolicMetric.ofCompactSpace). Finite volume then follows separately (TauCeti.HyperbolicMetric.hasFiniteVolume_of_compactSpace). So the existence of a hyperbolic metric in the conformal class of g is equivalent to the solvability of the curvature equation, and by the maximum principle there is at most one such metric. Since total curvature is a conformal invariant of a closed surface, the area of this metric is -∫ K dV_g.

Main results

• Bundle.ContMDiffRiemannianMetric.exists_hyperbolicMetric_metric_eq_rescale_iff: a closed surface carries a hyperbolic metric conformal to g exactly when the curvature equation has a smooth solution.
• TauCeti.HyperbolicMetric.eq_of_metric_eq_rescale: two hyperbolic metrics conformal to g are equal.
• TauCeti.HyperbolicMetric.hypVolumeOfMetric_eq_of_metric_eq_rescale: a hyperbolic metric conformal to g has area -∫ K dV_g.

References

• J. L. Kazdan and F. W. Warner, Curvature functions for compact 2-manifolds, Ann. of Math. 99 (1974), 14–47.
• M. S. Berger, Riemannian structures of prescribed Gaussian curvature for compact 2-manifolds, J. Differential Geom. 5 (1971), 325–332.

theorem Bundle.ContMDiffRiemannianMetric.exists_hyperbolicMetric_metric_eq_rescale_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] [CompactSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hE : Module.finrank ℝ E = 2) : (∃ (G : TauCeti.HyperbolicMetric) (f : M → ℝ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x), G.metric = g.rescale f hf hf_pos) ↔ ∃ (φ : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) φ ∧ ∀ (x : M), -TauCeti.Manifold.laplaceBeltrami I φ x + g.scalarCurvature x / 2 + Real.exp (2 * φ x) = 0

Hyperbolic metrics in a conformal class and the curvature equation. A closed surface carries a hyperbolic metric conformal to g, that is of the form f g for a smooth positive function f, exactly when the curvature equation Δ⁺φ + K + e^(2φ) = 0 has a smooth solution φ; here Δ⁺ = -div grad is the nonnegative Laplacian of g and K = Scal^g / 2 its Gaussian curvature. The hyperbolic metric is then e^(2φ) g.

theorem TauCeti.HyperbolicMetric.eq_of_metric_eq_rescale {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [I.Boundaryless] (hE : Module.finrank ℝ E = 2) {g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (G₁ G₂ : HyperbolicMetric) {f₁ f₂ : M → ℝ} {hf₁ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f₁} {hf₁_pos : ∀ (x : M), 0 < f₁ x} {hf₂ : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f₂} {hf₂_pos : ∀ (x : M), 0 < f₂ x} (h₁ : G₁.metric = g.rescale f₁ hf₁ hf₁_pos) (h₂ : G₂.metric = g.rescale f₂ hf₂ hf₂_pos) : G₁ = G₂

Uniqueness of the hyperbolic metric in a conformal class. On a closed surface two hyperbolic metrics conformal to the same metric g are equal.

theorem TauCeti.HyperbolicMetric.hypVolumeOfMetric_eq_of_metric_eq_rescale {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [I.Boundaryless] [MeasurableSpace M] [BorelSpace M] (hE : Module.finrank ℝ E = 2) {g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x} (G : HyperbolicMetric) {f : M → ℝ} {hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f} {hf_pos : ∀ (x : M), 0 < f x} (h : G.metric = g.rescale f hf hf_pos) : hypVolumeOfMetric G = (-∫ (x : WithMetric g), g.scalarCurvature x.ofWithMetric ∂riemannianVolume I (WithMetric g)) / 2

Area of the hyperbolic metric in a conformal class. On a closed surface, a hyperbolic metric conformal to g has area -∫ K dV_g, where K = Scal^g / 2 is the Gaussian curvature of g.