The divergence of the Weyl tensor

For a metric-compatible torsion-free connection on the tangent bundle of a Riemannian manifold of dimension n ≠ 2, the divergence of the Weyl tensor is a multiple of the Cotton tensor:

∑ᵢ (∇_{eᵢ} W)(eᵢ, u, v, w) = (n - 3) C(u, v, w)

in any orthonormal basis eᵢ, where C(u, v, w) = (∇_w P)(u, v) - (∇_v P)(u, w) and P is the Schouten tensor. In dimension 3 the left side vanishes because W does, while C is the obstruction to local conformal flatness; in dimension at least 4 a metric with vanishing Weyl tensor therefore has vanishing Cotton tensor, which is the integrability condition behind the Weyl–Schouten theorem.

The covariant derivative of W = Rm - P ⊙ g is ∇_d W = ∇_d Rm - (∇_d P) ⊙ g, because the metric is parallel. We define it by this formula (CovariantDerivative.derivWeylTensor) and show that it satisfies the Leibniz rule characterizing the covariant derivative of a tensor (CovariantDerivative.IsMetricCompatible.derivWeylTensor_eq_mvfderiv_sub). The divergence of Rm is the antisymmetrized derivative of Ricci curvature by the contracted second Bianchi identity, and the divergence of (∇P) ⊙ g involves the divergence of P, which the twice contracted Bianchi identity 2 div Ric = d Scal identifies with d (tr_g P). The difference is (n - 3) C.

Main declarations

• CovariantDerivative.derivWeylTensor: the covariant derivative of the Weyl tensor, with CovariantDerivative.IsMetricCompatible.derivWeylTensor_eq_mvfderiv_sub its Leibniz rule on smooth vector fields.
• CovariantDerivative.IsMetricCompatible.sum_derivWeylTensor_self_eq_mul_cottonTensor: div W = (n - 3) C.
• CovariantDerivative.IsMetricCompatible.cottonTensor_eq_zero_of_eventually_weylTensor_eq_zero: away from dimensions 2 and 3, vanishing Weyl tensor near a point forces vanishing Cotton tensor at that point.

References

• A. L. Besse, Einstein Manifolds, Springer (1987), Section 1.G (the Cotton tensor and the divergence of the Weyl tensor).
• J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), Section 2.

noncomputable def CovariantDerivative.derivWeylTensor {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 (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (d : TangentSpace I x) : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ

The covariant derivative of the Weyl tensor along d, cov.derivWeylTensor x d u v w z = (∇_d W)(u, v, w, z), defined as ⟨(∇_d R)(u, v)w, z⟩ - ((∇_d P) ⊙ g)(u, v, w, z) with P the Schouten tensor. For a metric-compatible connection the metric is parallel, so this is the covariant derivative of W = Rm - P ⊙ g; on smooth vector fields it is given by the Leibniz rule CovariantDerivative.IsMetricCompatible.derivWeylTensor_eq_mvfderiv_sub.

@[simp]

theorem CovariantDerivative.derivWeylTensor_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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (d u v w z : TangentSpace I x) : ((((cov.derivWeylTensor x d) u) v) w) z = inner ℝ (((((cov.derivCurvatureTensor cov x) d) u) v) w) z - ((((cov.derivSchoutenTensor x) u) z) d * inner ℝ v w + (((cov.derivSchoutenTensor x) v) w) d * inner ℝ u z - (((cov.derivSchoutenTensor x) u) w) d * inner ℝ v z - (((cov.derivSchoutenTensor x) v) z) d * inner ℝ u w)

Evaluation of the covariant derivative of the Weyl tensor: (∇_d W)(u, v, w, z) = ⟨(∇_d R)(u, v)w, z⟩ - ((∇_d P) ⊙ g)(u, v, w, z).

theorem CovariantDerivative.IsMetricCompatible.derivWeylTensor_eq_mvfderiv_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] [Bundle.RiemannianBundle (TangentSpace I)] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I (↑⊤) E (TangentSpace I)] (hcov : cov.IsMetricCompatible) {U V W Z : (y : M) → TangentSpace I y} (hU : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, U y⟩) (hV : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, V y⟩) (hW : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, W y⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (y : M) => ⟨y, Z y⟩) (x : M) (d : TangentSpace I x) : ((((cov.derivWeylTensor x d) (U x)) (V x)) (W x)) (Z x) = ((d% fun (y : M) => ((((cov.weylTensor y) (U y)) (V y)) (W y)) (Z y)) x) d - ((((cov.weylTensor x) ((↑cov U x) d)) (V x)) (W x)) (Z x) - ((((cov.weylTensor x) (U x)) ((↑cov V x) d)) (W x)) (Z x) - ((((cov.weylTensor x) (U x)) (V x)) ((↑cov W x) d)) (Z x) - ((((cov.weylTensor x) (U x)) (V x)) (W x)) ((↑cov Z x) d)

The Leibniz rule for ∇W. For a metric-compatible connection and smooth vector fields, (∇_d W)(U, V, W, Z) = d (W(U, V, W, Z)) - W(∇_d U, V, W, Z) - W(U, ∇_d V, W, Z) - W(U, V, ∇_d W, Z) - W(U, V, W, ∇_d Z). This characterizes derivWeylTensor as the covariant derivative of the Weyl tensor.

theorem CovariantDerivative.IsMetricCompatible.sum_derivWeylTensor_self_eq_mul_cottonTensor {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 (TangentSpace I)] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I (↑⊤) E (TangentSpace I)] {ι : Type u_4} [Fintype ι] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (hn : Module.finrank ℝ E ≠ 2) (x : M) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (u v w : TangentSpace I x) : ∑ i : ι, ((((cov.derivWeylTensor x (b i)) (b i)) u) v) w = (↑(Module.finrank ℝ E) - 3) * (((cov.cottonTensor x) u) v) w

The divergence of the Weyl tensor. For a metric-compatible torsion-free connection in dimension n ≠ 2, ∑ᵢ (∇_{eᵢ} W)(eᵢ, u, v, w) = (n - 3) C(u, v, w) in any orthonormal basis, where C is the Cotton tensor.

theorem CovariantDerivative.IsMetricCompatible.derivWeylTensor_eq_zero_of_eventually_weylTensor_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] [Bundle.RiemannianBundle (TangentSpace I)] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I (↑⊤) E (TangentSpace I)] (hcov : cov.IsMetricCompatible) {x : M} (h : ∀ᶠ (y : M) in nhds x, cov.weylTensor y = 0) (d : TangentSpace I x) : cov.derivWeylTensor x d = 0

A Weyl tensor that vanishes near a point has zero covariant derivative there.

theorem CovariantDerivative.IsMetricCompatible.cottonTensor_eq_zero_of_eventually_weylTensor_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] [Bundle.RiemannianBundle (TangentSpace I)] {cov : CovariantDerivative I E (TangentSpace I)} [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I (↑⊤) E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (hn₂ : Module.finrank ℝ E ≠ 2) (hn₃ : Module.finrank ℝ E ≠ 3) {x : M} (h : ∀ᶠ (y : M) in nhds x, cov.weylTensor y = 0) : cov.cottonTensor x = 0

In dimensions other than 2 and 3, vanishing Weyl tensor near a point forces vanishing Cotton tensor at the point, by div W = (dim M - 3) C.