Curvature of the upper-half-space metric #
The metric (‖dx‖² + dt²) / t² has constant-curvature tensor with parameter -1.
The computation uses the Levi-Civita connection on constant coordinate fields and its
Leibniz rule, then reads the result in the hyperbolic tangent metric. It applies to every
finite-dimensional real inner product space of horizontal coordinates, including dimension zero.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 3 (the upper-half-space model) and Theorem 8.34 (its constant sectional curvature).
@[simp]
theorem
TauCeti.UpperHalfSpace.curvatureTensor_eq
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
(x : UpperHalfSpace E)
(u v w : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x)
:
((((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ)))
(UpperHalfSpace E)).curvatureTensor
x)
u)
v)
w = -1 • (inner ℝ v w • u - inner ℝ u w • v)
The upper-half-space curvature tensor is the constant-curvature tensor with parameter -1,
with inner products taken in the hyperbolic tangent metric.
theorem
TauCeti.UpperHalfSpace.hasConstantSectionalCurvature
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
:
(CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ)))
(UpperHalfSpace E)).HasConstantSectionalCurvature
⋯ (-1)
Every tangent two-plane of the upper-half-space model has sectional curvature -1.
@[simp]
theorem
TauCeti.UpperHalfSpace.ricciTensor_eq
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
(x : UpperHalfSpace E)
(u v : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x)
:
(((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (UpperHalfSpace E)).ricciTensor
x)
u)
v = -↑(Module.finrank ℝ E) * inner ℝ u v
The Ricci tensor of hyperbolic space is minus the horizontal dimension times the hyperbolic metric. In dimension one it vanishes.