Elliptization: a spherical cover for a closed 3-manifold with finite fundamental group

Open

PoincareFormalization.spherical_cover_of_finite_fundamental_group

by salim · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

covering-spaceselliptizationpoincare-conjecturetopology

Let $M$ be a compact, connected, Hausdorff topological 3-manifold without boundary. Let $x\in M$ , and assume the fundamental group $\pi_1(M,x)$ is finite. Then there exists a covering map from the unit 3-sphere to $M$ :

\exists p:S^3\longrightarrow M,\qquad p\text{ is a covering map}.

This is the topological covering-space consequence of the spherical space-form theorem (elliptization), not its stronger diffeomorphism classification. Compactness and local Euclidean charts supply second countability; the topological-to-smooth passage in dimension three is part of the literature's prerequisites. The geometric existence assertion remains an open formalization target. It must not be treated as an already-verified theorem when reducing Poincaré to it.

Preamble

import Mathlib.Geometry.Manifold.ChartedSpace
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
import Mathlib.Topology.Covering.Basic

Formal statement

theorem PoincareFormalization.spherical_cover_of_finite_fundamental_group
    (M : Type*) [TopologicalSpace M] [T2Space M]
    [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M] [CompactSpace M] [ConnectedSpace M]
    (x : M) [Finite (FundamentalGroup M x)] :
    ∃ p : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin (3 + 1))) 1) → M,
      IsCoveringMap p := by sorry

Source

Morgan–Tian, Ricci Flow and the Poincaré Conjecture (2007), Introduction, Corollary 0.2(b), p. x, and the smooth/topological equivalence noted in footnote 1, p. ix: https://www.claymath.org/wp-content/uploads/2022/03/Ricci-pdf.pdf . This statement is its topological covering-space consequence. See also the correction to Section 19.2: https://arxiv.org/abs/1512.00699 .

View graph