The Ricci identity for the second covariant derivative

Let ∇ be a smooth connection on a vector bundle V and ∇ᵀ a connection on the tangent bundle, and let ∇²σ(X, Y) = ∇_X (∇_Y σ) - ∇_{∇ᵀ_X Y} σ be the second covariant derivative of a smooth section σ of V (CovariantDerivative.secondCovariantDerivative).

The Ricci identity expresses the failure of ∇²σ to be symmetric through the curvature R of ∇ and the torsion T of ∇ᵀ:

∇²σ(u, v) - ∇²σ(v, u) = R(u, v) σ - ∇_{T(u, v)} σ,

where T(X, Y) = ∇ᵀ_X Y - ∇ᵀ_Y X - [X, Y] is Mathlib's CovariantDerivative.torsion. For a torsion-free ∇ᵀ, such as a Levi-Civita connection, the torsion term disappears and the antisymmetric part of ∇²σ is the curvature R(u, v) σ. For V the tangent bundle this is the Ricci identity for vector fields. It is the rule for commuting covariant derivatives used in Bochner and Weitzenböck formulas.

Main results

• CovariantDerivative.secondCovariantDerivative_sub_swap: the Ricci identity with its torsion correction.
• CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree: the Ricci identity ∇²σ(u, v) - ∇²σ(v, u) = R(u, v) σ for a torsion-free connection on the tangent bundle.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (the Ricci identities).

theorem CovariantDerivative.secondCovariantDerivative_sub_swap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (covT : CovariantDerivative I E (TangentSpace I)) {σ : (y : M) → V y} [FiniteDimensional ℝ E] [T2Space M] [FiniteDimensional ℝ F] [ContMDiffVectorBundle (↑⊤) F V I] (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩) (x : M) (u v : TangentSpace I x) : ((cov.secondCovariantDerivative covT σ x) u) v - ((cov.secondCovariantDerivative covT σ x) v) u = (((cov.curvatureTensor x) u) v) (σ x) - (↑cov σ x) (((covT.torsion x) u) v)

The Ricci identity, with its torsion correction. For a smooth section σ, the antisymmetric part of its second covariant derivative is the curvature of ∇ applied to σ, corrected by the covariant derivative of σ along the torsion of ∇ᵀ:

∇²σ(u, v) - ∇²σ(v, u) = R(u, v) σ - ∇_{T(u, v)} σ.

theorem CovariantDerivative.secondCovariantDerivative_sub_swap_of_isTorsionFree {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (covT : CovariantDerivative I E (TangentSpace I)) {σ : (y : M) → V y} [FiniteDimensional ℝ E] [T2Space M] [FiniteDimensional ℝ F] [ContMDiffVectorBundle (↑⊤) F V I] (ht : covT.IsTorsionFree) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩) (x : M) (u v : TangentSpace I x) : ((cov.secondCovariantDerivative covT σ x) u) v - ((cov.secondCovariantDerivative covT σ x) v) u = (((cov.curvatureTensor x) u) v) (σ x)

The Ricci identity. For a torsion-free connection ∇ᵀ on the tangent bundle, the antisymmetric part of the second covariant derivative of a smooth section σ is the curvature of ∇ applied to σ: ∇²σ(u, v) - ∇²σ(v, u) = R(u, v) σ.

theorem CovariantDerivative.secondCovariantDerivative_comm_of_curvatureTensor_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : M → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(x : M) → AddCommGroup (V x)] [(x : M) → Module ℝ (V x)] [(x : M) → TopologicalSpace (V x)] [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (covT : CovariantDerivative I E (TangentSpace I)) {σ : (y : M) → V y} [FiniteDimensional ℝ E] [T2Space M] [FiniteDimensional ℝ F] [ContMDiffVectorBundle (↑⊤) F V I] {x : M} (hT : covT.torsion x = 0) (hR : cov.curvatureTensor x = 0) (u v : TangentSpace I x) : ((cov.secondCovariantDerivative covT σ x) u) v = ((cov.secondCovariantDerivative covT σ x) v) u

If the torsion of ∇ᵀ and the curvature of ∇ both vanish at x, then the second covariant derivative of every section at x is symmetric. (For a section that is not smooth, both sides are the junk value 0.)