3D topological Poincaré conjecture (Perelman)

← All problems

poincare_3d_topological

Submitter: Kim Morrison.

Notes: Every simply connected compact Hausdorff 3-manifold is homeomorphic to 𝕊³. Recorded as `proof_wanted SimplyConnectedSpace.nonempty_homeomorph_sphere_three` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Proved by Perelman in 2002-2003 via Hamilton's Ricci flow with surgery; one of the seven Millennium Problems. Mathlib has ChartedSpace, SimplyConnectedSpace, CompactSpace, T2Space, Homeomorph and the unit sphere as a smooth manifold but no Ricci flow, no Hamilton-Perelman surgery, and no Poincaré conjecture itself.

Source: G. Perelman, The entropy formula for the Ricci flow and its geometric applications (arXiv:math/0211159, 2002); Ricci flow with surgery on three-manifolds (arXiv:math/0303109, 2003); Finite extinction time for the solutions to the Ricci flow on certain three-manifolds (arXiv:math/0307245, 2003). Recorded as a `proof_wanted` in Mathlib/Geometry/Manifold/PoincareConjecture.lean. Originally conjectured by Henri Poincaré in 1904.

Informal solution: Run Ricci flow ∂g/∂t = -2 Ric(g) on M with surgery to remove finite-time singularities (Hamilton's program, completed by Perelman). The flow simplifies the metric, and Perelman's monotonicity formulas (reduced volume, ℒ-functional, no local collapsing) together with the canonical-neighbourhood theorem control the geometry. In finite time the flow either becomes extinct (M is a connected sum of spherical space forms and S²×S¹s, in particular when π_1(M) = 1, M = S³) or decomposes M along incompressible 2-tori into pieces of one of Thurston's eight geometric types; the simply-connected hypothesis rules out the toroidal decomposition and the spherical-space-form ambiguity, leaving M ≃ S³.

theorem declaration uses `sorry`poincare_3d_topological {M : Type*} [TopologicalSpace M] [T2Space M] [ChartedSpace (EuclideanSpace (Fin 3)) M] [SimplyConnectedSpace M] [CompactSpace M] : Nonempty (M ≃ₜ sphere (0 : EuclideanSpace (Fin 4)) 1) := M:Type u_1inst✝⁴:TopologicalSpace Minst✝³:T2Space Minst✝²:ChartedSpace (EuclideanSpace (Fin 3)) Minst✝¹:SimplyConnectedSpace Minst✝:CompactSpace MNonempty (M ≃ₜ (sphere 0 1)) All goals completed! 🐙

Solved by

Not yet solved.