Acceleration and second covariant derivatives under local Riemannian isometries #
The differential of a local Riemannian isometry carries the covariant acceleration of a
C² curve to that of its image. Since this differential is injective, vanishing acceleration
can also be tested after composing with the local isometry. These statements apply to curves
lifted through Riemannian covering sheets, without a global inverse or a completeness assumption.
The derivatives are taken within an explicit parameter set with unique derivatives, including
closed intervals. The unrestricted forms apply to globally C² curves.
For smooth metrics the same naturality holds for the second covariant derivative of any field
with a C² tangent-bundle lift, without an assumed Jacobi equation.
The argument specializes the arbitrary-field naturality theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_alongCurveWithin to the curve's velocity.
References #
- M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Chapter 2, Theorem 3.6.
theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_accelerationWithin
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 2 M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 2 N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y]
{f : M → N}
{γ : ℝ → M}
{s : Set ℝ}
{t : ℝ}
(hf : IsLocalRiemannianIsometry I J f)
(hs : UniqueDiffOn ℝ s)
(hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s)
(ht : t ∈ s)
:
(mfderiv% f (γ t)) ((CovariantDerivative.leviCivitaConnection I M).accelerationWithin γ s t) = (CovariantDerivative.leviCivitaConnection J N).accelerationWithin (f ∘ γ) s t
A local Riemannian isometry preserves covariant acceleration within a parameter set.
theorem
TauCeti.IsLocalRiemannianIsometry.accelerationWithin_comp_eq_zero_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 2 M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 2 N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y]
{f : M → N}
{γ : ℝ → M}
{s : Set ℝ}
{t : ℝ}
(hf : IsLocalRiemannianIsometry I J f)
(hs : UniqueDiffOn ℝ s)
(hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 2 γ s)
(ht : t ∈ s)
:
(CovariantDerivative.leviCivitaConnection J N).accelerationWithin (f ∘ γ) s t = 0 ↔ (CovariantDerivative.leviCivitaConnection I M).accelerationWithin γ s t = 0
The acceleration of a C² curve vanishes exactly when that of its image under a local
Riemannian isometry vanishes.
theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_acceleration
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 2 M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 2 N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y]
{f : M → N}
{γ : ℝ → M}
(hf : IsLocalRiemannianIsometry I J f)
(hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 2 γ)
(t : ℝ)
:
(mfderiv% f (γ t)) ((CovariantDerivative.leviCivitaConnection I M).acceleration γ t) = (CovariantDerivative.leviCivitaConnection J N).acceleration (f ∘ γ) t
A local Riemannian isometry preserves the unrestricted covariant acceleration.
theorem
TauCeti.IsLocalRiemannianIsometry.acceleration_comp_eq_zero_iff
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 2 M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 2 N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y]
{f : M → N}
{γ : ℝ → M}
(hf : IsLocalRiemannianIsometry I J f)
(hγ : ContMDiff (modelWithCornersSelf ℝ ℝ) I 2 γ)
(t : ℝ)
:
(CovariantDerivative.leviCivitaConnection J N).acceleration (f ∘ γ) t = 0 ↔ (CovariantDerivative.leviCivitaConnection I M).acceleration γ t = 0
A globally C² curve has zero acceleration exactly when its image under a local
Riemannian isometry does.
theorem
TauCeti.IsLocalRiemannianIsometry.mfderiv_alongCurveWithin_alongCurveWithin
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[TopologicalSpace M]
[ChartedSpace H M]
[IsManifold I 2 M]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[FiniteDimensional ℝ F]
{H' : Type u_5}
[TopologicalSpace H']
{J : ModelWithCorners ℝ F H'}
{N : Type u_6}
[TopologicalSpace N]
[ChartedSpace H' N]
[IsManifold J 2 N]
[Bundle.RiemannianBundle fun (y : N) => TangentSpace J y]
[IsContMDiffRiemannianBundle J 1 F fun (y : N) => TangentSpace J y]
{f : M → N}
{γ : ℝ → M}
{s : Set ℝ}
{t : ℝ}
[IsManifold I (↑⊤) M]
[IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x]
(hf : IsLocalRiemannianIsometry I J f)
{V : (r : ℝ) → TangentSpace I (γ r)}
(hs : UniqueDiffOn ℝ s)
(hV : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I.tangent 2 (fun (r : ℝ) => ⟨γ r, V r⟩) s)
(ht : t ∈ s)
:
(mfderiv% f (γ t))
((CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ
((CovariantDerivative.leviCivitaConnection I M).alongCurveWithin γ V s) s t) = (CovariantDerivative.leviCivitaConnection J N).alongCurveWithin (f ∘ γ)
((CovariantDerivative.leviCivitaConnection J N).alongCurveWithin (f ∘ γ) (fun (r : ℝ) => (mfderiv% f (γ r)) (V r))
s)
s t
A local Riemannian isometry commutes with the second covariant derivative of a field with
C² tangent-bundle lift. No geodesic or Jacobi equation is assumed.