Coordinate changes for Christoffel maps

This file proves the transformation law for the model-space Christoffel map of a covariant derivative on the tangent bundle. The law is stated for independent vector and direction arguments, so its diagonal specialization is available for the geodesic spray.

Main results

• TauCeti.Manifold.christoffelMap_coordChange: the Christoffel transformation law under a change of tangent trivialization.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §2.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2018, Ch. 4.

theorem TauCeti.Manifold.christoffelMap_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] {ι : Type u_5} (b : Module.Basis ι 𝕜 E) {x x₀ : M} {cov : ((z : M) → TangentSpace I z) → (z : M) → TangentSpace I z →L[𝕜] TangentSpace I z} [Fintype ι] [IsManifold I 2 M] (_hx₀ : x ∈ (extChartAt I x₀).source) (U V : TangentSpace I x) (hcov : IsCovariantDerivativeOn E cov (trivializationAt E (TangentSpace I) x₀).baseSet) (hcov' : IsCovariantDerivativeOn E cov (trivializationAt E (TangentSpace I) x).baseSet) : ((christoffelMap b hcov x) ((tangentCoordChange I x x₀ x) V)) ((tangentCoordChange I x x₀ x) U) = (tangentCoordChange I x x₀ x) (((christoffelMap b hcov' x) V) U) - ((d% fun (z : M) => (tangentCoordChange I x x₀ z) V) x) U

The Christoffel transformation law. The Christoffel map of a covariant derivative on the tangent bundle, read in the trivialization centred at x₀ and evaluated at the x₀-coordinates of a tangent vector V and direction U, is the pushforward by tangentCoordChange I x x₀ x of its value read in the trivialization centred at x, less the derivative of the tangent coordinate change between the two charts along U applied to V.