A space covered by the 3-sphere has finite fundamental group

Proved

PoincareFormalization.finite_fundamental_group_of_spherical_cover

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

covering-spacespoincare-conjecturetopology

Let $M$ be a connected Hausdorff topological space and let $p:S^3\to M$ be a covering map, where $S^3$ is the unit sphere in $\mathbb R^4$ . Then the fundamental group $\pi_1(M,x)$ is finite for every $x\in M$ . No manifold structure or compactness hypothesis on $M$ is needed. This is the necessary direction of the spherical-cover characterization relevant to elliptization. It does not prove existence of a spherical cover, elliptization, or the Poincaré conjecture.

Preamble

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

Formal statement

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

Source

Hatcher, Algebraic Topology (2002), Section 1.3, Proposition 1.32, p. 61 (the compact simply connected covering case), and Proposition 1.14, p. 35 (simple connectedness of spheres): https://pi.math.cornell.edu/~hatcher/AT/AT.pdf . The supplied sphere proof is reused from Kenta Kitamura, https://github.com/KitaKen1/lean-eval-pi-succ-sphere-n-mulequiv-zmod-two/tree/de4d09ac3e86a17d4544c1c86839336ec03a4734 , Submission/PiLow.lean, sphere_simplyConnected, with its four transitive local imports (Apache-2.0). The compact-cover Lean endpoint-injection argument is written for this contribution; the mathematics is classical.

View graph