4D topological Poincaré conjecture (Freedman)
poincare_4d_topological
Submitter: Kim Morrison.
Notes: Every Hausdorff 4-manifold homotopy-equivalent to 𝕊⁴ is homeomorphic to 𝕊⁴. Specialization to n = 4 of mathlib's generalized `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Michael Freedman's 1982 theorem (J. Differential Geom. 17), Fields Medal 1986. Proof uses Casson handles and the Bing-topology infinite-process construction. The corresponding smooth 4D Poincaré conjecture (every smooth homotopy 4-sphere is diffeomorphic to S⁴) remains famously OPEN and is not included here. Mathlib has the homotopy-equiv / homeo / ChartedSpace scaffolding but no Casson handles or Freedman's theorem.
Source: M. H. Freedman, The topology of four-dimensional manifolds, J. Differential Geom. 17 (1982), 357-453. Specialization of `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in Mathlib/Geometry/Manifold/PoincareConjecture.lean.
Informal solution: Freedman's main theorem: every topological 4-manifold homotopy equivalent to a topological model is homeomorphic to it, provided one can construct topological Casson handles. The construction of Casson handles is via a Bing-style limiting process (countably many handle additions, infinite tower of 2-handles) that produces a topological — but not smooth — 4-ball. Applying this to a homotopy 4-sphere M, one writes M as the union of two 2-handlebodies along their boundary, replaces handles with Casson handles, and assembles a homeomorphism to S⁴. The smooth analogue is open because Casson handles need not be smoothly standard (Donaldson's invariants distinguish smooth structures in dim 4).
theorem declaration uses `sorry`poincare_4d_topological {M : Type*} [TopologicalSpace M] [T2Space M]
[ChartedSpace (EuclideanSpace ℝ (Fin 4)) M]
(_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) :
Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin 5)) 1) := M:Type u_1inst✝²:TopologicalSpace Minst✝¹:T2Space Minst✝:ChartedSpace (EuclideanSpace ℝ (Fin 4)) M_h:M ≃ₕ ↑(sphere 0 1)⊢ Nonempty (M ≃ₜ ↑(sphere 0 1))
All goals completed! 🐙Solved by
Not yet solved.