Sectional curvature determines the curvature tensor

For a metric-compatible torsion-free connection on a Riemannian tangent bundle, the metric-lowered curvature tensor Rm(u, v, w, z) = ⟨R(u, v)w, z⟩ is antisymmetric in each pair of arguments and satisfies the first Bianchi identity. By the polarization identity LinearMap.six_mul_apply_eq_of_cyclic_eq_zero it is therefore determined by the numerators ⟨R(u, v)v, u⟩ of the sectional curvatures, and in fact by their values on linearly independent pairs u, v, which are the pairs spanning a tangent two-plane (CovariantDerivative.IsMetricCompatible.riemannCurvatureTensor_eq_of_forall_linearIndependent).

In particular, the tangent two-planes at a point all have sectional curvature κ exactly when the curvature tensor there has the constant-curvature form

R(w, u)v = κ (⟨u, v⟩ w - ⟨w, v⟩ u).

So constant sectional curvature κ is equivalent to the constant-curvature tensor equation Bundle.RiemannianMetric.IsConstantCurvatureTensor, and it forces Ric = (n - 1) κ g and Scal = n (n - 1) κ in dimension n. In dimension at most one there are no tangent two-planes, so every κ is a sectional curvature (CovariantDerivative.hasSectionalCurvatureAt_of_finrank_le_one), and correspondingly the constant-curvature equation then holds for every κ. From dimension two on the sectional curvature at a point is unique (CovariantDerivative.HasSectionalCurvatureAt.eq_of_one_lt_finrank).

In dimension exactly two the tangent space is itself the only tangent two-plane, and its sectional curvature, the Gaussian curvature, is half the scalar curvature. So on a surface the scalar curvature alone determines the curvature tensor, R(w, u)v = (Scal / 2) (⟨u, v⟩ w - ⟨w, v⟩ u), and a metric has constant curvature κ exactly when its scalar curvature is the constant 2 κ. This is how the scalar-curvature equation of a conformal metric on a surface produces a metric of constant curvature.

Main results

• CovariantDerivative.hasSectionalCurvatureAt_iff_curvatureTensor_eq_smul_inner_sub: sectional curvature κ at a point is the constant-curvature form of the curvature tensor there.
• CovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor: the global version.
• CovariantDerivative.HasSectionalCurvatureAt.ricciTensor_eq and CovariantDerivative.HasSectionalCurvatureAt.scalarCurvature_eq: the Ricci and scalar curvature of a point of sectional curvature κ.
• CovariantDerivative.hasSectionalCurvatureAt_scalarCurvature_div_two: in dimension two the sectional curvature is half the scalar curvature.
• CovariantDerivative.exists_curvatureTensor_eq_smul_inner_sub_of_finrank_eq_two and CovariantDerivative.curvatureTensor_eq_scalarCurvature_div_two_smul: in dimension two a metric-compatible connection has curvature tensor R(w, u)v = (Scal / 2) (⟨u, v⟩ w - ⟨w, v⟩ u), with no torsion hypothesis.
• isConstantCurvatureTensor_iff_scalarCurvature_eq_of_finrank_eq_two, in the namespace Bundle.ContMDiffRiemannianMetric: a metric on a surface has constant curvature κ exactly when its scalar curvature is 2 κ.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 8, Propositions 8.31 and 8.36.

theorem CovariantDerivative.HasSectionalCurvatureAt.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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] {hcov : cov.IsMetricCompatible} {x : M} {κ : ℝ} (h : cov.HasSectionalCurvatureAt hcov x κ) (ht : cov.torsion = 0) (w u v : TangentSpace I x) : (((cov.curvatureTensor x) w) u) v = κ • (inner ℝ u v • w - inner ℝ w v • u)

At a point where every tangent two-plane has sectional curvature κ, the curvature tensor of a metric-compatible torsion-free connection has the constant-curvature form R(w, u)v = κ (⟨u, v⟩ w - ⟨w, v⟩ u).

theorem CovariantDerivative.HasSectionalCurvatureAt.curvatureTensor_apply_self_of_inner_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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] {hcov : cov.IsMetricCompatible} {x : M} {κ : ℝ} (h : cov.HasSectionalCurvatureAt hcov x κ) (ht : cov.torsion = 0) {w u : TangentSpace I x} (hwu : inner ℝ w u = 0) : (((cov.curvatureTensor x) w) u) u = (κ * ‖u‖ ^ 2) • w

At a point where every tangent two-plane has sectional curvature κ, the Jacobi operator w ↦ R(w, u)u of a metric-compatible torsion-free connection acts on the orthogonal complement of u as multiplication by κ ‖u‖².

theorem CovariantDerivative.hasSectionalCurvatureAt_iff_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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (x : M) (κ : ℝ) : cov.HasSectionalCurvatureAt hcov x κ ↔ ∀ (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = κ • (inner ℝ u v • w - inner ℝ w v • u)

For a metric-compatible torsion-free connection, every tangent two-plane at x has sectional curvature κ if and only if the curvature tensor at x has the constant-curvature form R(w, u)v = κ (⟨u, v⟩ w - ⟨w, v⟩ u).

theorem CovariantDerivative.hasConstantSectionalCurvature_iff_isConstantCurvatureTensor {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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (κ : ℝ) : cov.HasConstantSectionalCurvature hcov κ ↔ Bundle.RiemannianBundle.g.IsConstantCurvatureTensor cov ⋯ κ

A metric-compatible torsion-free connection has constant sectional curvature κ if and only if its curvature tensor is the constant-curvature tensor R(w, u)v = κ (⟨u, v⟩ w - ⟨w, v⟩ u) at every point. Applied to the Levi-Civita connection, this identifies constant sectional curvature of a Riemannian manifold with the constant-curvature equation.

theorem CovariantDerivative.HasSectionalCurvatureAt.ricciTensor_eq {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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] {hcov : cov.IsMetricCompatible} {x : M} {κ : ℝ} (h : cov.HasSectionalCurvatureAt hcov x κ) (ht : cov.torsion = 0) : cov.ricciTensor x = ((↑(Module.finrank ℝ (TangentSpace I x)) - 1) * κ) • innerₗ (TangentSpace I x)

At a point where every tangent two-plane has sectional curvature κ, the Ricci tensor of a metric-compatible torsion-free connection is (n - 1) κ g in dimension n.

theorem CovariantDerivative.HasSectionalCurvatureAt.scalarCurvature_eq {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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] {hcov : cov.IsMetricCompatible} {x : M} {κ : ℝ} (h : cov.HasSectionalCurvatureAt hcov x κ) : cov.scalarCurvature x = ↑(Module.finrank ℝ (TangentSpace I x)) * (↑(Module.finrank ℝ (TangentSpace I x)) - 1) * κ

At a point where every tangent two-plane has sectional curvature κ, the scalar curvature of a metric-compatible connection is n (n - 1) κ in dimension n.

theorem CovariantDerivative.exists_curvatureTensor_eq_smul_inner_sub_of_finrank_eq_two {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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) {x : M} (hx : Module.finrank ℝ (TangentSpace I x) = 2) : ∃ (K : ℝ), ∀ (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = K • (inner ℝ u v • w - inner ℝ w v • u)

In dimension two the curvature tensor of a metric-compatible connection has the constant-curvature form R(w, u)v = K (⟨u, v⟩ w - ⟨w, v⟩ u) for some real K, the Gaussian curvature. Neither torsion-freeness nor the Bianchi identity is needed: in an orthonormal basis, antisymmetry in the first two arguments and metric compatibility leave the single number ⟨R(e₀, e₁)e₁, e₀⟩.

theorem CovariantDerivative.curvatureTensor_eq_scalarCurvature_div_two_smul {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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) {x : M} (hx : Module.finrank ℝ (TangentSpace I x) = 2) (w u v : TangentSpace I x) : (((cov.curvatureTensor x) w) u) v = (cov.scalarCurvature x / 2) • (inner ℝ u v • w - inner ℝ w v • u)

The curvature tensor of a surface. In dimension two the curvature tensor of a metric-compatible connection is determined by the scalar curvature: R(w, u)v = (Scal / 2) (⟨u, v⟩ w - ⟨w, v⟩ u).

theorem CovariantDerivative.hasSectionalCurvatureAt_scalarCurvature_div_two {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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I 2 E fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) {x : M} (hx : Module.finrank ℝ (TangentSpace I x) = 2) : cov.HasSectionalCurvatureAt hcov x (cov.scalarCurvature x / 2)

The Gaussian curvature of a surface is half its scalar curvature. In dimension two the tangent space at x is the only tangent two-plane there, and for a metric-compatible connection its sectional curvature is Scal(x) / 2.

theorem Bundle.ContMDiffRiemannianMetric.isConstantCurvatureTensor_iff_scalarCurvature_eq_of_finrank_eq_two {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] [T2Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (hE : Module.finrank ℝ E = 2) (κ : ℝ) : g.IsConstantCurvatureTensor κ ↔ ∀ (x : M), g.scalarCurvature x = 2 * κ

Constant curvature on a surface. A smooth metric on a surface has constant curvature κ, in the tensor form R(w, u)v = κ (⟨u, v⟩ w - ⟨w, v⟩ u), exactly when its scalar curvature is the constant 2 κ. In particular it has constant curvature -1 exactly when its scalar curvature is -2.