Serre-fibration replacement preserves fiber homology transport

By [F1]–[F2], the displayed $j_b$ is the restriction of $j$ to the strict fiber. Let $a:(I^n,\mathrm{\partial }{I}^n)⟶({\mathrm{hofib}}_b(p),j_b(e_0))$ be a based cube, $n\ge 1$, and write $a(x)=(e(x),{\gamma }_x)$. The adjoint $H(x,s)={\gamma }_x(s)$ is a homotopy from $p(e(x))$ to the constant map $b$. Apply [F3] to the finite pair $(I^n,\mathrm{\partial }{I}^n)$, prescribing $e(x)$ at $s=0$ and the constant lift $e_0$ on $\mathrm{\partial }{I}^n\times I$. We obtain $\tilde{H}$ with $p\tilde{H}=H$. For $0\le t\le 1$ put $a_t(x)=(\tilde{H}(x,t),s⟼{\gamma }_x(t+(1-t)s\left)\right)\mathrm{.}$ The second coordinate starts at $p\tilde{H}(x,t)={\gamma }_x(t)$ and ends at $b$, so $a_t$ stays in the homotopy fiber. It is continuous by [F4], is based for every $t$, begins at $a$, and ends at $j_b(x\mapsto \tilde{H}(x,1))$. Thus $(j_b{)}_{\ast }$ is surjective on every positive homotopy group.

Let $(T,S)$ have every component of $T$ meeting $S$ and all positive relative homotopy sets trivial. For a finite relative $G$-cycle $c=\sum g_{\sigma }\sigma$, attach one simplex for every distinct iterated face of its finite support. By [F7] this produces a finite CW pair $(K,L)$, a map $v:(K,L)\to (T,S)$, and a relative cycle $\tilde{c}$ with $v_{\mathrm{\#}}\tilde{c}=c$. Compress the finitely many cells of $K\setminus L$ in increasing dimension: paths move zero-cells into $S$, [F6] compresses each later characteristic disk once its boundary lies in $S$, and the cofibration clause in [F6] extends each finite-stage homotopy. The endpoint $w$ maps $K$ into $S$. The [F8] prism identity says $w_{\mathrm{\#}}\tilde{c}-v_{\mathrm{\#}}\tilde{c}=\mathrm{\partial }P\tilde{c}+P\mathrm{\partial }\tilde{c};$ all terms except $c$ vanish in the relative complex. Its degree-zero clause handles $k=0$. Hence $H_k(T,S;G)=0$ for every $k$, using only finitely many choices for this one chain.

Suppose a based cube $c:(I^n,\mathrm{\partial }{I}^n)\to (F_b,e_0)$ becomes null after applying $j_b$. Represent the nullhomotopy by a map from $I^n\times I$ to the homotopy fiber, constant on $(\mathrm{\partial }{I}^n\times I)\cup (I^n\times \{1\})$ and equal to $j_{b}c$ on $I^n\times \{0\}$. Repeat step 1.1 with this finite cube as parameter space, but prescribe the evident strict-fiber lift on that whole boundary subcomplex. The straightening is relative there. At its endpoint it is a homotopy in $F_b$ from $c$ to the constant cube, so $(j_b{)}_{\ast }$ is injective. The same argument with parameter space $I$ and its two endpoints shows that a path between $j_b(e_0)$ and $j_b(e_1)$ straightens, relative to its endpoints, to a path from $e_0$ to $e_1$ in $F_b$. With a point as parameter, step 1.1 shows every homotopy-fiber component meets $j_b(F_b)$. Hence $j_b$ is also bijective on path components and is a weak homotopy equivalence.

For any weak equivalence $f:X\to Y$, [F5] gives the relative-homotopy hypotheses of step 1.2 for its mapping-cylinder pair $(M_f,jX)$. Hence $H_{\ast }(M_f,jX;G)=0$, and exactness in [F8] makes $j_{\ast }:H_{\ast }(X;G)\to H_{\ast }(M_f;G)$ an isomorphism. The standard quotient formulas retract $M_f$ onto $Y$ and deform the identity to that retraction by [F9]; [F8] makes the induced maps inverse on homology. Thus every weak equivalence induces $G$-homology isomorphisms without AC. Apply this to $j_b$ from step 2.1.

A strictly commuting square $vp=p^{\mathrm{\prime }}u$ induces the pointwise mapping-path map $U:E_p\to E_{p^{\mathrm{\prime }}},U(e,\gamma )=(u(e),v\gamma ),$ and the formulas give the literal equality $Uj=j^{\mathrm{\prime }}u$. Restricting to fibers therefore makes the $(j_b{)}_{\ast }$ natural before and after homology. For a base path $\gamma :b\to c$, the maps $U_c{T}_{\gamma }^{p_p}$ and $T_{v\gamma }^{p_{p^{\mathrm{\prime }}}}{U}_b$ are two endpoint maps obtained by lifting the same path $v\gamma$ with the same initial fiber map. Lifting-function independence in [F10] makes them homotopic in the target fiber. The prism identity [F8], tensored with the arbitrary abelian group $G$, therefore makes their induced $G$-homology maps equal. Define ${\tau }_{\gamma }=(j_c{)}_{\ast }^{-1}{H}_q(T_{\gamma }^{p_p};G)(j_b{)}_{\ast }\mathrm{.}$ Cancellation shows that $(j_b{)}_{\ast }$ commutes with transport, and the just-proved square together with $Uj=j^{\mathrm{\prime }}u$ proves naturality for $(u,v)$.

If $F_b=\mathrm{\varnothing }$ but $(e,\gamma )$ belonged to the homotopy fiber, path lifting for the single path $\gamma$ in [F3] would end at a point of $F_b$, a contradiction; hence both fibers are empty. A one-point fiber, constant paths, both path endpoints, $n=1$, $q=0$, $G=0$, and $G=\mathbb{Z}$ were included above. Every lift concerns one finite CW problem, and step 1.2 handles one finite chain at a time; no family of lifts, bases, or homology representatives is selected. Thus no form of AC is used.