The Levi-Civita connection of a pseudo-Riemannian metric #
This file adapts Mathlib's Levi-Civita connection of a Riemannian manifold
(Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita.lean) to a
pseudo-Riemannian metric g, which need not be positive definite. Mathlib's covariant
derivatives (CovariantDerivative) and torsion (CovariantDerivative.torsion) are used as they
are; the inner product of Mathlib's IsMetricCompatible is replaced by g.
Main definitions #
CovariantDerivative.IsMetricCompatibleWith:X g(σ, τ) = g(∇_X σ, τ) + g(σ, ∇_X τ).CovariantDerivative.IsLeviCivitaFor: torsion-free and metric-compatible.PseudoRiemannianMetric.leviCivita: the Levi-Civita connection ofg.
Main results #
CovariantDerivative.IsLeviCivitaFor.koszul: the Koszul formula.CovariantDerivative.IsLeviCivitaFor.uniqueness: uniqueness on differentiable vector fields.PseudoRiemannianMetric.exists_isLeviCivitaFor: existence.
Blueprint reference: def:metric-compatible-connection, def:levi-civita-connection,
lmm:koszul-formula, thrm:levi-civita-exists-unique.
A covariant derivative ∇ on the tangent bundle is compatible with the metric g: the Leibniz rule X(g(σ, τ)) = g(∇_X σ, τ) + g(σ, ∇_X τ) holds.
The left side is the derivative of the function y ↦ g_y(σ(y), τ(y)) at x in the direction X(x); the identity is asked at every point x where X, σ and τ are differentiable. In index notation it is ∇μ g(νρ) = 0: parallel transport preserves inner products, and so the causal type of vectors.
Implementation note: this is Mathlib's condition CovariantDerivative.isMetricCompatible_iff
with g in place of the inner product. The covariant derivative is Mathlib's
CovariantDerivative, a map sending a vector field Y to the field of linear maps
(∇Y)_x : TₓM → TₓM, with ∇_X Y at x given by (∇Y)_x(X(x)).
Blueprint: def:metric-compatible-connection
Equations
- One or more equations did not get rendered due to their size.
Instances For
A covariant derivative is a Levi-Civita connection of the metric g: it is torsion-free and compatible with g.
Torsion-free means ∇X Y - ∇Y X = [X, Y] for vector fields differentiable at the point, so the
Christoffel symbols are symmetric, Γ^ρ(μν) = Γ^ρ(νμ). Every pseudo-Riemannian metric has a
Levi-Civita connection (PseudoRiemannianMetric.exists_isLeviCivitaFor), and two of them agree
on differentiable vector fields (IsLeviCivitaFor.uniqueness); the Koszul formula expresses it
through g (IsLeviCivitaFor.koszul).
Implementation note: the structure mirrors Mathlib's CovariantDerivative.IsLeviCivitaConnection,
with g in place of the inner product. Uniqueness holds only on differentiable vector fields,
since a covariant derivative is unconstrained on the others.
Blueprint: def:levi-civita-connection
- isMetricCompatibleWith : IsMetricCompatibleWith g cov
∇ is compatible with g (
IsMetricCompatibleWith). ∇ is torsion-free: its torsion T(X, Y) = ∇_X Y - ∇_Y X - [X, Y] vanishes.
Instances For
The Koszul formula. For a Levi-Civita connection of g and vector fields X, Y, Z
differentiable at x, 2 g(∇_X Y, Z) is expressed through derivatives of g and Lie brackets
alone, without reference to ∇. This is Mathlib's IsLeviCivitaConnection.apply_eq multiplied
by 2, with g in place of the inner product; the blueprint's form of the formula is the same
statement after mlieBracket_swap and the symmetry of g.
Blueprint reference: lmm:koszul-formula.
Uniqueness of the Levi-Civita connection. Two Levi-Civita connections of g agree on
every vector field differentiable at x. (Covariant derivatives are unconstrained on
non-differentiable vector fields, as in Mathlib's IsLeviCivitaConnection.uniqueness.)
Blueprint reference: thrm:levi-civita-exists-unique.
Existence #
The construction follows Mathlib's CovariantDerivative.leviCivitaConnection: the right-hand
side of the Koszul formula (koszulAux) is tensorial in X and Z, hence a bilinear form at
each point, and the musical isomorphism flatEquiv turns it into the desired ∇_X Y.
The right-hand side of the Koszul formula, divided by 2: for the Levi-Civita connection
this is g(∇_X Y, Z).
Blueprint reference: lmm:koszul-expression-tensorial.
Equations
- One or more equations did not get rendered due to their size.
Instances For
y ↦ g_y(Y y, Z y) is differentiable at x if Y and Z are.
The real-valued mfderiv terms of koszulAux are mvfderiv terms.
koszulAux is tensorial in its first argument.
Blueprint reference: lmm:koszul-expression-tensorial.
koszulAux is tensorial in its third argument.
Blueprint reference: lmm:koszul-expression-tensorial.
The candidate ∇ Y at x for a vector field Y differentiable at x.
Equations
- g.leviCivitaAuxOfMDiffAt hY = ↑(g.flatEquiv x).symm ∘SL TensorialAt.mkHom₂ (fun (X Z : (x : M) → TangentSpace I x) => g.koszulAux X Y Z x) x ⋯ ⋯
Instances For
The function underlying the Levi-Civita connection of g (zero on vector fields that are
not differentiable at the point).
Equations
- g.leviCivitaAux Y x = if hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x then g.leviCivitaAuxOfMDiffAt hY else 0
Instances For
g(∇_X Y, Z) = koszulAux X Y Z for the constructed connection.
A tangent vector is determined by its g-pairings with vector fields differentiable at the
point.
The constructed operator is a covariant derivative.
Blueprint reference: lmm:koszul-connection-is-covariant-derivative.
The Koszul connection of g: the covariant derivative defined by the Koszul formula.
g(∇_X Y, Z) is set equal to the right-hand side of the Koszul formula (koszulAux), which is
tensorial in X and Z, and the musical isomorphism flatEquiv solves for ∇_X Y. It is compatible
with g and torsion-free (isMetricCompatibleWith_koszulConnection,
torsion_koszulConnection_eq_zero), which proves that a Levi-Civita connection exists.
Equations
- g.koszulConnection = { toFun := g.leviCivitaAux, isCovariantDerivativeOnUniv := ⋯ }
Instances For
The Koszul connection is compatible with g.
Blueprint reference: lmm:koszul-connection-is-levi-civita.
The Koszul connection is torsion-free.
Blueprint reference: lmm:koszul-connection-is-levi-civita.
Existence of the Levi-Civita connection. Every pseudo-Riemannian metric has a Levi-Civita connection.
Blueprint reference: thrm:levi-civita-exists-unique.
The Levi-Civita connection ∇ of the metric g.
It is torsion-free and compatible with g (isLeviCivitaFor_leviCivita), and any other connection
with these properties agrees with it on differentiable vector fields
(CovariantDerivative.IsLeviCivitaFor.uniqueness). In coordinates its Christoffel symbols are
Γ^ρ_(μν) = ½ g^(ρσ)(∂μ g(σν) + ∂ν g(σμ) - ∂σ g(μν)). Geodesics of a spacetime are defined
with it (Spacetime.IsGeodesic). For a constant metric on a vector space, as in Minkowski
spacetime, it is the ordinary directional derivative (leviCivita_apply_eq_fderiv).
Implementation note: the connection is a choice (Exists.choose) from
exists_isLeviCivitaFor, so its values on non-differentiable vector fields are unspecified;
statements about it use only differentiable fields.
Blueprint: thrm:levi-civita-exists-unique
Equations
- g.leviCivita = ⋯.choose
Instances For
The chosen leviCivita connection is a Levi-Civita connection of g.