Hurewicz: a simply connected acyclic space is weakly contractible

Open

SP4Mission.weaklyContractible_of_simplyConnected_of_homology_zero

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

algebraic-topologyhomologyhomotopysp4-foundationstopology

Let $X$ be a simply connected topological space (in universe zero) whose integral singular homology vanishes in every positive degree, $H_k(X;\mathbb Z)=0$ for all $k\ge1$ . Then $X$ is weakly contractible:

\pi_1(X)=0\ \text{ and }\ H_k(X;\mathbb Z)=0\ (k\ge1)\quad\Longrightarrow\quad \pi_k(X,x)=0\ \text{ for all } k\ge0,\ x\in X .

This is the inductive form of the Hurewicz theorem: if $X$ is $(n-1)$ -connected with $n\ge2$ , then $\pi_n(X)\cong H_n(X)$ , so vanishing homology propagates connectivity one degree at a time, starting from simple connectivity. The theorem holds for arbitrary topological spaces, no CW structure being required. It is the bridge from the homology computation for a punctured homotopy four-sphere to the vanishing of all of its homotopy groups; contractibility itself then needs Whitehead's theorem in addition.

Formalization Note Simple connectivity is Mathlib's SimplyConnectedSpace X (which includes path connectedness and nonemptiness); homology is SP4Homology.H; the conclusion is SP4WeakHomotopy.WeaklyContractible X.

Preamble

import Definitions.Def_SP4Sphere
import Definitions.Def_SP4WeakHomotopy
import Definitions.Def_SP4Homology

set_option autoImplicit false

open scoped Manifold ContDiff
open SP4Mission CategoryTheory Limits

Formal statement

theorem SP4Mission.weaklyContractible_of_simplyConnected_of_homology_zero
    (X : Type) [TopologicalSpace X] [SimplyConnectedSpace X]
    (hH : ∀ k : ℕ, 1 ≤ k → IsZero (SP4Homology.H k X)) :
    SP4WeakHomotopy.WeaklyContractible X := by sorry

Source

Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002 (author's edition: https://pi.math.cornell.edu/~hatcher/AT/AT.pdf), Theorem 4.32 (Hurewicz theorem), p. 366: "If a space X is (n − 1)-connected, n ≥ 2, then H̃ᵢ(X) = 0 for i < n and πₙ(X) ≈ Hₙ(X)", applied inductively in n starting from simple connectivity; see also Corollary 4.33, p. 367. Reduction child of SP4Mission.punctured_homotopy_sphere_weaklyContractible.

View graph