The second Bianchi identity

Let ∇ be a smooth connection on a vector bundle V, with curvature R(X, Y) = [∇_X, ∇_Y] - ∇_[X, Y], and let ∇ᵀ be a smooth torsion-free connection on the tangent bundle. The covariant derivative of the curvature along a vector field X is

(∇_X R)(Y, Z) σ = ∇_X (R(Y, Z) σ) - R(∇ᵀ_X Y, Z) σ - R(Y, ∇ᵀ_X Z) σ - R(Y, Z) (∇_X σ),

and the second (differential) Bianchi identity states that its cyclic sum over X, Y, Z vanishes. For V the tangent bundle and ∇ = ∇ᵀ this is the classical identity (∇_X R)(Y, Z) + (∇_Y R)(Z, X) + (∇_Z R)(X, Y) = 0; for a general bundle it is the operator form of d_∇ R = 0.

The proof first establishes the identity [∇_X, R(Y, Z)] + R(X, [Y, Z]) + (cyclic) = 0, which holds for every smooth connection: the third-order terms cancel by the Jacobi identity for commutators of operators, and the remaining first-order terms by the Jacobi identity for the Lie bracket of vector fields. Torsion-freeness of ∇ᵀ then converts the bracket terms into the derivative terms of ∇R.

Main results

• CovariantDerivative.curvatureOperator_commutator_cyclic_eq_zero: the cyclic sum of [∇_X, R(Y, Z)] σ + R(X, [Y, Z]) σ vanishes, for any smooth connection.
• CovariantDerivative.covariantDerivative_curvatureOperator_cyclic_eq_zero: the second Bianchi identity, for a smooth connection on any vector bundle and a smooth torsion-free connection on the tangent bundle.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176, 2018, Chapter 7, Proposition 7.5 (the differential Bianchi identity).

theorem CovariantDerivative.curvatureOperator_commutator_cyclic_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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 ↑⊤] {X Y Z : (x : M) → TangentSpace I x} {σ : (x : M) → V x} (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩) (x : M) : (↑cov (cov.curvatureOperator Y Z σ) x) (X x) - cov.curvatureOperator Y Z (fun (y : M) => (↑cov σ y) (X y)) x + cov.curvatureOperator X (VectorField.mlieBracket I Y Z) σ x + ((↑cov (cov.curvatureOperator Z X σ) x) (Y x) - cov.curvatureOperator Z X (fun (y : M) => (↑cov σ y) (Y y)) x + cov.curvatureOperator Y (VectorField.mlieBracket I Z X) σ x) + ((↑cov (cov.curvatureOperator X Y σ) x) (Z x) - cov.curvatureOperator X Y (fun (y : M) => (↑cov σ y) (Z y)) x + cov.curvatureOperator Z (VectorField.mlieBracket I X Y) σ x) = 0

The cyclic sum of [∇_X, R(Y, Z)] σ + R(X, [Y, Z]) σ vanishes for every smooth connection. This is the torsion-independent core of the second Bianchi identity covariantDerivative_curvatureOperator_cyclic_eq_zero.

theorem CovariantDerivative.covariantDerivative_curvatureOperator_cyclic_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace 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 ↑⊤] {X Y Z : (x : M) → TangentSpace I x} {σ : (x : M) → V x} (covT : CovariantDerivative I E (TangentSpace I)) [covT.ContMDiffCovariantDerivative ↑⊤] (ht : covT.IsTorsionFree) (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (x : M) => ⟨x, σ x⟩) (x : M) : (↑cov (cov.curvatureOperator Y Z σ) x) (X x) - cov.curvatureOperator (fun (y : M) => (↑covT Y y) (X y)) Z σ x - cov.curvatureOperator Y (fun (y : M) => (↑covT Z y) (X y)) σ x - cov.curvatureOperator Y Z (fun (y : M) => (↑cov σ y) (X y)) x + ((↑cov (cov.curvatureOperator Z X σ) x) (Y x) - cov.curvatureOperator (fun (y : M) => (↑covT Z y) (Y y)) X σ x - cov.curvatureOperator Z (fun (y : M) => (↑covT X y) (Y y)) σ x - cov.curvatureOperator Z X (fun (y : M) => (↑cov σ y) (Y y)) x) + ((↑cov (cov.curvatureOperator X Y σ) x) (Z x) - cov.curvatureOperator (fun (y : M) => (↑covT X y) (Z y)) Y σ x - cov.curvatureOperator X (fun (y : M) => (↑covT Y y) (Z y)) σ x - cov.curvatureOperator X Y (fun (y : M) => (↑cov σ y) (Z y)) x) = 0

The second Bianchi identity. Let ∇ be a smooth connection on a vector bundle and ∇ᵀ a smooth torsion-free connection on the tangent bundle. Writing (∇_X R)(Y, Z) σ = ∇_X (R(Y, Z) σ) - R(∇ᵀ_X Y, Z) σ - R(Y, ∇ᵀ_X Z) σ - R(Y, Z) (∇_X σ), the cyclic sum (∇_X R)(Y, Z) σ + (∇_Y R)(Z, X) σ + (∇_Z R)(X, Y) σ vanishes.