The Levi-Civita connection of Sol

Compute the Levi-Civita derivative of constant coordinate fields for the metric exp (2z) dx² + exp (-2z) dy² + dz², and its Christoffel map in the global coordinates. These coefficients are the input for curvature computations and for the geodesic equation of Sol. The Christoffel map takes the field value first and the differentiation direction second, following the local-frame convention.

The calculation uses Mathlib's Levi-Civita connection, characterized by the Koszul formula CovariantDerivative.two_inner_leviCivitaConnection_eq_koszul. Constant coordinate fields commute, but their metric inner products vary with height. This follows the constant-field Koszul calculation in TauCeti.Geometry.Manifold.Riemannian.Hyperbolic.UpperHalfSpace.Connection; the chart-frame identification uses the model-space trivializations as in TauCeti.Geometry.Manifold.Riemannian.Geodesic.Euclidean.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 5 (the Koszul formula and Christoffel symbols).
• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983), 401–487 (the Sol geometry and its metric).

noncomputable def TauCeti.Sol.constantField (v : ℝ × ℝ × ℝ) (p : Sol) : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p

The vector field with constant value v in the global coordinates of Sol.

@[simp]

theorem TauCeti.Sol.constantField_apply (v : ℝ × ℝ × ℝ) (p : Sol) : constantField v p = (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p).symm v

The value of a constant coordinate vector field.

theorem TauCeti.Sol.contMDiff_constantField (v : ℝ × ℝ × ℝ) : ContMDiff (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) ((modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)).prod (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ))) ↑⊤ fun (q : Sol) => ⟨q, constantField v q⟩

Constant coordinate fields are smooth as sections of the tangent bundle.

theorem TauCeti.Sol.mdifferentiableAt_constantField (v : ℝ × ℝ × ℝ) (p : Sol) : (MDiffAt fun (q : Sol) => ⟨q, constantField v q⟩) p

Constant coordinate fields are differentiable as sections of the tangent bundle.

@[simp]

theorem TauCeti.Sol.mlieBracket_constantField (u v : ℝ × ℝ × ℝ) (p : Sol) : VectorField.mlieBracket (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (constantField u) (constantField v) p = 0

Constant coordinate fields on Sol have zero Lie bracket.

theorem TauCeti.Sol.mdifferentiableAt_exp_height (c : ℝ) (p : Sol) : (MDiffAt fun (q : Sol) => Real.exp (c * q.z)) p

The exponential of a scalar multiple of height is differentiable on Sol.

theorem TauCeti.Sol.mvfderiv_exp_height (c : ℝ) (p : Sol) (u : ℝ × ℝ × ℝ) : ((d% fun (q : Sol) => Real.exp (c * q.z)) p) (constantField u p) = Real.exp (c * p.z) * c * u.2.2

The derivative of an exponential of height along a constant coordinate field.

@[simp]

theorem TauCeti.Sol.leviCivitaConnection_const_apply (p : Sol) (u v : ℝ × ℝ × ℝ) : (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) ((↑(CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Sol) (constantField v) p) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p).symm u)) = (u.2.2 * v.1 + v.2.2 * u.1, -(u.2.2 * v.2.1 + v.2.2 * u.2.1), -Real.exp (2 * p.z) * u.1 * v.1 + Real.exp (-2 * p.z) * u.2.1 * v.2.1)

The Levi-Civita derivative of a constant coordinate field on Sol. The horizontal coefficients couple the horizontal and vertical directions; the vertical coefficient is -exp (2z) u₁ v₁ + exp (-2z) u₂ v₂.

@[simp]

theorem TauCeti.Sol.christoffelMap_leviCivitaConnection_apply {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℝ (ℝ × ℝ × ℝ)) (p : Sol) (u v : ℝ × ℝ × ℝ) : ((Manifold.christoffelMap b ⋯ p) v) u = (u.2.2 * v.1 + v.2.2 * u.1, -(u.2.2 * v.2.1 + v.2.2 * u.2.1), -Real.exp (2 * p.z) * u.1 * v.1 + Real.exp (-2 * p.z) * u.2.1 * v.2.1)

The Christoffel map of Sol in its global coordinate chart. The formula is independent of the finite basis used to define the map, and applies at every height.