The Levi-Civita connection in global linear coordinates #
A finite-dimensional real normed space F is a manifold with a single chart, and its tangent
space at every point is F. A Riemannian metric on F is then a field
g : F → F →L[ℝ] F →L[ℝ] ℝ of inner products, as for the left-invariant metrics of the model
geometries Nil, Sol and SL₂ℝ~ on ℝ³. This file computes the Levi-Civita connection of such
a metric from the derivative of g, by the Christoffel formula of the first kind:
2 g(∇_u V, w) = 2 g(DV(u), w) + (Dg(u))(V, w) + (Dg(V))(w, u) - (Dg(w))(u, V).
The derivative Dg(u) of the metric differentiates its coefficients only, with the two
arguments held fixed. For a constant field V the first term vanishes, so the remaining terms
are the Christoffel symbols of the first kind of g. A candidate vector satisfying the
right-hand side is then the value of the connection. Together with
TauCeti.Manifold.christoffelMap_model_space, which reads the Christoffel map on the model space
as the value of the connection on constant fields, these turn an explicit metric on F into its
Christoffel map, which is the input of the coordinate curvature formula of
TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature.Coordinates.
Main results #
TauCeti.Manifold.two_mul_leviCivitaConnection_model_space: the Christoffel formula of the first kind for the Levi-Civita connection of a differentiable metric onF.TauCeti.Manifold.leviCivitaConnection_model_space_eq_fderiv_add: the Levi-Civita connection is the flat derivative plus any vector solving the Christoffel formula of the first kind.TauCeti.Manifold.leviCivitaConnection_model_space_eq_fderiv_add_christoffelSecondKind: the Levi-Civita connection is the flat derivative plus the Christoffel symbols of the second kind of the metric, as constructed for any nondegenerate metric inTauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita.Christoffel.Basic.TauCeti.Manifold.leviCivitaConnection_eq_fderiv_model_space: for the standard metric, the Levi-Civita connection is the ordinary Fréchet derivative.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 5: Theorem 5.10 (the Koszul formula) and the Christoffel symbols of a metric in coordinates.
- M. P. do Carmo, Riemannian Geometry, Birkhäuser (1992), Chapter 2, §3.
The Christoffel formula of the first kind #
The Christoffel formula of the first kind. If the Riemannian metric of the model space
F is the field of bilinear forms g, differentiable at x, then the Levi-Civita derivative of
a vector field V differentiable at x satisfies
2 g(∇_u V, w) = 2 g(DV(u), w) + (Dg(u))(V, w) + (Dg(V))(w, u) - (Dg(w))(u, V).
Tangent vectors are read in the model space through tangentSpaceCastModel.
The Levi-Civita derivative ∇_u V of a vector field V on the model space F, for a metric
given by the field of bilinear forms g, is the flat derivative DV(u) plus any vector γ
solving the Christoffel formula of the first kind
2 g(γ, w) = (Dg(u))(V, w) + (Dg(V))(w, u) - (Dg(w))(u, V) for all w.
The Levi-Civita derivative ∇_u V of a vector field V on the model space F, for a metric
given by the field of bilinear forms g, is the flat derivative DV(u) plus the Christoffel
symbols of the second kind of g: ∇_u V = DV(u) + Γ(u, V). Thus the Christoffel symbols of a
general nondegenerate metric specialize, for a positive-definite one, to those of Mathlib's
Levi-Civita connection.
For the standard Riemannian metric on a finite-dimensional real inner-product space, the Levi-Civita derivative is the ordinary Fréchet derivative.