The second Bianchi identity with torsion

For a smooth connection on a vector bundle, differentiating its curvature with an arbitrary connection on the tangent bundle gives

(∇_u R)(v,w) + (∇_v R)(w,u) + (∇_w R)(u,v) = -R(T(u,v),w) - R(T(v,w),u) - R(T(w,u),v).

Here T(u,v) = ∇ᵀ_u v - ∇ᵀ_v u - [u,v] is the native torsion tensor. The sign uses R(u,v) = [∇_u,∇_v] - ∇_[u,v]. This is the tensor formula for the covariant exterior closedness of curvature when the auxiliary tangent connection has torsion. It includes the usual differential Bianchi identity when torsion vanishes at the point in question.

The auxiliary tangent connection need not be smooth: only its values at the point enter the formula. No metric is needed. The proof uses the torsion-independent identity CovariantDerivative.curvatureOperator_commutator_cyclic_eq_zero and the characteristic evaluation formula for CovariantDerivative.derivCurvatureTensor.

References

• S. Kobayashi and K. Nomizu, Foundations of Differential Geometry, Vol. I, Chapter III (the Bianchi identities for connections with torsion).

theorem CovariantDerivative.derivCurvatureTensor_cyclic_eq_neg_torsion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [T2Space M] [IsManifold I (↑⊤) M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ 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] [ContMDiffVectorBundle (↑⊤) F V I] (cov : CovariantDerivative I F V) [cov.ContMDiffCovariantDerivative ↑⊤] (covT : CovariantDerivative I E (TangentSpace I)) (x : M) (u v w : TangentSpace I x) : (((cov.derivCurvatureTensor covT x) u) v) w + (((cov.derivCurvatureTensor covT x) v) w) u + (((cov.derivCurvatureTensor covT x) w) u) v = -(((cov.curvatureTensor x) (((covT.torsion x) u) v)) w + ((cov.curvatureTensor x) (((covT.torsion x) v) w)) u + ((cov.curvatureTensor x) (((covT.torsion x) w) u)) v)

The second Bianchi identity with torsion. The cyclic covariant derivative of curvature is minus the cyclic curvature contraction with the torsion of the tangent connection. The identity is an equality of endomorphisms of the bundle fibre.