The Levi-Civita connection under Riemannian isometries #
A local Riemannian isometry f : M → N, and in particular a smooth Riemannian isometry, transports
the Levi-Civita connection of N to that of M: for a vector field Y on N, differentiable at
f x, and a tangent vector v at x,
df_x (∇ᴹ_v (f^* Y)) = ∇ᴺ_{df_x v} Y,
where f^* Y = VectorField.mpullback I J f Y is the pullback vector field
x ↦ (df_x)⁻¹ (Y (f x)). Equivalently, the connection on M obtained by transporting ∇ᴺ
along f agrees with ∇ᴹ on differentiable vector fields. Only the differential of f at each
point enters, so f need not be injective or surjective: this also covers the inclusion of an
open submanifold with the restricted metric.
This is the connection-level input for transporting geodesics, their maximal intervals, and exponential maps along Riemannian isometries.
Main results #
In the namespace TauCeti.IsLocalRiemannianIsometry:
koszul_mpullback: the Koszul expression is natural under local Riemannian isometries.mfderiv_apply_mpullback_of_isLeviCivitaConnection: naturality of Levi-Civita connections under local Riemannian isometries.mfderiv_leviCivitaConnection_mpullback: the same statement for Mathlib'sCovariantDerivative.leviCivitaConnection.leviCivitaConnection_mpullback_apply_mpullback: the vector-field form∇ᴹ_{f^* Y} (f^* Z) = f^* (∇ᴺ_Y Z).
A Riemannian isometry Φ is a local Riemannian isometry
(TauCeti.RiemannianIsometry.isLocalRiemannianIsometry), so these apply to it through
Φ.isLocalRiemannianIsometry.
References #
- M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 2, Thm. 3.6.
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., GTM 176, 2018, Prop. 5.13.
Naturality of the Koszul expression. The Koszul expression of the pullbacks of three
vector fields along a local Riemannian isometry f is the Koszul expression of the fields
themselves, evaluated at the image point.
Naturality of Levi-Civita connections under local Riemannian isometries. If ∇ᴹ and ∇ᴺ
are Levi-Civita connections of M and N and f : M → N is a local Riemannian isometry, then
df_x (∇ᴹ_v (f^* Y)) = ∇ᴺ_{df_x v} Y for every vector field Y on N differentiable at
f x.
Naturality of the Levi-Civita connection under local Riemannian isometries, for Mathlib's
CovariantDerivative.leviCivitaConnection:
df_x (∇ᴹ_v (f^* Y)) = ∇ᴺ_{df_x v} Y for every vector field Y on N differentiable at
f x.
The covariant derivative of a pulled-back vector field in a pulled-back direction is the
pullback of the covariant derivative: ∇ᴹ_{f^* Y} (f^* Z) = f^* (∇ᴺ_Y Z) at x.