The Christoffel map on the model space

A normed space F is a manifold with a single chart, and the tangent trivialization reads every tangent space of F as F itself. In the frame of that trivialization the constant vector fields have constant coefficients, so the flat covariant derivative of the frame kills them, and the Christoffel map of any covariant derivative on F is its value on constant fields: Γₓ(v, u) = ∇_u v. This turns an explicit computation of a connection on constant fields into its Christoffel map, the input of the coordinate curvature formula of TauCeti.Geometry.Manifold.VectorBundle.CovariantDerivative.Curvature.Coordinates.

Main results

• TauCeti.Manifold.frameCovariantDerivative_const_model_space: the flat covariant derivative of the tangent trivialization of F kills constant fields.
• TauCeti.Manifold.christoffelMap_model_space: on the model space, the Christoffel map of a covariant derivative is its value on constant fields.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 4, the Christoffel symbols of a connection in coordinates.

@[simp]

theorem TauCeti.Manifold.frameCovariantDerivative_const_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_3} [Fintype ι] (b : Module.Basis ι 𝕜 F) (x₀ x v : F) : frameCovariantDerivative (modelWithCornersSelf 𝕜 F) b (trivializationAt F (TangentSpace (modelWithCornersSelf 𝕜 F)) x₀) (fun (x : F) => v) x = 0

The frame of the tangent trivialization of the model space differentiates a constant field to zero: its coefficients in the frame are constant.

theorem TauCeti.Manifold.christoffelMap_model_space {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_3} [Fintype ι] (b : Module.Basis ι 𝕜 F) {cov : ((x : F) → TangentSpace (modelWithCornersSelf 𝕜 F) x) → (x : F) → TangentSpace (modelWithCornersSelf 𝕜 F) x →L[𝕜] TangentSpace (modelWithCornersSelf 𝕜 F) x} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] {x : F} (hcov : IsCovariantDerivativeOn F cov (trivializationAt F (TangentSpace (modelWithCornersSelf 𝕜 F)) x).baseSet) (v u : F) : ((christoffelMap b hcov x) v) u = (cov (fun (x : F) => v) x) u

On the model space F, the Christoffel map of a covariant derivative of the tangent bundle, in the tangent trivialization at x and any basis, is the covariant derivative of constant fields: Γₓ(v, u) = ∇_u v, with the field value v first and the direction u second.