The first Bianchi identity

For a torsion-free smooth connection on the tangent bundle, curvature satisfies R(X,Y)Z + R(Y,Z)X + R(Z,X)Y = 0.

Together with the skew-adjointness of metric curvature, this identity gives the pair-interchange symmetry of the Riemann tensor and symmetry of its Ricci contraction.

The sign convention and identity follow J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7 (curvature symmetries).

theorem 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] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] (ht : cov.IsTorsionFree) {X Y Z : (x : M) → TangentSpace I 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⟩) (x : M) : cov.curvatureOperator X Y Z x + cov.curvatureOperator Y Z X x + cov.curvatureOperator Z X Y x = 0

The first Bianchi identity for smooth vector fields and a torsion-free smooth connection on the tangent bundle.

theorem CovariantDerivative.curvatureTensor_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] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [FiniteDimensional ℝ E] [T2Space M] (ht : cov.torsion = 0) (x : M) (u v w : TangentSpace I x) : (((cov.curvatureTensor x) u) v) w + (((cov.curvatureTensor x) v) w) u + (((cov.curvatureTensor x) w) u) v = 0

The first Bianchi identity on tangent vectors. It applies in particular to the Levi-Civita connection, which has zero torsion.

theorem CovariantDerivative.IsMetricCompatible.inner_curvatureTensor_swap_pairs {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] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [FiniteDimensional ℝ E] [T2Space M] [Bundle.RiemannianBundle (TangentSpace I)] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (u v w z : TangentSpace I x) : inner ℝ ((((cov.curvatureTensor x) u) v) w) z = inner ℝ ((((cov.curvatureTensor x) w) z) u) v

The metric-lowered curvature tensor of a metric-compatible torsion-free connection is unchanged when its two pairs of arguments are interchanged.