Finite CW approximation from bounded homology (source code)

= Finite CW approximation from bounded homology
{title2=$H_i(X)=0\ (i>n)\Rightarrow\dim C\leq n+1$}

Let $X$ be <simply connected>, with finitely generated integral <homology groups>, and suppose $H_i(X;\mathbb Z)=0$ for $i>n$, where $n\geq2$. Then $X$ admits a <weak homotopy equivalence> $C\to X$ from a <finite CW complex> of <dimension> at most $n+1$. If $X$ already has <CW complex> homotopy type, this map is a <homotopy equivalence>.

Start with a finite $n$-dimensional <CW complex> $C_n$ and an \b[$n$-connected map] $f:C_n\to X$, constructed by the <finite type CW approximation>. This means that $f$ induces <isomorphisms> on <homotopy groups> below $n$ and a <surjection> in degree $n$; it does not mean that $C_n$ itself is $n$-connected.

The <kernel> of $H_n(C_n;\mathbb Z)\to H_n(X;\mathbb Z)$ is a finitely generated free <abelian group>, because $H_n(C_n;\mathbb Z)$ is a <subgroup> of its finite free top <cellular chain group>. The <Relative Hurewicz theorem> represents a basis of this kernel by attaching $(n+1)$-cells whose maps extend into $X$. Their <cellular boundary> is injective, killing exactly that kernel without adding top <homology>. All integral <homology groups> now agree, so the <homological Whitehead theorem> proves the conclusion. The acyclic simply connected case is already weakly equivalent to a <point>.