Sphere theorem

DefinitionRiemann curvature of a covariant derivative#✓fully proved

Let \(\nabla\) be a covariant derivative on the tangent bundle of a smooth manifold \(M\). For vector fields \(X, Y, Z\) on \(M\), the curvature of \(\nabla\) is the vector field \(R(X,Y)Z = \nabla_X \nabla_Y Z - \nabla_Y \nabla_X Z - \nabla_{[X,Y]} Z\), where \([X,Y]\) is the Lie bracket of \(X\) and \(Y\).

noncomputable def curv (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    (X Y Z : Π x : M, TangentSpace I x) : Π x : M, TangentSpace I x :=
  fun x =>
    cov (fun y => cov Z y (Y y)) x (X x)
      - cov (fun y => cov Z y (X y)) x (Y x)
      - cov Z x (mlieBracket I X Y x)

Used by 1

Used byStrictly quarter-pinched curvature

DefinitionStrictly quarter-pinched curvature#✓fully proved

Let \(\nabla\) be a covariant derivative on the tangent bundle of a Riemannian manifold \(M\), with curvature \(R\). Then \(\nabla\) is strictly quarter-pinched when, for all smooth vector fields \(X, Y\) on \(M\) and every point \(x \in M\) at which \(X(x)\) and \(Y(x)\) are orthonormal, the sectional curvature \(K = \langle R(X,Y)Y(x), X(x) \rangle\) satisfies \(1 < K \le 4\). The interval \((1, 4]\) is Knill's normalization of strict quarter pinching.

def QuarterPinched
    (cov : CovariantDerivative I E (TangentSpace I (M := M))) : Prop :=
  ∀ (X Y : Π x : M, TangentSpace I x),
    CMDiff ∞ (T% X) → CMDiff ∞ (T% Y) →
    ∀ x : M,
      inner ℝ (X x) (X x) = (1 : ℝ) → inner ℝ (Y x) (Y x) = (1 : ℝ) →
      inner ℝ (X x) (Y x) = (0 : ℝ) →
      (1 : ℝ) < inner ℝ (curv cov X Y Y x) (X x) ∧
        inner ℝ (curv cov X Y Y x) (X x) ≤ (4 : ℝ)

Uses 1 · Used by 2

Statement usesRiemann curvature of a covariant derivative

Used byDifferentiable sphere theorem · Topological sphere theorem

TheoremTopological sphere theorem#●ready to prove

Let \(M\) be a compact, Hausdorff, simply connected smooth manifold without boundary, of dimension \(d \ge 2\), with a smooth Riemannian metric. Suppose \(M\) carries a smooth covariant derivative \(\nabla\) on its tangent bundle that is torsion-free, compatible with the metric and strictly quarter-pinched (every sectional curvature at an orthonormal pair lies in \((1, 4]\)). Then \(M\) is homeomorphic to the unit sphere \(S^d \subset \mathbb{R}^{d+1}\).

public theorem_wanted sphere_theorem
    [I.Boundaryless] [T2Space M] [CompactSpace M] [SimplyConnectedSpace M]
    (hdim : 2 ≤ Module.finrank ℝ E)
    (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    [ContMDiffCovariantDerivative cov ∞]
    (_htor : cov.torsion = 0) (_hmet : IsMetricCompatible cov)
    (_hpinch : QuarterPinched cov) :
    Nonempty
      (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1)

Sources

• M. Berger; W. Klingenberg; H. E. Rauch (topological sphere theorem, 1951–1961). Knill, Some fundamental theorems in mathematics, §121. Problem sphere_theorem_topological of the lean-eval benchmark.

Uses 2

Statement usesMetric-compatible covariant derivative · Strictly quarter-pinched curvature

TheoremDifferentiable sphere theorem#●ready to prove

Let \(M\) be a compact, Hausdorff, simply connected smooth manifold without boundary, of dimension \(d \ge 2\), with a smooth Riemannian metric. Suppose \(M\) carries a smooth covariant derivative \(\nabla\) on its tangent bundle that is torsion-free, compatible with the metric and strictly quarter-pinched (every sectional curvature at an orthonormal pair lies in \((1, 4]\)). Then \(M\) is diffeomorphic to the unit sphere \(S^d \subset \mathbb{R}^{d+1}\) with its standard smooth structure.

public theorem_wanted differentiable_sphere_theorem
    [I.Boundaryless] [T2Space M] [CompactSpace M] [SimplyConnectedSpace M]
    (hdim : 2 ≤ Module.finrank ℝ E)
    (cov : CovariantDerivative I E (TangentSpace I (M := M)))
    [ContMDiffCovariantDerivative cov ∞]
    (_htor : cov.torsion = 0) (_hmet : IsMetricCompatible cov)
    (_hpinch : QuarterPinched cov) :
    Nonempty
      (M ≃ₘ⟮I, 𝓡 (Module.finrank ℝ E)⟯
        (sphere (0 : EuclideanSpace ℝ (Fin (Module.finrank ℝ E + 1))) 1))

Sources

• S. Brendle & R. Schoen, Manifolds with 1/4-pinched curvature are space forms, J. AMS 22 (2009). Knill, Some fundamental theorems in mathematics, §121. Problem sphere_theorem_differentiable of the lean-eval benchmark.

Uses 2

Statement usesMetric-compatible covariant derivative · Strictly quarter-pinched curvature

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.