Sectional curvature

For a metric-compatible connection, the sectional curvature of the tangent plane spanned by linearly independent vectors u, v is

<R(u, v)v, u> / det(Gram(u, v)).

This file defines that quotient for a smooth metric-compatible connection on a Riemannian tangent bundle and packages the pointwise and global constant-sectional-curvature predicates. The quotient is defined for all pairs, as is conventional for an algebraic API; the geometric predicates quantify only over linearly independent pairs, where the Gram determinant is strictly positive. Metric compatibility supplies the curvature symmetries that make the quotient independent of the chosen basis of the tangent plane; no torsion-free hypothesis is needed.

The constant-curvature tensor R(w, u)v = κ * (<u, v> * w - <w, v> * u) has sectional curvature κ, fixing the sign convention and providing the form used to state constant negative curvature.

The definition and convention follow J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 8, pp. 250–254 (Proposition 8.36). The curvature convention is R(X,Y)Z = ∇_X ∇_Y Z - ∇_Y ∇_X Z - ∇_[X,Y] Z.

Main definitions

• CovariantDerivative.sectionalCurvature: sectional curvature evaluated on two spanning vectors.
• CovariantDerivative.HasSectionalCurvatureAt: every tangent two-plane at a point has a given sectional curvature.
• CovariantDerivative.HasConstantSectionalCurvature: every tangent two-plane at every point has the same sectional curvature.

Main results

• CovariantDerivative.hasSectionalCurvatureAt_of_finrank_le_one and CovariantDerivative.HasSectionalCurvatureAt.eq_of_one_lt_finrank: in dimension at most one every k is a sectional curvature, since there are no tangent two-planes; from dimension two on the sectional curvature at a point is unique.
• CovariantDerivative.forall_sectionalCurvature_le_fixed_iff and CovariantDerivative.forall_le_sectionalCurvature_fixed_iff: an upper or lower sectional bound on the two-planes containing a fixed vector is equivalent to the corresponding bound on all curvature numerators with that vector in the second slot, the interface for radial curvature bounds.

noncomputable def CovariantDerivative.sectionalCurvature {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) (u v : TangentSpace I x) : ℝ

The sectional curvature evaluated on the tangent vectors u and v: <R(u,v)v,u> / det(Gram(u,v)).

Its geometric use is on linearly independent vectors. Defining the quotient on all pairs makes it an ordinary real-valued function; the constant-curvature predicates below impose linear independence explicitly.

@[simp]

theorem CovariantDerivative.sectionalCurvature_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 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) (u v : TangentSpace I x) : cov.sectionalCurvature hcov x u v = inner ℝ ((((cov.curvatureTensor x) u) v) v) u / (Matrix.gram ℝ ![u, v]).det

The defining quotient for sectional curvature.

theorem CovariantDerivative.sectionalCurvature_eq_of_orthonormal {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) (u v : TangentSpace I x) (h : Orthonormal ℝ ![u, v]) : cov.sectionalCurvature hcov x u v = inner ℝ ((((cov.curvatureTensor x) u) v) v) u

On an orthonormal pair, sectional curvature is just <R(u,v)v,u>.

theorem CovariantDerivative.sectionalCurvature_smul_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) (u v : TangentSpace I x) (a b : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) : cov.sectionalCurvature hcov x (a • u) (b • v) = cov.sectionalCurvature hcov x u v

Rescaling either spanning vector by a nonzero scalar does not change sectional curvature.

theorem CovariantDerivative.sectionalCurvature_add_smul_right {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) (u v : TangentSpace I x) (a : ℝ) : cov.sectionalCurvature hcov x u (v + a • u) = cov.sectionalCurvature hcov x u v

Adding a multiple of the first spanning vector to the second does not change sectional curvature.

theorem CovariantDerivative.IsMetricCompatible.sectionalCurvature_comm {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) (u v : TangentSpace I x) : cov.sectionalCurvature hcov x u v = cov.sectionalCurvature hcov x v u

For a metric-compatible connection, sectional curvature is symmetric in its two spanning vectors.

theorem CovariantDerivative.forall_sectionalCurvature_le_iff {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) (κ : ℝ) : (∀ (u v : TangentSpace I x), LinearIndependent ℝ ![u, v] → cov.sectionalCurvature hcov x u v ≤ κ) ↔ ∀ (u v : TangentSpace I x), inner ℝ ((((cov.curvatureTensor x) u) v) v) u ≤ κ * (Matrix.gram ℝ ![u, v]).det

An upper sectional-curvature bound is equivalent to the corresponding bound on every curvature numerator, including dependent pairs. The latter have zero numerator and Gram determinant, so no dimension or nonzero-vector hypothesis is needed.

theorem CovariantDerivative.forall_sectionalCurvature_le_fixed_iff {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) (v : TangentSpace I x) (κ : ℝ) : (∀ (u : TangentSpace I x), LinearIndependent ℝ ![u, v] → cov.sectionalCurvature hcov x u v ≤ κ) ↔ ∀ (u : TangentSpace I x), inner ℝ ((((cov.curvatureTensor x) u) v) v) u ≤ κ * (Matrix.gram ℝ ![u, v]).det

An upper sectional bound on planes through a fixed vector bounds every curvature numerator.

theorem CovariantDerivative.forall_le_sectionalCurvature_fixed_iff {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) (v : TangentSpace I x) (κ : ℝ) : (∀ (u : TangentSpace I x), LinearIndependent ℝ ![u, v] → κ ≤ cov.sectionalCurvature hcov x u v) ↔ ∀ (u : TangentSpace I x), κ * (Matrix.gram ℝ ![u, v]).det ≤ inner ℝ ((((cov.curvatureTensor x) u) v) v) u

A lower sectional bound on planes through a fixed vector bounds every curvature numerator.

def CovariantDerivative.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 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) (k : ℝ) : Prop

A connection has sectional curvature k at x when every tangent two-plane at x has sectional curvature k.

theorem CovariantDerivative.hasSectionalCurvatureAt_iff {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) (k : ℝ) : cov.HasSectionalCurvatureAt hcov x k ↔ ∀ (u v : TangentSpace I x), LinearIndependent ℝ ![u, v] → cov.sectionalCurvature hcov x u v = k

The pointwise characterization of having prescribed sectional curvature.

theorem CovariantDerivative.HasSectionalCurvatureAt.sectionalCurvature_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} {k : ℝ} (h : cov.HasSectionalCurvatureAt hcov x k) (u v : TangentSpace I x) (huv : LinearIndependent ℝ ![u, v]) : cov.sectionalCurvature hcov x u v = k

Evaluate the prescribed sectional curvature of a linearly independent tangent pair.

theorem CovariantDerivative.hasSectionalCurvatureAt_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 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) (k : ℝ) (hn : Module.finrank ℝ (TangentSpace I x) ≤ 1) : cov.HasSectionalCurvatureAt hcov x k

In dimension at most one there are no tangent two-planes, so every k is the sectional curvature at every point.

theorem CovariantDerivative.HasSectionalCurvatureAt.eq_of_one_lt_finrank {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} {k k' : ℝ} (h : cov.HasSectionalCurvatureAt hcov x k) (h' : cov.HasSectionalCurvatureAt hcov x k') (hn : 1 < Module.finrank ℝ (TangentSpace I x)) : k = k'

In dimension at least two the tangent two-planes at a point determine their common sectional curvature.

def CovariantDerivative.HasConstantSectionalCurvature {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) (k : ℝ) : Prop

A connection has constant sectional curvature k when it has sectional curvature k at every point.

theorem CovariantDerivative.hasConstantSectionalCurvature_iff {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) (k : ℝ) : cov.HasConstantSectionalCurvature hcov k ↔ ∀ (x : M), cov.HasSectionalCurvatureAt hcov x k

The pointwise characterization of constant sectional curvature.

theorem CovariantDerivative.HasConstantSectionalCurvature.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 2 E fun (x : M) => TangentSpace I x] {cov : CovariantDerivative I E fun (x : M) => TangentSpace I x} [cov.ContMDiffCovariantDerivative ↑⊤] {hcov : cov.IsMetricCompatible} {k : ℝ} (h : cov.HasConstantSectionalCurvature hcov k) (x : M) : cov.HasSectionalCurvatureAt hcov x k

Constant sectional curvature specializes to the prescribed curvature at each point.

theorem CovariantDerivative.hasSectionalCurvatureAt_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 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) (k : ℝ) (h : ∀ (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = k • (inner ℝ u v • w - inner ℝ w v • u)) : cov.HasSectionalCurvatureAt hcov x k

The algebraic constant-curvature tensor with parameter k has sectional curvature k on every tangent two-plane at the point.

theorem CovariantDerivative.hasConstantSectionalCurvature_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 2 E fun (x : M) => TangentSpace I x] (cov : CovariantDerivative I E fun (x : M) => TangentSpace I x) [cov.ContMDiffCovariantDerivative ↑⊤] (hcov : cov.IsMetricCompatible) (k : ℝ) (h : ∀ (x : M) (w u v : TangentSpace I x), (((cov.curvatureTensor x) w) u) v = k • (inner ℝ u v • w - inner ℝ w v • u)) : cov.HasConstantSectionalCurvature hcov k

If the curvature tensor has the constant-curvature form with the same parameter at every point, then the connection has constant sectional curvature with that parameter.

theorem CovariantDerivative.hasConstantSectionalCurvature_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 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) (h : ∀ (x : M), cov.curvatureTensor x = 0) : cov.HasConstantSectionalCurvature hcov 0

A connection whose curvature tensor vanishes everywhere has constant sectional curvature zero.