Field Kunneth isomorphism for homology of products

A nonzero ideal of $k$ contains an invertible element and hence $1$, so every ideal is either zero or generated by $1$; thus $k$ is a PID and [F1] applies. For every homology vector space $V$, [F2] gives a basis and projectivity. The complex with $V$ only in degree zero, augmented by its identity to $V$, is a projective resolution. Tensoring it with any $k$-vector space $W$ yields a complex supported only in degree zero, whose first homology is zero. By [F3], ${\mathrm{Tor}}_1^k(V,W)=0$. AC supplies the DC required there, as in the stated supplier, and the resolution is explicitly supplied rather than inferred from DC.

Every term of the finite Tor diagonal in [F1] vanishes by step 1.1. Its exact sequence becomes $0\to K\stackrel{\times }{\to }{H}_n(X\times Y;k)\to 0$, which makes the actual cross product injective and onto. Its naturality is the naturality of that same left arrow in [F1], so no chosen vector-space basis enters the isomorphism.

At $n=0$, the Tor diagonal was already empty and the same conclusion holds; at every higher $n$ only $n+1$ tensor summands occur, regardless of their dimensions. Empty $X$ or $Y$ gives zero source and target. On two point zero-simplices the unit tensor maps to the unit product simplex. Zero homology factors contribute zero tensor summands, as follows directly from the tensor relations. The basis and projectivity uses in step 1.1 are covered by AC, with no finite-dimensional substitution for that assumption.