Whitehead's theorem: a weakly contractible CW complex is contractible

Open

SP4Mission.whitehead_contractible

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

algebraic-topologyhomotopysp4-foundationstopology

Let $Y$ be a Hausdorff CW complex which is weakly contractible, i.e. nonempty with all homotopy groups trivial:

\pi_k(Y,y)=0\quad\text{for all } k\ge0 \text{ and all } y\in Y .

Then $Y$ is contractible. This is Whitehead's theorem (Hatcher, Theorem 4.5: a map between connected CW complexes inducing isomorphisms on all homotopy groups is a homotopy equivalence) applied to the map from $Y$ to a one-point CW complex: the hypothesis says exactly that this map is a weak homotopy equivalence, so it is a homotopy equivalence, i.e. $Y\simeq\ast$ . The CW hypothesis cannot be dropped: Hatcher's quasi-circle and the long line are weakly contractible spaces that are not contractible.

Formalization Note The CW structure is Mathlib's Topology.CWComplex (Set.univ : Set Y) (Whitehead's classical definition on the whole space) together with T2Space Y; weak contractibility is SP4WeakHomotopy.WeaklyContractible Y (nonempty, and Subsingleton (HomotopyGroup.Pi k Y y) for all k and y); the conclusion is Mathlib's ContractibleSpace Y. The space is universe polymorphic.

Preamble

import Definitions.Def_SP4Sphere
import Definitions.Def_SP4WeakHomotopy

set_option autoImplicit false

open scoped Manifold ContDiff
open SP4Mission

Formal statement

theorem SP4Mission.whitehead_contractible.{u} (Y : Type u) [TopologicalSpace Y] [T2Space Y]
    [Topology.CWComplex (Set.univ : Set Y)] (hY : SP4WeakHomotopy.WeaklyContractible Y) :
    ContractibleSpace Y := by sorry

Source

Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002 (author's edition: https://pi.math.cornell.edu/~hatcher/AT/AT.pdf), §4.1, Theorem 4.5, 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 from Y to a point; cf. p. 352 (weak homotopy equivalences).

View graph