Whitehead theorem

By [F2], with the empty fixed subcomplex, take a cellular $g:X\to Y$ and a homotopy $E:f\simeq g$. If $X$ is finite this uses its finite clause; otherwise use [A1]. For each $x\in X$, the track ${\gamma }_x(t)=E(x,t)$ runs from $f(x)$ to $g(x)$, and [F6] gives $f_{\ast }={\beta }_{{\gamma }_x}{g}_{\ast }$ on ${\pi }_n(X,x)$ for every $n\ge 1$. Since $f_{\ast }$ and ${\beta }_{{\gamma }_x}$ are isomorphisms, $g_{\ast }$ is an isomorphism. The same tracks show that $f,g$ induce the identical function on components. Thus $g$ is weak at all basepoints and on all components, even though $E$ need not fix any prescribed basepoint.

Form the ordinary mapping cylinder $M=M_g$ using [F3], with source inclusion $j:X\hookrightarrow M$, target inclusion $k:Y\hookrightarrow M$ and retraction $r:M\to Y$. Then $rj=g$, $rk={\mathrm{i}\mathrm{d}}_Y$, and the cylinder deformation $D$ runs from ${\mathrm{i}\mathrm{d}}_M$ to $kr$, fixing $k(Y)$. By [F4] and step 1.1, $j$ is bijective on components and ${\pi }_n(M,X,j(x))$ is trivial for every $x$ and $n\ge 1$. These are exactly the hypotheses of [F5] for the CW pair $(M,j(X))$.

Apply [F5] to obtain a continuous $\rho :M\to X$ with $\rho j={\mathrm{i}\mathrm{d}}_X$ and a homotopy $K:{\mathrm{i}\mathrm{d}}_M\simeq j\rho$ fixing $j(X)$. If $X,Y$ are finite, [F3] lists the cells of $M\setminus j(X)$ as the cells of $Y$ and one prism for each cell of $X$, a finite family. Hence the finite clause of [F5] applies and needs no choice. For arbitrary $X,Y$, use its [A1] clause. These are the only second-stage choices; the mapping-cylinder construction itself was specified without choices.

Put $h=\rho k:Y\to X$. The homotopy $(x,t)\mapsto \rho D(j(x),t)$ starts at $\rho j={\mathrm{i}\mathrm{d}}_X$ and ends at $\rho krj=\rho kg=hg$. The homotopy $(y,t)\mapsto rK(k(y),t)$ starts at $rk={\mathrm{i}\mathrm{d}}_Y$ and ends at $rj\rho k=gh$. Thus $hg\simeq {\mathrm{i}\mathrm{d}}_X$ and $gh\simeq {\mathrm{i}\mathrm{d}}_Y$, with continuous homotopies supplied by these formulas. By [F6], $h$ is a homotopy inverse of $g$.

Composing $E$ with $h$ on the left and right gives $hf\simeq hg$ and $fh\simeq gh$. Concatenating with the reversals of the two homotopies in step 4.1 yields $hf\simeq {\mathrm{i}\mathrm{d}}_X$ and $fh\simeq {\mathrm{i}\mathrm{d}}_Y$. This proves that the original $f$, rather than just its cellular replacement, is a homotopy equivalence. No based inverse is asserted for an arbitrary unbased map.

If $X$ is empty, weak equivalence forces $Y$ empty by the component condition; the unique maps give the conclusion. Zero relative cells in step 3.1 give the stationary compression, and zero-dimensional cells and coincident endpoint images are covered by the cylinder construction. Neither disconnectedness nor unbounded dimension is excluded: [F1], [F4] and [F5] use every source point and the component bijection. The finite case uses only the finite clauses in steps 1.1 and 3.1. In the arbitrary case AC selects the disk deformations for cellular approximation and the compression witnesses for the source retraction, exactly as accounted for in those two suppliers. The explicit compositions in steps 4.1–5.1 introduce no further choice and check both inverse identities.