Curvature and the central direction of Nil

Compute the curvature and Ricci tensors of dx² + dy² + (dz - x dy)² using the existing Levi-Civita connection on left-invariant fields. In the orthonormal frame ∂ₓ, ∂ᵧ + x ∂_z, ∂_z, the Ricci eigenvalues are -1/2, -1/2, 1/2. The positive eigenspace is exactly the central line, so every Riemannian isometry preserves that line. This constrains arbitrary isometries when comparing them with the known action of the Heisenberg group and O(2).

The curvature convention is R(u,v)w = ∇ᵤ∇ᵥw - ∇ᵥ∇ᵤw - ∇_[u,v]w. The Ricci contraction follows the coordinate-basis argument in TauCeti.Geometry.Manifold.Riemannian.Sol.Curvature.

References

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

@[simp]

theorem TauCeti.Nil.curvatureTensor_eq (p : Nil) (a b c : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : have A := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) a; have B := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) b; have C := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) c; have u := (A.1, A.2.1, A.2.2 - p.x * A.2.1); have v := (B.1, B.2.1, B.2.2 - p.x * B.2.1); have w := (C.1, C.2.1, C.2.2 - p.x * C.2.1); have r := ((-3 * w.2.1 * (u.1 * v.2.1 - u.2.1 * v.1) + w.2.2 * (u.1 * v.2.2 - u.2.2 * v.1)) / 4, (3 * w.1 * (u.1 * v.2.1 - u.2.1 * v.1) + w.2.2 * (u.2.1 * v.2.2 - u.2.2 * v.2.1)) / 4, (-w.1 * (u.1 * v.2.2 - u.2.2 * v.1) - w.2.1 * (u.2.1 * v.2.2 - u.2.2 * v.2.1)) / 4); (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) (((((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil).curvatureTensor p) a) b) c) = (r.1, r.2.1, r.2.2 + p.x * r.2.1)

The curvature tensor of Nil in global coordinates, with vectors first read in the left-invariant orthonormal frame. The final coordinate adds x times the second frame component to convert back to coordinate vectors.

@[simp]

theorem TauCeti.Nil.ricciTensor_eq (p : Nil) (u v : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : have a := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u; have b := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v; (((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil).ricciTensor p) u) v = (-a.1 * b.1 - a.2.1 * b.2.1 + (a.2.2 - p.x * a.2.1) * (b.2.2 - p.x * b.2.1)) / 2

The Ricci tensor of Nil is (-dx² - dy² + (dz - x dy)²) / 2. In particular, the central direction has eigenvalue 1/2.

@[simp]

theorem TauCeti.Nil.ricciTensor_eq_half_inner_iff (p : Nil) (u : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : (∀ (v : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p), (((CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil).ricciTensor p) u) v = inner ℝ u v / 2) ↔ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u).1 = 0 ∧ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u).2.1 = 0

The Ricci eigenspace with eigenvalue 1/2 is precisely the central line: both horizontal coordinate components vanish.

theorem TauCeti.Nil.mfderiv_central_iff (Φ : Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil) (p : Nil) (u : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (Φ p)) ((mfderiv% ⇑Φ p) u)).1 = 0 ∧ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (Φ p)) ((mfderiv% ⇑Φ p) u)).2.1 = 0 ↔ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u).1 = 0 ∧ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u).2.1 = 0

The differential of every Riemannian isometry of Nil preserves the central line, in both directions, at every point.