The Koszul formula for Levi-Civita connections #
A covariant derivative ∇ on the tangent bundle of a Riemannian manifold is a Levi-Civita
connection, or Riemannian connection, if it is torsion free and compatible with the metric.
Mathlib states this as CovariantDerivative.IsLeviCivitaConnection, constructs such a connection,
CovariantDerivative.leviCivitaConnection, and proves that it is unique on differentiable sections,
CovariantDerivative.IsLeviCivitaConnection.uniqueness. This file develops the right-hand side of
the Koszul formula
2 ⟪∇_X Y, Z⟫ = X ⟪Y, Z⟫ + Y ⟪Z, X⟫ - Z ⟪X, Y⟫ + ⟪[X, Y], Z⟫ - ⟪[X, Z], Y⟫ - ⟪[Y, Z], X⟫
as an object in its own right. It involves the metric only, so it is packaged as a standalone
function TauCeti.Manifold.koszul. The Koszul formula in that form is
IsLeviCivitaConnection.two_inner_eq_koszul, and for Mathlib's connection
two_inner_leviCivitaConnection_eq_koszul; this is the shape in which
TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita.Regularity reads the
connection in a local frame. The converse direction isLeviCivitaConnection_iff shows nothing is
lost in the passage to koszul: a connection satisfying the Koszul formula is automatically torsion
free and metric.
Two covariant derivatives can only be compared through sections that are differentiable at the
point under consideration, because CovariantDerivative puts no constraint whatsoever on the
value of ∇ σ for a nowhere differentiable section σ. Mathlib's uniqueness is accordingly
stated for Y differentiable at x; IsLeviCivitaConnection.difference_eq_zero repackages it as
the vanishing of the endomorphism-valued one-form CovariantDerivative.difference ∇ ∇'.
Main definitions and results #
TauCeti.Manifold.koszulandTauCeti.Manifold.koszul_apply: the right-hand side of the Koszul formula, a function of the Riemannian metric alone, and its defining formula.CovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul: the Koszul formula, andCovariantDerivative.two_inner_leviCivitaConnection_eq_koszulfor Mathlib's connection.CovariantDerivative.isLeviCivitaConnection_iff: the Koszul formula characterises the Levi-Civita connections.CovariantDerivative.IsLeviCivitaConnection.difference_eq_zero: uniqueness of the Levi-Civita connection, as the vanishing of the difference of two of them.TauCeti.Manifold.koszul_sub_koszul_swap_first_twoandTauCeti.Manifold.koszul_add_koszul_swap_last_two: the two symmetries of the Koszul expression from which the converse direction is read off.TauCeti.Manifold.tensorialAt_koszul_thirdandTauCeti.Manifold.tensorialAt_koszul_first: the Koszul expression is tensorial in its last argument and in its first.TauCeti.Manifold.koszul_add_secondandTauCeti.Manifold.koszul_smul_second: additivity and the Leibniz rule in the middle argument, the slot which the connection differentiates.TauCeti.Manifold.koszulBilinear_mpullback: the Koszul expression of a pairing is natural under maps with invertible differentials pulling one pairing back to the other.TauCeti.Manifold.koszulBilinear_sub_two_mul_apply_eq_derivBilinearTensor: along a torsion-free connection, the Koszul expression of a symmetric pairingbdiffers from2 b(∇_X Y, Z)by(∇_X b)(Y, Z) + (∇_Y b)(X, Z) - (∇_Z b)(X, Y).
References #
- mathlib4#36845: the first-slot tensoriality and second-slot Leibniz identities follow its design.
- M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 2, Thm. 3.6.
- J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Thm. 5.10.
- A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.K, Theorem 1.174: the first variation of the Levi-Civita connection, obtained by differentiating the Koszul formula.
Nondegeneracy of the metric along differentiable sections #
Two continuous linear maps between fibres are equal if their values on differentiable sections have the same inner products against every differentiable section of the target bundle.
The Koszul expression #
The right-hand side of the Koszul formula for a pointwise bilinear pairing b.
Instances For
The defining formula for the Koszul expression of a pointwise bilinear pairing.
Antisymmetrizing the bilinear Koszul expression in its first two arguments returns twice the pairing of the Lie bracket with the third argument.
Symmetrizing the bilinear Koszul expression in its last two arguments returns twice the derivative of their pairing along the first argument.
The Koszul identity for a symmetric pointwise bilinear pairing implies its metric product rule along differentiable vector fields.
The Koszul identity for a symmetric nondegenerate pointwise bilinear pairing implies that the connection is torsion free.
The Koszul expression is additive in the differentiated vector field.
The Koszul expression obeys the connection Leibniz rule in its second argument.
The Koszul expression is additive in its first argument.
The Koszul expression is tensorial in its first argument: replacing X by f • X multiplies
it by f x.
The Koszul expression is tensorial in its first argument. Together with
TauCeti.Manifold.tensorialAt_koszulBilinear_third, in finite dimension this yields a continuous
bilinear form on the tangent fibre via TensorialAt.mkHom₂, as used to build the Levi-Civita
connection.
The Koszul expression is tensorial in its third argument.
The Koszul expression of a symmetric field of bilinear forms along a torsion-free
connection. For a torsion-free covariant derivative ∇ on the tangent bundle and a symmetric
field of bilinear forms b which pairs differentiable vector fields to differentiable functions,
K_b(X, Y, Z) - 2 b(∇_X Y, Z) = (∇_X b)(Y, Z) + (∇_Y b)(X, Z) - (∇_Z b)(X, Y),
where K_b is the Koszul expression of b and ∇b is
CovariantDerivative.derivBilinearTensor. When ∇ is compatible with b, the right-hand side
vanishes and this is the Koszul formula. For a family of metrics gₜ with Levi-Civita connections
∇ᵗ and h = ∂ₜ gₜ, differentiating the Koszul formula 2 gₜ(∇ᵗ_X Y, Z) = K_{gₜ}(X, Y, Z) in
t gives 2 g((∂ₜ∇)_X Y, Z) = K_h(X, Y, Z) - 2 h(∇_X Y, Z); this identity, applied to b = h,
rewrites the right-hand side as the covariant derivative of h.
Naturality of the bilinear Koszul expression. Let f : M → N be a map with invertible
differentials, C² at x, which pulls the pairing b' on N back to the pairing b on M,
b_y(v, w) = b'_{f y}(df_y v, df_y w). Suppose that b' pairs vector fields differentiable at
f x to a function differentiable at f x. Then the Koszul expression of b on the pullbacks of
three vector fields differentiable at f x is the Koszul expression of b' on the fields
themselves, evaluated at f x.
The right-hand side of the Koszul formula,
X ⟪Y, Z⟫ + Y ⟪Z, X⟫ - Z ⟪X, Y⟫ + ⟪[X, Y], Z⟫ - ⟪[X, Z], Y⟫ - ⟪[Y, Z], X⟫,
evaluated at x. It depends on the Riemannian metric alone; for the Levi-Civita connection ∇ of
that metric it computes 2 ⟪∇_X Y, Z⟫, by
CovariantDerivative.IsLeviCivitaConnection.two_inner_eq_koszul.
Instances For
The defining formula for the Koszul expression, available outside the module where
TauCeti.Manifold.koszul is defined.
Antisymmetrising the Koszul expression in its first two arguments returns twice the inner
product of the Lie bracket with the third argument. This is the identity behind the torsion-free
half of CovariantDerivative.isLeviCivitaConnection_iff.
Symmetrising the Koszul expression in its last two arguments returns twice the derivative of
their inner product along the first argument. This is the identity behind the metric half of
CovariantDerivative.isLeviCivitaConnection_iff.
The pointwise inner product of two sections of the tangent bundle that are differentiable at
x is differentiable at x. This is the tangent-bundle specialisation of
MDifferentiableAt.inner_bundle, whose bundle argument Lean cannot infer from hypotheses phrased
through TangentSpace.
Behaviour in the first two arguments #
The Koszul expression is tensorial in its first argument, just as it is in its third, and obeys a
Leibniz rule in its second. These are the identities from which a connection is built out of the
Koszul formula, as Mathlib builds CovariantDerivative.leviCivitaConnection.
The Koszul expression is additive in its second argument.
The Leibniz rule for the Koszul expression in its second argument: replacing Y by f • Y
multiplies the expression by f x and adds 2 (df X) ⟪Y, Z⟫. This is the identity behind the
Leibniz axiom of the connection built from the Koszul formula.
The Koszul expression is additive in its first argument.
The Koszul expression is tensorial in its first argument: replacing X by f • X multiplies
it by f x.
The Koszul expression is tensorial in its first argument. Together with
TauCeti.Manifold.tensorialAt_koszul_third, in finite dimension this yields a continuous bilinear
form on the tangent fibre via TensorialAt.mkHom₂, as used to build the Levi-Civita connection.
The Koszul expression is tensorial in its third argument: replacing Z by f • Z multiplies
it by f x, and it is additive in Z. Together with
CovariantDerivative.isLeviCivitaConnection_iff this is what turns the Koszul formula from a
characterisation of the Levi-Civita connection into a construction of it.
Levi-Civita connections and the Koszul expression #
Two covariant derivatives have zero difference if they agree on every section differentiable at the point where they are evaluated.
The Koszul formula: for a Levi-Civita connection, 2 ⟪∇_X Y, Z⟫ is the Koszul expression
of the metric. Mathlib's CovariantDerivative.IsLeviCivitaConnection.apply_eq is the same identity
with the expression written out; this form is the one TauCeti.Manifold.koszul controls.
A covariant derivative on the tangent bundle is a Levi-Civita connection exactly when it satisfies the Koszul formula.
Uniqueness of the Levi-Civita connection, as the vanishing of the endomorphism-valued
one-form measuring the difference of two connections. On a single differentiable section this is
Mathlib's CovariantDerivative.IsLeviCivitaConnection.uniqueness.
The Koszul formula for Mathlib's Levi-Civita connection
CovariantDerivative.leviCivitaConnection, in terms of TauCeti.Manifold.koszul.