Covariant differentiation along curves under local Riemannian isometries

For a local Riemannian isometry f : M → N, covariant differentiation along a curve commutes with the tangent map of f. This is the along-curve form of the naturality of the Levi-Civita connection. It applies to differentiable tangent fields along arbitrary parameter sets with unique derivatives, including closed intervals.

Naturality for arbitrary tangent fields along a curve, rather than only for fields pulled back from an ambient vector field, is what allows intrinsic equations involving covariant derivatives along curves to be transported by an isometry. The main example is the geodesic equation: the velocity field of a curve is generally not the restriction of an ambient vector field.

Main results

• mfderiv_alongCurveWithin_mpullback: naturality for a field pulled back from the target.
• mfderiv_alongCurveWithin: naturality for an arbitrary differentiable tangent field along the curve.
• mfderiv_alongCurve: the unrestricted form.

See do Carmo, Riemannian Geometry, Chapter 2, Theorem 3.6.

theorem TauCeti.IsLocalRiemannianIsometry.mfderiv_alongCurveWithin_mpullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {f : M → N} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (hf : IsLocalRiemannianIsometry I J f) {γ : ℝ → M} {s : Set ℝ} {t : ℝ} {Y : (y : N) → TangentSpace J y} (hs : UniqueDiffWithinAt ℝ s t) (hγ : MDiffAt[s] γ t) (hY : (MDiffAt fun (y : N) => ⟨y, Y y⟩) (f (γ t))) : (mfderiv% f (γ t)) ((CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ (fun (r : ℝ) => VectorField.mpullback I J f Y (γ r)) s t) = (CovariantDerivative.leviCivitaConnection J N).alongCurveWithin (f ∘ γ) (fun (r : ℝ) => Y ((f ∘ γ) r)) s t

Covariant differentiation along a curve of an ambient vector field commutes with a local Riemannian isometry. The field on the source is the pullback of the field on the target.

theorem TauCeti.IsLocalRiemannianIsometry.mfderiv_alongCurve_mpullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {f : M → N} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (hf : IsLocalRiemannianIsometry I J f) {γ : ℝ → M} {t : ℝ} {Y : (y : N) → TangentSpace J y} (hγ : MDiffAt γ t) (hY : (MDiffAt fun (y : N) => ⟨y, Y y⟩) (f (γ t))) : (mfderiv% f (γ t)) ((CovariantDerivative.leviCivitaConnection I M).alongCurve γ (fun (r : ℝ) => VectorField.mpullback I J f Y (γ r)) t) = (CovariantDerivative.leviCivitaConnection J N).alongCurve (f ∘ γ) (fun (r : ℝ) => Y ((f ∘ γ) r)) t

For a differentiable curve, the unrestricted along-curve Levi-Civita derivative of a pulled-back ambient field is carried to the derivative of that field along the image curve.

Arbitrary tangent fields along a curve

theorem TauCeti.IsLocalRiemannianIsometry.mfderiv_alongCurveWithin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {f : M → N} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (hf : IsLocalRiemannianIsometry I J f) {γ : ℝ → M} {V : (r : ℝ) → TangentSpace I (γ r)} {s : Set ℝ} {t : ℝ} (hs : UniqueDiffWithinAt ℝ s t) (hγ : MDiffAt[s] γ t) (hV : DifferentiableWithinAt ℝ (Manifold.sectionCoord γ V (γ t)) s t) : (mfderiv% f (γ t)) ((CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ V s t) = (CovariantDerivative.leviCivitaConnection J N).alongCurveWithin (f ∘ γ) (fun (r : ℝ) => (mfderiv% f (γ r)) (V r)) s t

Naturality of covariant differentiation along a curve under a local Riemannian isometry. The differential of an isometry carries the Levi-Civita derivative of a differentiable tangent field along γ to the derivative of the transported field along f ∘ γ.

The hypothesis hV expresses differentiability of the tangent field in local bundle coordinates.

theorem TauCeti.IsLocalRiemannianIsometry.mfderiv_alongCurve {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] {f : M → N} [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [IsManifold I 2 M] [IsManifold J 2 N] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y] (hf : IsLocalRiemannianIsometry I J f) {γ : ℝ → M} {V : (r : ℝ) → TangentSpace I (γ r)} {t : ℝ} (hγ : MDiffAt γ t) (hV : DifferentiableAt ℝ (Manifold.sectionCoord γ V (γ t)) t) : (mfderiv% f (γ t)) ((CovariantDerivative.leviCivitaConnection I M).alongCurve γ V t) = (CovariantDerivative.leviCivitaConnection J N).alongCurve (f ∘ γ) (fun (r : ℝ) => (mfderiv% f (γ r)) (V r)) t

The unrestricted form of naturality of covariant differentiation along a curve under a local Riemannian isometry.