The along-curve covariant derivative read in an arbitrary chart

CovariantDerivative.alongCurveWithin differentiates a tangent field V along a curve γ by the moving-chart formula v' + Γ (v, u'), read in the chart centred at the current point γ t. This file proves that the same formula computed in any chart around γ t, transported back to TangentSpace I (γ t), returns the same tangent vector, for an arbitrary field along the curve. AlongCurve/Pullback.lean obtains this only for fields pulled back from an ambient vector field, where the value is identified with the ambient covariant derivative; the general statement needs the Christoffel transformation law instead.

Two chart readings of V differ by the tangent coordinate change A z (TauCeti.Manifold.sectionCoord_coordChange), so differentiating the reading in the chart at x produces the extra term (d/dt) (A (γ t)) v, while the Christoffel transformation law TauCeti.Manifold.christoffelMap_coordChange produces exactly its negative. The cancellation of these two inhomogeneous terms is the content of the main theorem, and is what allows a fixed chart to be used in place of the moving one.

Main results

• CovariantDerivative.symmL_alongCurveInChartWithin: chart independence -- the coordinate formula read in an arbitrary chart around γ t transports back to the moving-chart value.
• CovariantDerivative.alongCurveInChartWithin_coordChange: the resulting transformation law for the coordinate formula between two charts around γ t.

References

• M. P. do Carmo, Riemannian Geometry, Birkhauser, 1992, Ch. 2, Proposition 2.2.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Ch. 4.

theorem CovariantDerivative.symmL_alongCurveInChartWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {x : M} {s : Set 𝕜} {t : 𝕜} (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : MDiffAt[s] γ t) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) : (Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) x) (γ t)) (cov.alongCurveInChartWithin γ V s x t) = cov.alongCurveWithin γ V s t

Chart independence of the along-curve derivative. The coordinate formula computed in the chart at an arbitrary point x whose base set contains γ t, transported back to TangentSpace I (γ t), is the moving-chart value CovariantDerivative.alongCurveWithin. The field along the curve is arbitrary: only differentiability of its moving-chart reading is assumed.

theorem CovariantDerivative.alongCurveInChartWithin_coordChange {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] (cov : CovariantDerivative I E fun (y : M) => TangentSpace I y) (γ : 𝕜 → M) (V : (t : 𝕜) → TangentSpace I (γ t)) {x y : M} {s : Set 𝕜} {t : 𝕜} (hx : γ t ∈ (trivializationAt E (TangentSpace I) x).baseSet) (hy : γ t ∈ (trivializationAt E (TangentSpace I) y).baseSet) (hu : UniqueDiffWithinAt 𝕜 s t) (hγ : MDiffAt[s] γ t) (hV : DifferentiableWithinAt 𝕜 (TauCeti.Manifold.sectionCoord γ V (γ t)) s t) : cov.alongCurveInChartWithin γ V s y t = (tangentCoordChange I x y (γ t)) (cov.alongCurveInChartWithin γ V s x t)

The transformation law for the along-curve coordinate formula. Between the trivializations at two points whose base sets contain γ t, the coordinate formula transforms by the tangent coordinate change.