Christoffel symbols in a coordinate frame

Torsion-freedom of a covariant derivative on the tangent bundle says that ∇_X Y - ∇_Y X is the Lie bracket [X, Y]. Since the vector fields of a coordinate frame commute, a torsion-free connection satisfies ∇_{∂ᵢ} ∂ⱼ = ∇_{∂ⱼ} ∂ᵢ. This is the classical symmetry Γᵏᵢⱼ = Γᵏⱼᵢ of the Christoffel symbols in a chart, and gives the corresponding symmetry of the model-space Christoffel map.

The Christoffel map read in the canonical trivialization at a point x is also the covariant derivative at x of the vector fields with constant coordinates in the chart at x.

Main results

• TauCeti.Manifold.covariantDerivative_localFrame_comm: a torsion-free covariant derivative differentiates a coordinate frame symmetrically.
• TauCeti.Manifold.christoffelSymbol_comm and TauCeti.Manifold.christoffelMap_comm: the Christoffel symbols and Christoffel map of a torsion-free covariant derivative are symmetric in their two lower arguments.
• TauCeti.Manifold.covariantDerivative_extend_eq_christoffelMap: at x, the covariant derivative of the vector field with constant coordinates w in the chart at x is the Christoffel map.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 2, §3, the symmetry of the Riemannian connection in a coordinate system.
• J. M. Lee, Introduction to Riemannian Manifolds, GTM 176, 2nd ed., 2018, Problem 4-6(b).

theorem TauCeti.Manifold.covariantDerivative_localFrame_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_5} {x : M} [IsManifold I (minSmoothness 𝕜 2) M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {cov : CovariantDerivative I E (TangentSpace I)} (ht : cov.IsTorsionFree) (b : Module.Basis ι 𝕜 E) (x₀ : M) (hx : x ∈ (extChartAt I x₀).source) (i j : ι) : (↑cov ((trivializationAt E (TangentSpace I) x₀).localFrame b j) x) ((trivializationAt E (TangentSpace I) x₀).localFrame b i x) = (↑cov ((trivializationAt E (TangentSpace I) x₀).localFrame b i) x) ((trivializationAt E (TangentSpace I) x₀).localFrame b j x)

A torsion-free connection differentiates the coordinate frame symmetrically: in the chart at x₀, ∇_{∂ᵢ} ∂ⱼ = ∇_{∂ⱼ} ∂ᵢ.

theorem TauCeti.Manifold.christoffelSymbol_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_5} {x : M} [IsManifold I (minSmoothness 𝕜 2) M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {cov : CovariantDerivative I E (TangentSpace I)} (ht : cov.IsTorsionFree) (b : Module.Basis ι 𝕜 E) (x₀ : M) (hx : x ∈ (extChartAt I x₀).source) (i j k : ι) : christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) i j k x = christoffelSymbol I b (trivializationAt E (TangentSpace I) x₀) (↑cov) j i k x

The Christoffel symbols of a torsion-free connection are symmetric in their lower indices: Γᵏᵢⱼ = Γᵏⱼᵢ in the frame of the canonical tangent-bundle trivialization at x₀.

theorem TauCeti.Manifold.christoffelMap_comm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_5} {x : M} [IsManifold I (minSmoothness 𝕜 2) M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {cov : CovariantDerivative I E (TangentSpace I)} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] [Fintype ι] (ht : cov.IsTorsionFree) (b : Module.Basis ι 𝕜 E) (x₀ : M) (hx : x ∈ (extChartAt I x₀).source) (v w : E) : ((christoffelMap b ⋯ x) v) w = ((christoffelMap b ⋯ x) w) v

The Christoffel map of a torsion-free connection is symmetric. Read in the canonical tangent-bundle trivialization at x₀, the model-space Christoffel map of a torsion-free covariant derivative is a symmetric bilinear map.

theorem TauCeti.Manifold.covariantDerivative_extend_eq_christoffelMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {ι : Type u_5} {x : M} [IsManifold I (minSmoothness 𝕜 2) M] [ContMDiffVectorBundle 1 E (TangentSpace I) I] {cov : CovariantDerivative I E (TangentSpace I)} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] [Fintype ι] (b : Module.Basis ι 𝕜 E) (v w : TangentSpace I x) : (↑cov (FiberBundle.extend E w) x) v = ((christoffelMap b ⋯ x) w) v

The Christoffel map in the chart at a point. At x, a covariant derivative differentiates the extension W = FiberBundle.extend E w of a tangent vector w at x, the vector field with constant coordinates w in the canonical tangent-bundle trivialization at x, along v by the Christoffel map read in that trivialization: ∇_v W = Γ(w, v).