The covariant derivative of the curvature tensor

Let ∇ be a smooth connection on a finite-rank vector bundle V with curvature tensor R, and let ∇ᵀ be a connection on the tangent bundle. The covariant derivative of the curvature is

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

Its value at a point depends only on the values of X, Y, Z and σ there, so it is a pointwise tensor, CovariantDerivative.derivCurvatureTensor, linear in three tangent vectors and one bundle vector. On the tangent bundle with ∇ = ∇ᵀ this is the classical tensor ∇R of an affine connection, whose vanishing says the connection has parallel curvature, and which enters the contracted Bianchi identity and the normal-coordinate expansion of a Riemannian metric.

The construction uses globally smooth extensions of fibre vectors and the tensoriality criterion TauCeti.Manifold.eq_of_contMDiff_tensorial. Its characteristic equation derivCurvatureTensor_apply evaluates it on any smooth fields and section. In this form the second Bianchi identity covariantDerivative_curvatureOperator_cyclic_eq_zero becomes the pointwise identity derivCurvatureTensor_cyclic_eq_zero.

Main definitions and results

• CovariantDerivative.derivCurvatureTensor: the covariant derivative ∇R of the curvature tensor, with derivCurvatureTensor cov covT x v u w s = (∇_v R)(u, w) s.
• CovariantDerivative.derivCurvatureTensor_apply and CovariantDerivative.derivCurvatureTensor_apply_eq_curvatureOperator: its value on smooth fields and sections.
• CovariantDerivative.derivCurvatureTensor_apply_of_contMDiffOn: evaluation on local smooth fields and sections, including local frames.
• CovariantDerivative.derivCurvatureTensor_antisymm: ∇R is antisymmetric in its two curvature arguments.
• CovariantDerivative.derivCurvatureTensor_eq_zero_of_curvatureTensor_eq_zero: ∇R = 0 for a flat connection ∇.
• CovariantDerivative.derivCurvatureTensor_cyclic_eq_zero: the second Bianchi identity (∇_u R)(v, w) + (∇_v R)(w, u) + (∇_w R)(u, v) = 0, for a smooth torsion-free ∇ᵀ.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 7, Proposition 7.5 (the differential Bianchi identity, with ∇R as a tensor field).

noncomputable def CovariantDerivative.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) → 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) : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] V x →ₗ[ℝ] V x

The covariant derivative of the curvature tensor of a smooth connection ∇ on V, taken with ∇ on V and a connection ∇ᵀ on the tangent bundle: the tensor with derivCurvatureTensor cov covT x v u w s = (∇_v R)(u, w) s, where on smooth fields and sections

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

by CovariantDerivative.derivCurvatureTensor_apply. On the tangent bundle, with ∇ = ∇ᵀ, this is the tensor ∇R of an affine connection.

theorem CovariantDerivative.derivCurvatureTensor_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] {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)) {Y Z : (y : M) → TangentSpace I y} {σ : (y : M) → V y} (x : M) (v : TangentSpace I x) (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⟩) : ((((cov.derivCurvatureTensor covT x) v) (Y x)) (Z x)) (σ x) = (↑cov (cov.curvatureOperator Y Z σ) x) v - (((cov.curvatureTensor x) ((↑covT Y x) v)) (Z x)) (σ x) - (((cov.curvatureTensor x) (Y x)) ((↑covT Z x) v)) (σ x) - (((cov.curvatureTensor x) (Y x)) (Z x)) ((↑cov σ x) v)

The covariant derivative of the curvature tensor on smooth fields and a smooth section: (∇_v R)(Y, Z) σ = ∇_v (R(Y, Z) σ) - R(∇ᵀ_v Y, Z) σ - R(Y, ∇ᵀ_v Z) σ - R(Y, Z) (∇_v σ).

theorem CovariantDerivative.derivCurvatureTensor_apply_of_contMDiffOn {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)) {Y Z : (y : M) → TangentSpace I y} {σ : (y : M) → V y} (x : M) {U : Set M} (hU : IsOpen U) (hx : x ∈ U) (v : TangentSpace I x) (hY : ContMDiffOn I I.tangent (↑⊤) (fun (y : M) => ⟨y, Y y⟩) U) (hZ : ContMDiffOn I I.tangent (↑⊤) (fun (y : M) => ⟨y, Z y⟩) U) (hσ : ContMDiffOn I (I.prod (modelWithCornersSelf ℝ F)) (↑⊤) (fun (y : M) => ⟨y, σ y⟩) U) : ((((cov.derivCurvatureTensor covT x) v) (Y x)) (Z x)) (σ x) = (↑cov (cov.curvatureOperator Y Z σ) x) v - (((cov.curvatureTensor x) ((↑covT Y x) v)) (Z x)) (σ x) - (((cov.curvatureTensor x) (Y x)) ((↑covT Z x) v)) (σ x) - (((cov.curvatureTensor x) (Y x)) (Z x)) ((↑cov σ x) v)

The covariant curvature derivative evaluated on fields smooth only on a neighbourhood. This applies in particular to local frames, without choosing global frame extensions.

theorem CovariantDerivative.derivCurvatureTensor_apply_eq_curvatureOperator {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)) {Y Z : (y : M) → TangentSpace I y} {σ : (y : M) → V y} [covT.ContMDiffCovariantDerivative ↑⊤] {X : (y : M) → TangentSpace I y} (x : M) (hX : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, X 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⟩) : ((((cov.derivCurvatureTensor covT x) (X x)) (Y x)) (Z x)) (σ x) = (↑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

For a smooth connection ∇ᵀ on the tangent bundle, the covariant derivative of the curvature tensor along a smooth vector field X is given entirely by curvature operators: (∇_X R)(Y, Z) σ = ∇_X (R(Y, Z) σ) - R(∇ᵀ_X Y, Z) σ - R(Y, ∇ᵀ_X Z) σ - R(Y, Z) (∇_X σ).

theorem CovariantDerivative.derivCurvatureTensor_antisymm {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) (v u w : TangentSpace I x) : (((cov.derivCurvatureTensor covT x) v) u) w = -(((cov.derivCurvatureTensor covT x) v) w) u

The covariant derivative of the curvature tensor is antisymmetric in its two curvature arguments: (∇_v R)(u, w) = -(∇_v R)(w, u).

@[simp]

theorem CovariantDerivative.derivCurvatureTensor_self {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) (v u : TangentSpace I x) : (((cov.derivCurvatureTensor covT x) v) u) u = 0

The covariant derivative of the curvature tensor vanishes when its two curvature arguments coincide.

theorem CovariantDerivative.derivCurvatureTensor_eq_zero_of_curvatureTensor_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] {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)) (h : ∀ (x : M), cov.curvatureTensor x = 0) (x : M) : cov.derivCurvatureTensor covT x = 0

The covariant derivative of the curvature tensor of a flat connection vanishes.

theorem CovariantDerivative.derivCurvatureTensor_cyclic_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] {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)) [covT.ContMDiffCovariantDerivative ↑⊤] (ht : covT.torsion = 0) (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 = 0

The second Bianchi identity, pointwise: for a smooth connection ∇ on V and a smooth torsion-free connection ∇ᵀ on the tangent bundle, (∇_u R)(v, w) + (∇_v R)(w, u) + (∇_w R)(u, v) = 0.