The Weyl curvature tensor of a smooth connection

The Weyl tensor is the part of the Riemann curvature tensor left after removing the Kulkarni–Nomizu product of the Schouten tensor P with the metric g:

W = Rm - P ⊙ g, so that Rm = W + P ⊙ g,

with Rm(u, v, w, z) = ⟨R(u, v)w, z⟩ and (P ⊙ g)(u, v, w, z) = P(u, z) g(v, w) + P(v, w) g(u, z) - P(u, w) g(v, z) - P(v, z) g(u, w). It is the conformally invariant part of the curvature, and its vanishing characterizes local conformal flatness in dimension at least 4. In dimension 3 the Weyl tensor of a metric-compatible connection vanishes identically, so there the Riemann curvature is Rm = P ⊙ g and is determined by the Ricci curvature.

For a metric-compatible torsion-free connection W has all the algebraic symmetries of Rm. Away from dimension 2, the Ricci contraction of W vanishes for every smooth connection: the Schouten tensor is defined precisely so that P ⊙ g carries all of the Ricci curvature. In particular a space of constant curvature has vanishing Weyl tensor.

Main declarations

• CovariantDerivative.weylTensor: the Weyl curvature tensor.
• CovariantDerivative.IsMetricCompatible.weylTensor_swap_pairs and CovariantDerivative.IsMetricCompatible.weylTensor_cyclic_eq_zero: pair interchange and the first Bianchi identity.
• CovariantDerivative.sum_weylTensor_eq_zero: the Weyl tensor is trace-free.
• CovariantDerivative.weylTensor_eq_zero_of_curvatureTensor_eq_zero: a flat point has vanishing Weyl tensor.
• CovariantDerivative.curvatureTensor_eq_zero_iff_weylTensor_eq_zero_and_schoutenTensor_eq_zero: the curvature tensor vanishes exactly where the Weyl and Schouten tensors both do.
• CovariantDerivative.weylTensor_eq_zero_of_finrank_le_one: the Weyl tensor vanishes in dimension at most 1.
• CovariantDerivative.weylTensor_eq_zero_of_curvatureTensor_eq_smul_inner_sub: constant curvature implies vanishing Weyl tensor.
• CovariantDerivative.IsMetricCompatible.weylTensor_eq_zero_of_finrank_eq_three: the Weyl tensor vanishes in dimension 3.
• IsMetricCompatible.riemannCurvatureTensor_eq_kulkarniNomizu_of_finrank_eq_three: hence Rm = P ⊙ g in dimension 3.

References

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

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

The Weyl curvature tensor W = Rm - P ⊙ g, where Rm is the metric-lowered Riemann curvature tensor, P the Schouten tensor and ⊙ the Kulkarni–Nomizu product.

@[simp]

theorem CovariantDerivative.weylTensor_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) (u v w z : TangentSpace I x) : ((((cov.weylTensor x) u) v) w) z = ((((cov.riemannCurvatureTensor x) u) v) w) z - (((((LinearMap.BilinForm.kulkarniNomizu (cov.schoutenTensor x)) (innerₗ (TangentSpace I x))) u) v) w) z

Evaluation of the Weyl curvature tensor.

theorem CovariantDerivative.weylTensor_antisymm_first {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) (u v w z : TangentSpace I x) : ((((cov.weylTensor x) u) v) w) z = -((((cov.weylTensor x) v) u) w) z

The Weyl tensor is antisymmetric in its first pair of arguments.

theorem CovariantDerivative.sum_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 ↑⊤] {ι : Type u_4} [Fintype ι] (x : M) (hn : Module.finrank ℝ (TangentSpace I x) ≠ 2) (b : OrthonormalBasis ι ℝ (TangentSpace I x)) (u v : TangentSpace I x) : ∑ j : ι, ((((cov.weylTensor x) (b j)) u) v) (b j) = 0

Away from dimension 2, the Weyl tensor is trace-free: in an orthonormal basis, contracting its first and fourth arguments gives zero.

theorem CovariantDerivative.weylTensor_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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] (x : M) (h : cov.curvatureTensor x = 0) : cov.weylTensor x = 0

A point with zero curvature tensor has zero Weyl tensor, in every dimension.

theorem CovariantDerivative.curvatureTensor_eq_zero_iff_weylTensor_eq_zero_and_schoutenTensor_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 ↑⊤] (x : M) : cov.curvatureTensor x = 0 ↔ cov.weylTensor x = 0 ∧ cov.schoutenTensor x = 0

The curvature tensor vanishes at a point exactly when both the Weyl tensor and the Schouten tensor vanish there, since Rm = W + P ⊙ g. This holds in every dimension.

theorem CovariantDerivative.weylTensor_eq_zero_of_finrank_le_one {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) (hdim : Module.finrank ℝ (TangentSpace I x) ≤ 1) : cov.weylTensor x = 0

On a base of tangent dimension at most one, the Weyl tensor of every smooth connection vanishes.

theorem CovariantDerivative.weylTensor_eq_zero_of_curvatureTensor_eq_smul_inner_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 ↑⊤] (x : M) (k : ℝ) (hn : Module.finrank ℝ (TangentSpace I x) ≠ 2) (h : ∀ (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = k • (inner ℝ u v • w - inner ℝ w v • u)) : cov.weylTensor x = 0

A space of constant curvature R(w,u)v = κ (⟨u,v⟩ w - ⟨w,v⟩ u) has vanishing Weyl tensor, away from dimension 2.

theorem CovariantDerivative.IsMetricCompatible.weylTensor_antisymm_last {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 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (x : M) (u v w z : TangentSpace I x) : ((((cov.weylTensor x) u) v) w) z = -((((cov.weylTensor x) u) v) z) w

For a metric-compatible connection, the Weyl tensor is antisymmetric in its last pair of arguments.

theorem CovariantDerivative.IsMetricCompatible.weylTensor_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] [Bundle.RiemannianBundle (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (u v w z : TangentSpace I x) : ((((cov.weylTensor x) u) v) w) z + ((((cov.weylTensor x) v) w) u) z + ((((cov.weylTensor x) w) u) v) z = 0

For a metric-compatible torsion-free connection, the cyclic sum of the first three arguments of the Weyl tensor vanishes.

theorem CovariantDerivative.IsMetricCompatible.weylTensor_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 (TangentSpace I)] (cov : CovariantDerivative I E (TangentSpace I)) [cov.ContMDiffCovariantDerivative ↑⊤] [IsContMDiffRiemannianBundle I 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (u v w z : TangentSpace I x) : ((((cov.weylTensor x) u) v) w) z = ((((cov.weylTensor x) w) z) u) v

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

theorem CovariantDerivative.IsMetricCompatible.weylTensor_eq_zero_of_finrank_eq_three {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 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (x : M) (hn : Module.finrank ℝ (TangentSpace I x) = 3) : cov.weylTensor x = 0

In dimension 3, the Weyl tensor of a metric-compatible connection vanishes.

theorem CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_kulkarniNomizu_of_finrank_eq_three {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 2 E (TangentSpace I)] (hcov : cov.IsMetricCompatible) (x : M) (hn : Module.finrank ℝ (TangentSpace I x) = 3) (u v w z : TangentSpace I x) : ((((cov.riemannCurvatureTensor x) u) v) w) z = (((((LinearMap.BilinForm.kulkarniNomizu (cov.schoutenTensor x)) (innerₗ (TangentSpace I x))) u) v) w) z

In dimension 3, the curvature tensor of a metric-compatible connection is the Kulkarni–Nomizu product Rm = P ⊙ g of its Schouten tensor with the metric, so it is determined by the Ricci curvature.