The Schouten tensor of a smooth connection

On a Riemannian manifold of dimension n, the Schouten tensor is the bilinear form

P = (Ric - Scal g / (2 (n - 1))) / (n - 2).

It is the trace-adjusted Ricci tensor for which Ric = (n - 2) P + (tr_g P) g, and it is the part of the curvature that the Weyl tensor leaves out: Rm = W + P ⊙ g. Under a conformal change of metric it transforms by the Hessian of the conformal factor, which is why it governs conformal geometry and the Yamabe problem.

As for CovariantDerivative.ricciTensor and CovariantDerivative.scalarCurvature, the definition is made for any smooth connection on a Riemannian tangent bundle; symmetry of P needs a metric-compatible torsion-free connection. The formulas involving n - 2 assume n ≠ 2, the dimensions in which the Schouten tensor is defined; in dimension 2 the definition divides by zero and returns 0.

Main declarations

• CovariantDerivative.schoutenTensor: the Schouten tensor.
• CovariantDerivative.bilinFormTrace_schoutenTensor: tr_g P = Scal / (2 (n - 1)).
• CovariantDerivative.ricciTensor_eq_smul_schoutenTensor_add: Ric = (n - 2) P + (tr_g P) g.
• CovariantDerivative.schoutenTensor_eq_of_curvatureTensor_eq_smul_inner_sub: constant curvature κ gives P = (κ / 2) g.
• CovariantDerivative.schoutenTensor_eq_zero_of_curvatureTensor_eq_zero: zero curvature gives P = 0.
• CovariantDerivative.mdifferentiableAt_schoutenTensor_apply: for a smooth metric, P pairs differentiable vector fields to differentiable functions.

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.schoutenTensor {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 →ₗ[ℝ] ℝ

The Schouten tensor P = (Ric - Scal g / (2 (n - 1))) / (n - 2) of a smooth connection on a Riemannian tangent bundle of real dimension n.

@[simp]

theorem CovariantDerivative.schoutenTensor_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 : TangentSpace I x) : ((cov.schoutenTensor x) u) v = (↑(Module.finrank ℝ (TangentSpace I x)) - 2)⁻¹ * (((cov.ricciTensor x) u) v - cov.scalarCurvature x / (2 * (↑(Module.finrank ℝ (TangentSpace I x)) - 1)) * inner ℝ u v)

Evaluation of the Schouten tensor.

theorem CovariantDerivative.bilinFormTrace_schoutenTensor {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) (hn : Module.finrank ℝ (TangentSpace I x) ≠ 2) : TauCeti.bilinFormTrace (cov.schoutenTensor x) = cov.scalarCurvature x / (2 * (↑(Module.finrank ℝ (TangentSpace I x)) - 1))

The metric trace of the Schouten tensor is Scal / (2 (n - 1)), away from dimension 2.

theorem CovariantDerivative.ricciTensor_eq_smul_schoutenTensor_add {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) (hn : Module.finrank ℝ (TangentSpace I x) ≠ 2) : cov.ricciTensor x = (↑(Module.finrank ℝ (TangentSpace I x)) - 2) • cov.schoutenTensor x + TauCeti.bilinFormTrace (cov.schoutenTensor x) • innerₗ (TangentSpace I x)

Away from dimension 2, Ricci curvature decomposes as Ric = (n - 2) P + (tr_g P) g in terms of the Schouten tensor P.

theorem CovariantDerivative.IsMetricCompatible.schoutenTensor_isSymm {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) : (cov.schoutenTensor x).IsSymm

The Schouten tensor of a metric-compatible torsion-free connection is a symmetric bilinear form.

theorem CovariantDerivative.schoutenTensor_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.schoutenTensor x = 0

A point with zero curvature tensor has zero Schouten tensor.

theorem CovariantDerivative.schoutenTensor_eq_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 : 3 ≤ Module.finrank ℝ (TangentSpace I x)) (h : ∀ (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = k • (inner ℝ u v • w - inner ℝ w v • u)) : cov.schoutenTensor x = (k / 2) • innerₗ (TangentSpace I x)

The Schouten tensor of the constant-curvature model R(w,u)v = κ (⟨u,v⟩ w - ⟨w,v⟩ u) is (κ / 2) g, in dimension at least 3.

theorem CovariantDerivative.mdifferentiableAt_schoutenTensor_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 ↑⊤] [IsContMDiffRiemannianBundle I (↑⊤) E (TangentSpace I)] {σ τ : (x : M) → TangentSpace I x} {x : M} (hσ : (MDiffAt fun (x : M) => ⟨x, σ x⟩) x) (hτ : (MDiffAt fun (x : M) => ⟨x, τ x⟩) x) : (MDiffAt fun (y : M) => ((cov.schoutenTensor y) (σ y)) (τ y)) x

For a smooth metric, the Schouten tensor of a smooth connection pairs two vector fields differentiable at x to a function differentiable at x.

theorem CovariantDerivative.contMDiffAt_schoutenTensor_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 ↑⊤] [IsContMDiffRiemannianBundle I (↑⊤) E (TangentSpace I)] {σ τ : (x : M) → TangentSpace I x} {x : M} (hσ : ContMDiffAt I I.tangent (↑⊤) (fun (x : M) => ⟨x, σ x⟩) x) (hτ : ContMDiffAt I I.tangent (↑⊤) (fun (x : M) => ⟨x, τ x⟩) x) : ContMDiffAt I (modelWithCornersSelf ℝ ℝ) (↑⊤) (fun (y : M) => ((cov.schoutenTensor y) (σ y)) (τ y)) x

For a smooth metric, the Schouten tensor of a smooth connection pairs two vector fields that are C^∞ at x to a function that is C^∞ at x.