Milnor–Whitehead: a weakly contractible topological manifold is contractible

Open

SP4Mission.contractible_of_weaklyContractible_manifold

by ryanshin · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologyhomotopymanifoldssp4-foundationstopology

Let $X$ be a Hausdorff, second countable topological space with a charted-space structure modeled on $\mathbb R^n$ , so that $X$ is a separable metrizable topological $n$ -manifold (without boundary, of any dimension $n\ge0$ ). If all homotopy groups of $X$ vanish at all base points, then $X$ is contractible:

\pi_k(X,x)=0\ \text{ for all } k\ge0,\ x\in X\quad\Longrightarrow\quad X\simeq\ast .

This combines two classical theorems. By Milnor's theorem, every separable manifold has the homotopy type of a countable CW complex; by Whitehead's theorem, a weak homotopy equivalence between connected CW complexes — here the map from a CW model of $X$ to a point — is a homotopy equivalence. Second countability cannot be dropped: the long line has trivial homotopy groups but is not contractible. The statement provides the passage from homotopy-group information to genuine contractibility for the punctured homotopy four-sphere in Freedman's argument.

Formalization Note Weak contractibility is SP4WeakHomotopy.WeaklyContractible X; the conclusion is Mathlib's ContractibleSpace X (a homotopy equivalence with Unit). The manifold hypothesis is a topological atlas ChartedSpace (EuclideanSpace ℝ (Fin n)) X together with T2Space X and SecondCountableTopology X; no smooth structure is involved.

Preamble

import Definitions.Def_SP4Sphere
import Definitions.Def_SP4WeakHomotopy

set_option autoImplicit false

open scoped Manifold ContDiff
open SP4Mission

Formal statement

theorem SP4Mission.contractible_of_weaklyContractible_manifold
    (n : ℕ) (X : Type*) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) X] (hX : SP4WeakHomotopy.WeaklyContractible X) :
    ContractibleSpace X := by sorry

Source

John Milnor, On spaces having the homotopy type of a CW-complex, Trans. Amer. Math. Soc. 90 (1959), 272–280, https://www.ams.org/journals/tran/1959-090-02/S0002-9947-1959-0100267-4/, Theorem 1, p. 272 (the class W₀ of spaces having the homotopy type of a countable CW-complex coincides with the spaces dominated by a countable CW-complex, the spaces of the homotopy type of a countable locally finite simplicial complex, and the spaces of the homotopy type of an absolute neighborhood retract) and Corollary 1, p. 272: "Every separable manifold belongs to the class W₀." Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002 (author's edition: https://pi.math.cornell.edu/~hatcher/AT/AT.pdf), Theorem 4.5 (Whitehead's theorem), p. 346: "If a map f : X → Y between connected CW complexes induces isomorphisms f∗ : πₙ(X) → πₙ(Y) for all n, then f is a homotopy equivalence", applied to the map to a point, together with the remark on p. 352 that this extends to spaces homotopy equivalent to CW complexes; Corollary A.12, p. 529, for the compact case. Reduction child of SP4Mission.punctured_homotopy_sphere_contractible (Freedman 1982, p. 371).

View graph