Curvature and Ricci curvature of Sol

Compute the curvature tensor of the metric exp (2z) dx² + exp (-2z) dy² + dz² in global coordinates. Its Ricci tensor is -2 dz ⊗ dz: its kernel is precisely the horizontal plane, and its negative direction singles out the vertical line. These intrinsic subspaces constrain the differential of an isometry of Sol.

The calculation uses Sol.leviCivitaConnection_const_apply, the connection's Leibniz rule, and the basis-independent trace defining Ricci curvature. The curvature convention is R(u,v)w = ∇ᵤ∇ᵥw - ∇ᵥ∇ᵤw - ∇_[u,v]w.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 7 (curvature and Ricci contraction).
• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983), 401–487, Section 4 (Sol and its isometry group).

@[simp]

theorem TauCeti.Sol.curvatureTensor_eq (p : Sol) (a b c : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : have u := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) a; have v := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) b; have w := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) c; (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) (((((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Sol).curvatureTensor p) a) b) c) = (w.2.2 * (u.2.2 * v.1 - v.2.2 * u.1) + Real.exp (-2 * p.z) * w.2.1 * (v.2.1 * u.1 - u.2.1 * v.1), w.2.2 * (u.2.2 * v.2.1 - v.2.2 * u.2.1) + Real.exp (2 * p.z) * w.1 * (v.1 * u.2.1 - u.1 * v.2.1), -Real.exp (2 * p.z) * w.1 * (u.2.2 * v.1 - v.2.2 * u.1) - Real.exp (-2 * p.z) * w.2.1 * (u.2.2 * v.2.1 - v.2.2 * u.2.1))

The curvature tensor of Sol in global coordinates. The first two vectors are the curvature directions and the third is the vector acted on.

@[simp]

theorem TauCeti.Sol.ricciTensor_eq (p : Sol) (u v : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : (((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Sol).ricciTensor p) u) v = -2 * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u).2.2 * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.2

Ricci curvature of Sol is -2 dz ⊗ dz, at every point. The formula uses global coordinate vectors, without choosing an orthonormal frame.