Smooth Poincaré four-conjecture via local diffeomorphic homotopy equivalences

Proved

SP4Mission.spc4_iff_local_homotopy_equiv

by evgeth · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

covering-spacesdifferential-topologyfour-manifoldshomotopysmooth-poincare

Let $S^4$ be the standard unit sphere in Euclidean five-space. The sphere form of the smooth four-dimensional Poincare conjecture is equivalent to the following local-map statement: every compact Hausdorff smooth real four-manifold $M$ , with its given smooth atlas, that is homeomorphic to $S^4$ admits a homotopy equivalence $f:M \to S^4$ whose forward map is a smooth local diffeomorphism. In symbols,

\mathrm{SPC4} \iff \forall M\text{ as above},\quad M \cong_{\mathrm{top}} S^4 \Longrightarrow \exists f:M\simeq S^4,\quad f\text{ is a smooth local diffeomorphism}.

This is a supporting reformulation using standard covering-space theory. It retains the original atlas and isolates an existence problem for local smooth inverses. The existence of such maps for arbitrary smooth structures on a topological four-sphere remains unresolved.

Formalization Note The statement uses the exact platform definitions SPC4 and S4. It assumes neither Freedmans theorem nor the smooth Poincare conjecture.

Preamble

import Mathlib.Topology.Homotopy.Lifting
import Mathlib.Topology.Homotopy.Equiv
import Mathlib.Geometry.Manifold.LocalDiffeomorph
import Mathlib.Geometry.Manifold.Instances.Sphere
import Definitions.Def_SP4Sphere
import Mathlib.Analysis.Normed.Module.Connected

set_option autoImplicit false
open scoped Topology Manifold ContDiff
open ContinuousMap

open SP4Mission

Formal statement

theorem SP4Mission.spc4_iff_local_homotopy_equiv :
    SPC4 ↔
      ∀ (M : Type) [TopologicalSpace M] [T2Space M] [CompactSpace M]
        [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] [IsManifold (𝓡 4) ∞ M],
        Nonempty (M ≃ₜ S4) →
        ∃ f : M ≃ₕ S4, IsLocalDiffeomorph (𝓡 4) (𝓡 4) ∞ f := by sorry

Source

Derived supporting result for Prove2Me SP4Mission.smooth_poincare_4 (acb88840-8df8-4040-89df-f387272d80a9). Hatcher, Algebraic Topology, https://pi.math.cornell.edu/~hatcher/AT/AT.pdf, Propositions 1.30 and 1.34, printed pp. 60 and 62; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, Topology/Covering/Basic.lean, isLocalHomeomorph_iff_isCoveringMap, and Geometry/Manifold/LocalDiffeomorph.lean, IsLocalDiffeomorph.diffeomorphOfBijective. The displayed statement is a corollary derived from these results, not a quotation.

View graph