Contracting the covariant derivative of the curvature

Let ∇ be a smooth connection on the tangent bundle of a Riemannian manifold M. This file contracts the covariant derivative of its curvature, the tensor CovariantDerivative.derivCurvatureTensor, whose value on vector fields is

(∇_v R)(Y, Z) σ = ∇_v (R(Y, Z) σ) - R(∇_v Y, Z) σ - R(Y, ∇_v Z) σ - R(Y, Z) (∇_v σ)

(CovariantDerivative.derivCurvatureTensor_apply). It shows that the trace defining the Ricci tensor commutes with covariant differentiation. For a metric-compatible torsion-free connection, the contractions use pair symmetry of ⟪(∇_v R)(Y, Z) σ, U⟫, from CovariantDerivative.IsMetricCompatible.inner_derivCurvatureTensor_swap_pairs in DifferentiatedSymmetries.

The trace is taken in a local frame at the point: the frame of a trivialization, cut off by a bump function to globally smooth vector fields. Differentiating the frame coefficients by the local frame formula TauCeti.Manifold.covariantDerivative_eq_frameCovariantDerivative_add_sum shows that the trace commutes with covariant differentiation. The cyclic form is the second Bianchi identity CovariantDerivative.derivCurvatureTensor_cyclic_eq_zero.

On tangent vectors, derivRicciTensor_eq_trace identifies ∇Ric with the trace of ∇R. Contracting the second Bianchi identity gives

tr (z ↦ (∇_z R)(u, v) w) = (∇_u Ric)(v, w) - (∇_v Ric)(u, w).

This identity requires only a torsion-free affine connection. An orthonormal basis computes its trace when a metric is present. For a metric-compatible connection, pair interchange gives the Riemannian divergence formula

∑ᵢ (∇_{eᵢ} Rm)(eᵢ, u, v, w) = (∇_w Ric)(u, v) - (∇_v Ric)(u, w),

with Rm(u, v, w, z) = ⟨R(u, v)w, z⟩. Contracting once more, and using that the metric trace commutes with covariant differentiation for a metric-compatible connection, gives the twice contracted second Bianchi identity

2 ∑ᵢ (∇_{eᵢ} Ric)(eᵢ, v) = d Scal(v),

that is 2 div Ric = d Scal. These differential contractions underlie the divergence of the Weyl tensor and the Cotton tensor. The derivative of the Ricci tensor is the covariant derivative of a bilinear tensor; exists_frame_sum_derivCurvatureTensor identifies it with the trace of derivCurvatureTensor.

Main results

• CovariantDerivative.exists_frame_sum_derivCurvatureTensor: contracting (∇_v R)(·, B) C against the output gives (∇_v Ric)(B, C).
• CovariantDerivative.derivRicciTensor: the covariant derivative of Ricci curvature, with its direction of differentiation last.
• CovariantDerivative.derivRicciTensor_eq_trace: covariant differentiation commutes with the Ricci trace, without a metric assumption.
• CovariantDerivative.trace_derivCurvatureTensor_eq_sub: the metric-free first contracted second Bianchi identity.
• CovariantDerivative.sum_inner_derivCurvatureTensor_eq_sub: its orthonormal-basis form.
• CovariantDerivative.IsMetricCompatible.sum_inner_derivCurvatureTensor_self_eq_sub: the Riemannian divergence formula.
• CovariantDerivative.IsMetricCompatible.sum_derivRicciTensor_self_eq_mvfderiv_scalarCurvature: the trace of ∇Ric is the derivative of scalar curvature.
• CovariantDerivative.IsMetricCompatible.two_mul_sum_derivRicciTensor_eq_mvfderiv_scalarCurvature: the twice contracted second Bianchi identity 2 div Ric = d Scal.

References

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

theorem CovariantDerivative.exists_frame_sum_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] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) : ∃ (F : Fin (Module.finrank ℝ E) → (y : M) → TangentSpace I y) (c : Fin (Module.finrank ℝ E) → TangentSpace I x →ₗ[ℝ] ℝ), (∀ (i : Fin (Module.finrank ℝ E)), ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, F i y⟩) ∧ (∀ (i j : Fin (Module.finrank ℝ E)), (c i) (F j x) = if i = j then 1 else 0) ∧ (∀ (w : TangentSpace I x), ∑ i : Fin (Module.finrank ℝ E), (c i) w • F i x = w) ∧ ∀ (v : TangentSpace I x) {B C : (y : M) → TangentSpace I y}, (ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, B y⟩) → (ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, C y⟩) → ∑ i : Fin (Module.finrank ℝ E), (c i) (((((cov.derivCurvatureTensor cov x) v) (F i x)) (B x)) (C x)) = ((d% fun (y : M) => ((cov.ricciTensor y) (B y)) (C y)) x) v - ((cov.ricciTensor x) ((↑cov B x) v)) (C x) - ((cov.ricciTensor x) (B x)) ((↑cov C x) v)

Contracting (∇_v R)(·, B) C against the output, in a local frame at x, gives the covariant derivative (∇_v Ric)(B, C) = v (Ric(B, C)) - Ric(∇_v B, C) - Ric(B, ∇_v C) of the Ricci tensor. The frame is a family of global smooth vector fields F forming a basis at x, with dual coordinate functionals c at x.

noncomputable def CovariantDerivative.derivRicciTensor {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 ↑⊤] (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ

The covariant derivative of Ricci curvature, with the direction of differentiation last: derivRicciTensor x u v w = (∇_w Ric)(u, v).

theorem CovariantDerivative.derivRicciTensor_def {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 ↑⊤] (x : M) : cov.derivRicciTensor x = cov.derivBilinearTensor (fun (y : M) => (cov.ricciTensor y).toContinuousBilinearMap) x

The covariant derivative of Ricci curvature uses the native bilinear-tensor derivative.

theorem CovariantDerivative.derivRicciTensor_apply {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 ↑⊤] {σ τ : (y : M) → TangentSpace I y} {x : M} (hσ : (MDiffAt fun (y : M) => ⟨y, σ y⟩) x) (hτ : (MDiffAt fun (y : M) => ⟨y, τ y⟩) x) (v : TangentSpace I x) : (((cov.derivRicciTensor x) (σ x)) (τ x)) v = ((d% fun (y : M) => ((cov.ricciTensor y) (σ y)) (τ y)) x) v - ((cov.ricciTensor x) ((↑cov σ x) v)) (τ x) - ((cov.ricciTensor x) (σ x)) ((↑cov τ x) v)

On vector fields differentiable at x, the derivative of Ricci curvature is the directional derivative of its evaluation minus the two connection corrections.

theorem CovariantDerivative.derivRicciTensor_eq_trace {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 ↑⊤] (x : M) (u w v : TangentSpace I x) : (((cov.derivRicciTensor x) u) w) v = (LinearMap.trace ℝ (TangentSpace I x)) ((((cov.derivCurvatureTensor cov x) v).flip u).flip w)

Covariant differentiation commutes with the trace defining Ricci curvature: (∇_v Ric)(u, w) = tr (z ↦ (∇_v R)(z, u) w). No metric is needed.

theorem CovariantDerivative.trace_derivCurvatureTensor_eq_sub {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) (u v w : TangentSpace I x) : (LinearMap.trace ℝ (TangentSpace I x)) ((((cov.derivCurvatureTensor cov x).flip u).flip v).flip w) = (((cov.derivRicciTensor x) v) w) u - (((cov.derivRicciTensor x) u) w) v

The metric-free first contracted second Bianchi identity: tr (z ↦ (∇_z R)(u, v) w) = (∇_u Ric)(v, w) - (∇_v Ric)(u, w).

theorem CovariantDerivative.sum_inner_derivCurvatureTensor_eq_derivRicciTensor {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 ↑⊤] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {ι : Type u_4} [Fintype ι] (x : M) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (u w v : TangentSpace I x) : ∑ i : ι, inner ℝ (b i) (((((cov.derivCurvatureTensor cov x) v) (b i)) u) w) = (((cov.derivRicciTensor x) u) w) v

In any orthonormal basis, contracting the first curvature argument of ∇R against the output gives ∇Ric. The connection need not preserve the metric.

theorem CovariantDerivative.sum_inner_derivCurvatureTensor_eq_sub {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 ↑⊤] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {ι : Type u_4} [Fintype ι] (ht : cov.torsion = 0) (x : M) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (u v w : TangentSpace I x) : ∑ i : ι, inner ℝ (b i) (((((cov.derivCurvatureTensor cov x) (b i)) u) v) w) = (((cov.derivRicciTensor x) v) w) u - (((cov.derivRicciTensor x) u) w) v

The first contracted second Bianchi identity in an arbitrary orthonormal basis. The connection is torsion-free, but metric compatibility is not required.

theorem CovariantDerivative.IsMetricCompatible.derivRicciTensor_comm {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 ↑⊤] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (u v : TangentSpace I x) : ((cov.derivRicciTensor x) u) v = ((cov.derivRicciTensor x) v) u

For a metric-compatible torsion-free connection, the covariant derivative of Ricci is symmetric in the two Ricci arguments.

theorem CovariantDerivative.IsMetricCompatible.sum_inner_derivCurvatureTensor_self_eq_sub {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 ↑⊤] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {ι : Type u_4} [Fintype ι] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (u v w : TangentSpace I x) : ∑ i : ι, inner ℝ (((((cov.derivCurvatureTensor cov x) (b i)) (b i)) u) v) w = (((cov.derivRicciTensor x) u) v) w - (((cov.derivRicciTensor x) u) w) v

The divergence of the metric-lowered Riemann tensor is the antisymmetrized derivative of Ricci curvature. The sign uses Rm(u, v, w, z) = ⟨R(u, v)w, z⟩.

theorem CovariantDerivative.IsMetricCompatible.sum_derivRicciTensor_self_eq_mvfderiv_scalarCurvature {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 ↑⊤] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {ι : Type u_4} [Fintype ι] (hcov : cov.IsMetricCompatible) (x : M) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (v : TangentSpace I x) : ∑ i : ι, (((cov.derivRicciTensor x) (b i)) (b i)) v = (d% cov.scalarCurvature x) v

For a metric-compatible connection, the metric trace of the covariant derivative of Ricci curvature is the derivative of scalar curvature: ∑ᵢ (∇_v Ric)(eᵢ, eᵢ) = d Scal(v) in any orthonormal basis.

theorem CovariantDerivative.IsMetricCompatible.two_mul_sum_derivRicciTensor_eq_mvfderiv_scalarCurvature {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 ↑⊤] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {ι : Type u_4} [Fintype ι] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (v : TangentSpace I x) : 2 * ∑ i : ι, (((cov.derivRicciTensor x) (b i)) v) (b i) = (d% cov.scalarCurvature x) v

The twice contracted second Bianchi identity 2 div Ric = d Scal: for a metric-compatible torsion-free connection, 2 ∑ᵢ (∇_{eᵢ} Ric)(eᵢ, v) = d Scal(v) in any orthonormal basis.