Schur's theorem

Let ∇ be a smooth metric-compatible torsion-free connection on the tangent bundle of a Riemannian manifold M of dimension n ≥ 3, such as its Levi-Civita connection. Suppose that at every point x all tangent two-planes have the same sectional curvature κ x, so that the curvature tensor is R(w, u)v = κ(x) (⟨u, v⟩ w - ⟨w, v⟩ u). Schur's theorem states that the function κ is then locally constant, hence constant when M is connected.

The tensor (Y, Z, σ) ↦ ⟨Z, σ⟩ Y - ⟨Y, σ⟩ Z is parallel for a metric connection, so the covariant derivative of the curvature is (∇_X R)(Y, Z)σ = dκ(X) (⟨Z, σ⟩ Y - ⟨Y, σ⟩ Z). Inserting this into the second Bianchi identity and evaluating on three orthonormal vectors kills dκ; this is where n ≥ 3 is used. In dimension two every tangent space has a single two-plane, so the curvature is pointwise isotropic for every metric, and the conclusion fails for any surface whose Gaussian curvature is not constant.

Main results

• CovariantDerivative.IsMetricCompatible.covariantDerivative_curvatureOperator_eq_mvfderiv_smul: the covariant derivative at x of a curvature tensor of pointwise constant-curvature form near x.
• CovariantDerivative.mfderiv_eq_zero_of_curvatureTensor_eq_smul_inner_sub: the local form of Schur's theorem, dκ(x) = 0 in dimension at least three when the curvature has constant-curvature form near x.
• CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt and CovariantDerivative.hasConstantSectionalCurvature_of_forall_hasSectionalCurvatureAt: Schur's theorem on a preconnected manifold.

References

• S. Kobayashi and K. Nomizu, Foundations of Differential Geometry, Vol. I, Interscience (1963), Chapter V, Section 2 (Schur's theorem, proved from the second Bianchi identity).

theorem CovariantDerivative.IsMetricCompatible.covariantDerivative_curvatureOperator_eq_mvfderiv_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 (↑⊤) E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) {κ : M → ℝ} {x : M} (hκ : ∀ᶠ (y : M) in nhds x, ∀ (w u v : TangentSpace I y), (((cov.curvatureTensor y) w) u) v = κ y • (inner ℝ u v • w - inner ℝ w v • u)) {X Y Z σ : (x : M) → TangentSpace I x} (hX : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, X x⟩) (hY : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Y x⟩) (hZ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, Z x⟩) (hσ : ContMDiff I I.tangent ↑⊤ fun (x : M) => ⟨x, σ x⟩) (hκx : MDiffAt κ x) : (↑cov (cov.curvatureOperator Y Z σ) x) (X x) - cov.curvatureOperator (fun (y : M) => (↑cov Y y) (X y)) Z σ x - cov.curvatureOperator Y (fun (y : M) => (↑cov Z y) (X y)) σ x - cov.curvatureOperator Y Z (fun (y : M) => (↑cov σ y) (X y)) x = (d% κ x) (X x) • (inner ℝ (Z x) (σ x) • Y x - inner ℝ (Y x) (σ x) • Z x)

Let the curvature tensor of a metric-compatible connection have the pointwise constant-curvature form R(w, u)v = κ(y) (⟨u, v⟩ w - ⟨w, v⟩ u) at every point y near x, and let κ be differentiable at x. The covariant derivative of the curvature along X at x, (∇_X R)(Y, Z)σ = ∇_X (R(Y, Z)σ) - R(∇_X Y, Z)σ - R(Y, ∇_X Z)σ - R(Y, Z)(∇_X σ), is then dκ(X) (⟨Z, σ⟩ Y - ⟨Y, σ⟩ Z).

theorem CovariantDerivative.mfderiv_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 fun (x : M) => TangentSpace I x] [IsContMDiffRiemannianBundle I (↑⊤) 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) (hdim : 3 ≤ Module.finrank ℝ E) {κ : M → ℝ} {x : M} (hκ : ∀ᶠ (y : M) in nhds x, ∀ (w u v : TangentSpace I y), (((cov.curvatureTensor y) w) u) v = κ y • (inner ℝ u v • w - inner ℝ w v • u)) : mfderiv% κ x = 0

Schur's theorem, local form. Let a metric-compatible torsion-free connection have curvature tensor of the pointwise constant-curvature form R(w, u)v = κ(y) (⟨u, v⟩ w - ⟨w, v⟩ u) at every point y near x, in dimension at least three. Then dκ vanishes at x. No differentiability of κ is assumed: near x, κ is the smooth scalar curvature divided by n (n - 1).

theorem CovariantDerivative.eq_of_forall_hasSectionalCurvatureAt {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 (↑⊤) E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] [PreconnectedSpace M] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (hdim : 3 ≤ Module.finrank ℝ E) {κ : M → ℝ} (hκ : ∀ (x : M), cov.HasSectionalCurvatureAt hcov x (κ x)) (x y : M) : κ x = κ y

Schur's theorem. Let a metric-compatible torsion-free connection on a preconnected manifold of dimension at least three have, at every point x, the same sectional curvature κ x on all tangent two-planes at x. Then κ is constant.

theorem CovariantDerivative.hasConstantSectionalCurvature_of_forall_hasSectionalCurvatureAt {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 (↑⊤) E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] [PreconnectedSpace M] (hcov : cov.IsMetricCompatible) (ht : cov.torsion = 0) (hdim : 3 ≤ Module.finrank ℝ E) {κ : M → ℝ} (hκ : ∀ (x : M), cov.HasSectionalCurvatureAt hcov x (κ x)) (x₀ : M) : cov.HasConstantSectionalCurvature hcov (κ x₀)

Schur's theorem, global form. If a metric-compatible torsion-free connection on a preconnected manifold of dimension at least three has, at every point x, the same sectional curvature κ x on all tangent two-planes at x, then it has constant sectional curvature κ x₀ for any point x₀.