Algebraic symmetries of the covariant curvature derivative

Covariant differentiation preserves the algebraic first Bianchi identity of a torsion-free connection. Thus, for each fixed direction d, the tensor (∇_d R)(u, v)w has vanishing cyclic sum in u, v, w. This is distinct from the differential second Bianchi identity, whose cyclic sum includes the direction of differentiation.

On a real metric vector bundle, (∇_d R)(u, v) is skew-adjoint whenever the bundle connection is metric-compatible. The auxiliary connection differentiating the two tangent slots need not be metric-compatible or torsion-free. On the tangent bundle these identities, together with antisymmetry in the two curvature slots, give the algebraic symmetries needed to manipulate the curvature derivative in normal-coordinate expansions. For a metric-compatible connection on a metric bundle, CovariantDerivative.IsMetricCompatible.inner_derivCurvatureTensor expresses the metric lowering of ∇R as the derivative of the metric-lowered curvature; on the tangent bundle with a torsion-free connection this gives pair interchange CovariantDerivative.IsMetricCompatible.inner_derivCurvatureTensor_swap_pairs.

The proofs differentiate the existing first Bianchi and metric-curvature identities using CovariantDerivative.derivCurvatureTensor_apply and the metric product rule.

References

• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Chapter 7 (curvature symmetries and their covariant derivatives).

theorem CovariantDerivative.derivCurvatureTensor_cyclic_last_eq_zero {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] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (ht : cov.torsion = 0) (x : M) (d u v w : TangentSpace I x) : ((((cov.derivCurvatureTensor cov x) d) u) v) w + ((((cov.derivCurvatureTensor cov x) d) v) w) u + ((((cov.derivCurvatureTensor cov x) d) w) u) v = 0

The differentiated algebraic first Bianchi identity: the cyclic sum of ∇R over its three curvature arguments vanishes for a torsion-free connection. The differentiation direction is held fixed, unlike in the second Bianchi identity. No metric is needed.

theorem CovariantDerivative.IsMetricCompatible.inner_derivCurvatureTensor_eq_neg {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) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] [IsContMDiffRiemannianBundle I 2 F V] {cov : CovariantDerivative I F V} [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) (covT : CovariantDerivative I E (TangentSpace I)) (x : M) (d u v : TangentSpace I x) (s t : V x) : inner ℝ (((((cov.derivCurvatureTensor covT x) d) u) v) s) t = -inner ℝ s (((((cov.derivCurvatureTensor covT x) d) u) v) t)

The covariant derivative of the curvature of a metric connection is skew-adjoint in its bundle arguments. The connection on the tangent slots is arbitrary. In particular, for a metric connection on the tangent bundle this is last-pair antisymmetry of the metric-lowered ∇R.

theorem CovariantDerivative.IsMetricCompatible.inner_derivCurvatureTensor {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) → NormedAddCommGroup (V x)] [(x : M) → InnerProductSpace ℝ (V x)] [FiberBundle F V] [VectorBundle ℝ F V] [ContMDiffVectorBundle (↑⊤) F V I] [IsContMDiffRiemannianBundle I 2 F V] {cov : CovariantDerivative I F V} [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) (covT : CovariantDerivative I E (TangentSpace I)) (x : M) (v : TangentSpace I x) {Y Z : (y : M) → TangentSpace I y} {σ U : (y : M) → V y} (hY : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Y y⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Z y⟩) (hσ : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, σ y⟩) (hU : ContMDiff I (I.prod (modelWithCornersSelf ℝ F)) ↑⊤ fun (y : M) => ⟨y, U y⟩) : inner ℝ (((((cov.derivCurvatureTensor covT x) v) (Y x)) (Z x)) (σ x)) (U x) = ((d% fun (y : M) => inner ℝ ((((cov.curvatureTensor y) (Y y)) (Z y)) (σ y)) (U y)) x) v - inner ℝ ((((cov.curvatureTensor x) ((↑covT Y x) v)) (Z x)) (σ x)) (U x) - inner ℝ ((((cov.curvatureTensor x) (Y x)) ((↑covT Z x) v)) (σ x)) (U x) - inner ℝ ((((cov.curvatureTensor x) (Y x)) (Z x)) ((↑cov σ x) v)) (U x) - inner ℝ ((((cov.curvatureTensor x) (Y x)) (Z x)) (σ x)) ((↑cov U x) v)

For a metric-compatible connection, pairing (∇_v R)(Y, Z) σ with a section U gives the covariant derivative of the metric-lowered curvature ⟪R(Y, Z) σ, U⟫. The connection covT differentiating the two tangent slots is arbitrary.

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

Pair interchange for the metric-lowered covariant derivative of curvature: (∇_d Rm)(u, v, w, z) = (∇_d Rm)(w, z, u, v).