Documentation

TauCeti.Geometry.Manifold.Riemannian.Hyperbolic.CurvatureEquation

The curvature equation for conformal metrics on surfaces #

Let g be a smooth Riemannian metric on a surface and ĝ = e^(2φ) g a conformal metric. In dimension two the scalar curvature is twice the Gaussian curvature, and the conformal change of scalar curvature becomes Scal^ĝ = e^(-2φ) (Scal^g - 2 Δφ), with Δ = div ∘ grad the Laplace–Beltrami operator of g. Thus ĝ has constant Gaussian curvature -1 exactly when φ solves the curvature equation (Bundle.ContMDiffRiemannianMetric.scalarCurvature_rescale_eq_iff_of_finrank_eq_two)

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

where Δ⁺ = -Δ is the nonnegative Laplacian and K = Scal^g / 2 the Gaussian curvature of g. This is the equation whose solution on a closed surface of negative Euler characteristic gives the hyperbolic metric in a conformal class. Since the curvature tensor of a surface is determined by its scalar curvature, the solutions of this equation are exactly the conformal factors for which ĝ has constant curvature -1 in the tensor form R(w,u)v = -(⟪u,v⟫ w - ⟪w,v⟫ u) (Bundle.ContMDiffRiemannianMetric.isConstantCurvatureTensor_rescale_iff_of_finrank_eq_two).

On a closed surface the right side of Δφ = K + e^(2φ) is strictly increasing in φ, so the maximum principle controls solutions: evaluating the equation at a maximum or a minimum of φ gives the barriers min (-K) ≤ e^(2φ) ≤ max (-K), forces K to be negative somewhere, and the comparison principle gives uniqueness of the conformal factor. The statements below are proved for every constant negative scalar curvature c, the hyperbolic case being c = -2.

Main results #

References #

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

The hyperbolic curvature equation on a surface. Let g be a smooth metric on a surface and f = e^(2φ) a smooth positive function. Then f g has constant curvature -1 exactly when φ solves Δ⁺φ + K + e^(2φ) = 0 everywhere, where Δ⁺ = -div grad is the nonnegative Laplacian of g and K = Scal^g / 2 its Gaussian curvature.

theorem Bundle.ContMDiffRiemannianMetric.apply_le_of_scalarCurvature_rescale_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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) [CompactSpace M] [I.Boundaryless] (hE : Module.finrank ℝ E = 2) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {c : ℝ} (hc : c < 0) (h : ∀ (x : M), (g.rescale f hf hf_pos).scalarCurvature x = c) {C : ℝ} (hC : ∀ (x : M), c * C ≤ g.scalarCurvature x) (x : M) :
f x ≤ C

Upper barrier. On a closed surface, let f g have constant negative scalar curvature c. If c C ≤ Scal^g everywhere, then f ≤ C; for c = -2 this says that the conformal factor of a metric of Gaussian curvature -1 is at most max (-K), with K = Scal^g / 2.

theorem Bundle.ContMDiffRiemannianMetric.le_apply_of_scalarCurvature_rescale_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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) [CompactSpace M] [I.Boundaryless] (hE : Module.finrank ℝ E = 2) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {c : ℝ} (hc : c < 0) (h : ∀ (x : M), (g.rescale f hf hf_pos).scalarCurvature x = c) {C : ℝ} (hC : ∀ (x : M), g.scalarCurvature x ≤ c * C) (x : M) :
C ≤ f x

Lower barrier. On a closed surface, let f g have constant negative scalar curvature c. If Scal^g ≤ c C everywhere, then C ≤ f; for c = -2 this says that the conformal factor of a metric of Gaussian curvature -1 is at least min (-K), with K = Scal^g / 2.

theorem Bundle.ContMDiffRiemannianMetric.exists_scalarCurvature_neg_of_scalarCurvature_rescale_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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) [CompactSpace M] [I.Boundaryless] [Nonempty M] (hE : Module.finrank ℝ E = 2) {f : M → ℝ} (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) f) (hf_pos : ∀ (x : M), 0 < f x) {c : ℝ} (hc : c < 0) (h : ∀ (x : M), (g.rescale f hf hf_pos).scalarCurvature x = c) :
∃ (x : M), g.scalarCurvature x < 0

Sign obstruction. If a metric g on a nonempty closed surface is conformal to a metric of constant negative scalar curvature, then the scalar curvature of g is negative somewhere.

theorem Bundle.ContMDiffRiemannianMetric.eq_of_scalarCurvature_rescale_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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) [CompactSpace M] [I.Boundaryless] (hE : Module.finrank ℝ E = 2) {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) {c : ℝ} (hc : c < 0) (h₁ : ∀ (x : M), (g.rescale f₁ hf₁ hf₁_pos).scalarCurvature x = c) (h₂ : ∀ (x : M), (g.rescale f₂ hf₂ hf₂_pos).scalarCurvature x = c) :
f₁ = f₂

Uniqueness of the constant negative curvature metric in a conformal class. On a closed surface, two metrics f₁ g and f₂ g conformal to g with the same constant negative scalar curvature coincide. In particular a conformal class contains at most one metric of Gaussian curvature -1.