A closed simply connected 3-manifold is a homotopy 3-sphere

Open

PoincareFormalization.homotopyEquiv_sphere_three

by korbonits · 1 vote · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologymathlibpoincare-conjecturetopology

Let $M$ be a compact, Hausdorff, simply connected topological $3$ -manifold without boundary, modelled on Euclidean $3$ -space (a charted space over $\mathbb{R}^3 =$ EuclideanSpace ℝ (Fin 3)). Then $M$ is homotopy equivalent to the standard $3$ -sphere:

M \simeq_h \mathbb{S}^3 = \{\, x \in \mathbb{R}^4 : \lVert x\rVert = 1 \,\}.

This is the classical, purely homotopy-theoretic half of the three-dimensional Poincaré conjecture; it does not use geometrization or Ricci flow. A simply connected closed $3$ -manifold is orientable, so Poincaré duality forces its homology to coincide with that of $S^3$ , namely $H_0 = H_3 = \mathbb{Z}$ and $H_1 = H_2 = 0$ . The Hurewicz theorem then gives $\pi_3(M) \cong H_3(M) \cong \mathbb{Z}$ , and a generator is represented by a map $f : S^3 \to M$ that induces isomorphisms on all homology groups. Since both $M$ and $S^3$ are simply connected CW complexes, Whitehead's theorem promotes $f$ to a homotopy equivalence.

As a milestone this is the "easy" input to the topological Poincaré conjecture: combined with the statement that every homotopy $3$ -sphere is homeomorphic to $S^3$ , it yields that a compact simply connected $3$ -manifold is homeomorphic to $S^3$ .

Formalization Note The sphere $\mathbb{S}^3$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin (3 + 1))) 1 with the subspace topology, and $\simeq_h$ is Mathlib's ContinuousMap.HomotopyEquiv (notation ≃ₕ, scoped in the ContinuousMap namespace). No second-countability assumption is imposed, matching the parent statement PoincareFormalization.nonempty_homeomorph_sphere_three.

Preamble

import Mathlib.Geometry.Manifold.ChartedSpace
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
import Mathlib.Topology.Homotopy.Equiv
open scoped ContinuousMap

Formal statement

namespace PoincareFormalization

theorem homotopyEquiv_sphere_three (M : Type*) [TopologicalSpace M]
    [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]
    [SimplyConnectedSpace M] [CompactSpace M] :
    Nonempty (M ≃ₕ ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (3 + 1))) 1)) := by
  sorry

end PoincareFormalization

Source

Mathlib proof_wanted SimplyConnectedSpace.nonempty_homeomorph_sphere_three, Geometry/Manifold/PoincareConjecture.lean, rev 0df444a (author Junyan Xu). Mathematical reference: J. Milnor, The Poincaré Conjecture, Clay Mathematics Institute, Section 1, p. 1, https://www.claymath.org/wp-content/uploads/2022/06/poincare.pdf . Homotopy-theoretic ingredients: A. Hatcher, Algebraic Topology (2002): Poincaré duality (Theorem 3.30), Hurewicz theorem (Theorem 4.32), Whitehead theorem (Theorem 4.5).

View graph