[proofplan] We prove the isomorphism by comparing two cohomology theories on CW complexes via the cross product. Define graded functors $F^n(X) = \bigoplus_{k+l=n} H^k(X; R) \otimes_R H^l(Y; R)$ and $G^n(X) = H^n(X \times Y; R)$. The cross product defines a natural transformation $\Phi: F^n \to G^n$. Both functors satisfy the Eilenberg-Steenrod axioms for cohomology in the $X$ variable (homotopy invariance, Mayer-Vietoris/long exact sequences, and the dimension axiom), with the freeness hypothesis on $H^*(Y; R)$ ensuring that tensoring with $H^l(Y; R)$ preserves exactness for $F^n$. The base case $X = \{*\}$ is verified directly. The general case follows by induction on the CW cell structure of $X$: attaching an $n$-cell gives a pair $(X^n, X^{n-1})$ whose long exact sequences are related by $\Phi$, and the Five Lemma upgrades the inductive hypothesis to the inductive step. Passage to infinite CW complexes uses a limit argument. [/proofplan]

[step:Define the two graded functors $F^*$ and $G^*$ and the natural transformation $\Phi$]Fix a commutative ring $R$ and a topological space $Y$ such that $H^l(Y; R)$ is a finitely generated free $R$-module for every $l \geq 0$. For a topological space $X$, define graded $R$-modules \begin{align*} F^n(X) &:= \bigoplus_{k+l=n} H^k(X; R) \otimes_R H^l(Y; R), \\ G^n(X) &:= H^n(X \times Y; R). \end{align*} For a continuous map $f: X_1 \to X_2$, define $F^n(f): F^n(X_2) \to F^n(X_1)$ by $F^n(f) = \bigoplus_{k+l=n} f^* \otimes \operatorname{id}_{H^l(Y;R)}$, and $G^n(f) = (f \times \operatorname{id}_Y)^*: G^n(X_2) \to G^n(X_1)$. The cross product in singular cohomology defines a natural transformation \begin{align*} \Phi^n_X: F^n(X) &\to G^n(X), \\ \alpha \otimes \beta &\mapsto \alpha \times \beta, \end{align*} where $\alpha \times \beta \in H^{k+l}(X \times Y; R)$ is the cohomology cross product of $\alpha \in H^k(X; R)$ and $\beta \in H^l(Y; R)$. Naturality follows from the naturality of the cross product: for $f: X_1 \to X_2$, we have $(f \times \operatorname{id}_Y)^*(\alpha \times \beta) = f^*(\alpha) \times \beta$.[/step]

[guided]The strategy of the proof is to treat the cross product as a natural transformation between two "cohomology theories in the $X$ variable" (with $Y$ held fixed). We will verify that both $F^*$ and $G^*$ satisfy the axioms that characterise a cohomology theory, and then use a uniqueness argument -- induction on the cell structure of $X$ together with the Five Lemma -- to show that any natural transformation between two such theories that is an isomorphism on a point must be an isomorphism on all CW complexes. Why do we need $H^l(Y; R)$ to be free? The functor $G^n(X) = H^n(X \times Y; R)$ always has long exact sequences (from the long exact sequence of a pair). For $F^n$, which involves tensor products, we need the long exact sequence of a pair $(X, A)$ in the first variable to remain exact after tensoring with $H^l(Y; R)$. This is guaranteed when $H^l(Y; R)$ is a free $R$-module, since tensoring with a free module is exact.[/guided]

[step:Verify the base case: $\Phi$ is an isomorphism when $X = \{*\}$ is a point] When $X = \{*\}$, we have $H^k(\{*\}; R) = R$ for $k = 0$ and $H^k(\{*\}; R) = 0$ for $k \geq 1$. Therefore \begin{align*} F^n(\{*\}) = \bigoplus_{k+l=n} H^k(\{*\}; R) \otimes_R H^l(Y; R) = R \otimes_R H^n(Y; R) \cong H^n(Y; R). \end{align*} On the other hand, $\{*\} \times Y \cong Y$, so $G^n(\{*\}) = H^n(Y; R)$. Under the identification $R \otimes_R H^n(Y; R) \cong H^n(Y; R)$ given by $r \otimes \beta \mapsto r\beta$, the cross product $\Phi^n_{\{*\}}$ sends $1_R \otimes \beta$ to $1_R \times \beta$. The class $1_R \in H^0(\{*\}; R)$ is the unit of the cohomology ring, and $1_R \times \beta$ corresponds to the pullback of $\beta$ along the projection $\{*\} \times Y \to Y$, which under the identification $\{*\} \times Y \cong Y$ is just $\beta$ itself. Hence $\Phi^n_{\{*\}}$ is the canonical isomorphism $R \otimes_R H^n(Y; R) \cong H^n(Y; R)$, and in particular is an isomorphism. [/step]

[step:Verify that both $F^*$ and $G^*$ are homotopy-invariant in the $X$ variable] The functor $G^n$ is homotopy-invariant in $X$: if $f, g: X_1 \to X_2$ are homotopic, then $f \times \operatorname{id}_Y, g \times \operatorname{id}_Y: X_1 \times Y \to X_2 \times Y$ are homotopic (via the homotopy $H \times \operatorname{id}_Y$ where $H$ is the homotopy between $f$ and $g$), so $(f \times \operatorname{id}_Y)^* = (g \times \operatorname{id}_Y)^*$ on $H^n(X_2 \times Y; R)$. The functor $F^n$ is homotopy-invariant in $X$ because each $H^k(X; R)$ is a homotopy invariant of $X$. If $f \simeq g$, then $f^* = g^*$ on $H^k(X_2; R)$, so $f^* \otimes \operatorname{id} = g^* \otimes \operatorname{id}$ on each summand of $F^n$. [/step]

[step:Verify that $F^*$ and $G^*$ admit long exact sequences for pairs, using the freeness hypothesis for $F^*$]For a CW pair $(X, A)$ with inclusion $i: A \hookrightarrow X$ and quotient map $q: X \to X/A$, singular cohomology gives a long exact sequence in $G^*$: \begin{align*} \cdots \to H^{n-1}(A \times Y; R) \xrightarrow{\delta} H^n(X \times Y, A \times Y; R) \to H^n(X \times Y; R) \to H^n(A \times Y; R) \to \cdots \end{align*} which we identify with \begin{align*} \cdots \to G^{n-1}(A) \xrightarrow{\delta_G} G^n(X, A) \to G^n(X) \to G^n(A) \to \cdots \end{align*} where $G^n(X, A) := H^n(X \times Y, A \times Y; R)$. For $F^*$, the long exact sequence of the pair $(X, A)$ in singular cohomology gives, for each degree $k$: \begin{align*} \cdots \to H^{k-1}(A; R) \xrightarrow{\delta} H^k(X, A; R) \to H^k(X; R) \to H^k(A; R) \to \cdots \end{align*} We tensor this sequence with $H^l(Y; R)$ over $R$. Since $H^l(Y; R)$ is a finitely generated free $R$-module by hypothesis, the functor $- \otimes_R H^l(Y; R)$ is exact. Therefore the tensored sequence \begin{align*} \cdots \to H^{k-1}(A; R) \otimes_R H^l(Y; R) \xrightarrow{\delta \otimes \operatorname{id}} H^k(X, A; R) \otimes_R H^l(Y; R) \to H^k(X; R) \otimes_R H^l(Y; R) \to \cdots \end{align*} remains exact. Taking the direct sum over all pairs $(k, l)$ with $k + l = n$ gives a long exact sequence \begin{align*} \cdots \to F^{n-1}(A) \xrightarrow{\delta_F} F^n(X, A) \to F^n(X) \to F^n(A) \to \cdots \end{align*} where $F^n(X, A) := \bigoplus_{k+l=n} H^k(X, A; R) \otimes_R H^l(Y; R)$.[/step]

[guided]This is the step where the freeness hypothesis is consumed. If $H^l(Y; R)$ were merely a finitely generated $R$-module (with torsion), tensoring with it could destroy exactness. For example, tensoring the exact sequence $0 \to \mathbb{Z} \xrightarrow{\times 2} \mathbb{Z} \to \mathbb{Z}/2 \to 0$ with $\mathbb{Z}/2$ gives $0 \to \mathbb{Z}/2 \xrightarrow{0} \mathbb{Z}/2 \to \mathbb{Z}/2 \to 0$, which is not exact on the left. This failure is precisely what the Universal Coefficient Theorem for the Kunneth formula accounts for with $\operatorname{Tor}$ terms. Since $H^l(Y; R)$ is free, it is isomorphic to $R^{m_l}$ for some finite $m_l \geq 0$. Tensoring an exact sequence with $R^{m_l}$ simply takes $m_l$ copies of the sequence, which is exact. This is why the long exact sequence for $F^*$ works. The direct sum over $(k, l)$ with $k + l = n$ is finite in each degree (only finitely many $l$ contribute a nonzero $H^l(Y; R)$ in any bounded range) and a finite direct sum of exact sequences is exact.[/guided]

[step:Show $\Phi$ intertwines the long exact sequences of $F^*$ and $G^*$]For a CW pair $(X, A)$, the cross product extends to relative cohomology: there is a relative cross product \begin{align*} \Phi^n_{(X,A)}: F^n(X, A) = \bigoplus_{k+l=n} H^k(X, A; R) \otimes_R H^l(Y; R) \to H^n(X \times Y, A \times Y; R) = G^n(X, A) \end{align*} defined by $\alpha \otimes \beta \mapsto \alpha \times \beta$, where the cross product of a relative class $\alpha \in H^k(X, A; R)$ with $\beta \in H^l(Y; R)$ lands in $H^{k+l}(X \times Y, A \times Y; R)$. The naturality of the cross product with respect to the maps in the long exact sequence of a pair ensures that the following diagram commutes: \begin{align*} \cdots \to F^{n-1}(A) &\xrightarrow{\delta_F} F^n(X, A) \to F^n(X) \to F^n(A) \to \cdots \\ \Phi^{n-1}_A \downarrow \quad &\quad \Phi^n_{(X,A)} \downarrow \qquad \Phi^n_X \downarrow \qquad \Phi^n_A \downarrow \\ \cdots \to G^{n-1}(A) &\xrightarrow{\delta_G} G^n(X, A) \to G^n(X) \to G^n(A) \to \cdots \end{align*} The commutativity of the squares involving restriction maps follows from the naturality of the cross product. The commutativity of the connecting homomorphism square $\delta_G \circ \Phi^{n-1}_A = \Phi^n_{(X,A)} \circ \delta_F$ follows from the compatibility of the cross product with the coboundary map: for $\alpha \in H^{k-1}(A; R)$ and $\beta \in H^l(Y; R)$, we have $\delta(\alpha \times \beta) = \delta(\alpha) \times \beta$, which holds because the cross product is defined at the cochain level and the coboundary acts only on the first factor.[/step]

[guided]Why does $\delta(\alpha \times \beta) = \delta(\alpha) \times \beta$? At the cochain level, the cross product of cochains $\varphi \in C^k(X; R)$ and $\psi \in C^l(Y; R)$ is defined using the Eilenberg-Zilber map. The key property is that the coboundary of a cross product satisfies $\delta(\varphi \times \psi) = \delta\varphi \times \psi + (-1)^k \varphi \times \delta\psi$. When $\psi$ is a cocycle (representing $\beta \in H^l(Y; R)$), the second term vanishes, giving $\delta(\varphi \times \psi) = \delta\varphi \times \psi$. This cochain-level identity descends to the connecting homomorphism of the long exact sequence: if $\alpha \in H^{k-1}(A; R)$ is represented by a cocycle $\varphi$ on $A$, then $\delta(\alpha)$ is the class in $H^k(X, A; R)$ obtained by extending $\varphi$ and taking the coboundary, and the cross product of this extension with $\psi$ gives an extension of $\varphi \times \psi$ whose coboundary is $\delta\varphi \times \psi$. The commutativity of the diagram is what allows us to apply the Five Lemma: if four of the five vertical maps are isomorphisms, so is the fifth.[/guided]

[step:Prove the isomorphism for finite-dimensional CW complexes by induction on the number of cells]We prove by induction on the CW cell structure of $X$ that $\Phi^n_X: F^n(X) \to G^n(X)$ is an isomorphism for all $n$. **Base case: $X = \{*\}$.** This was established above. **Inductive step for attaching a single cell.** Suppose $X = X' \cup_\varphi D^m$, where $X'$ is a CW complex for which $\Phi_{X'}$ is an isomorphism in all degrees, and $D^m$ is an $m$-cell attached along $\varphi: \partial D^m \to X'$. Consider the CW pair $(X, X')$. By excision in singular cohomology, $H^n(X, X'; R) \cong H^n(D^m, \partial D^m; R)$, and similarly $H^n(X \times Y, X' \times Y; R) \cong H^n(D^m \times Y, \partial D^m \times Y; R)$. We verify that $\Phi$ is an isomorphism on the pair $(D^m, \partial D^m)$. Since $D^m$ is contractible, $\Phi_{D^m}$ is an isomorphism by homotopy invariance (reducing to the point case). For the relative term, we verify $\Phi$ is an isomorphism on $(D^m, \partial D^m)$ using the long exact sequences of $(D^m, \partial D^m)$: First, $\Phi_{\partial D^m}$ is an isomorphism. When $m \geq 2$, $\partial D^m \cong S^{m-1}$ is a CW complex with two cells (a $0$-cell and an $(m-1)$-cell), so by induction on the number of cells, $\Phi_{S^{m-1}}$ is an isomorphism. When $m = 1$, $\partial D^1 = S^0$ consists of two points, and the isomorphism follows from the point case and the additivity of cohomology on disjoint unions. Now consider the ladder of long exact sequences for $(D^m, \partial D^m)$: \begin{align*} \cdots \to F^{n-1}(\partial D^m) &\xrightarrow{\delta_F} F^n(D^m, \partial D^m) \to F^n(D^m) \to F^n(\partial D^m) \to \cdots \\ \Phi^{n-1}_{\partial D^m} \downarrow \quad &\quad \Phi^n_{(D^m, \partial D^m)} \downarrow \qquad \Phi^n_{D^m} \downarrow \qquad \Phi^n_{\partial D^m} \downarrow \\ \cdots \to G^{n-1}(\partial D^m) &\xrightarrow{\delta_G} G^n(D^m, \partial D^m) \to G^n(D^m) \to G^n(\partial D^m) \to \cdots \end{align*} The maps $\Phi_{D^m}$ and $\Phi_{\partial D^m}$ are isomorphisms by the preceding paragraph. By the [Five Lemma](/theorems/???), $\Phi_{(D^m, \partial D^m)}$ is an isomorphism in all degrees. Returning to the pair $(X, X')$: the excision isomorphisms identify $\Phi_{(X, X')}$ with $\Phi_{(D^m, \partial D^m)}$, which is an isomorphism. Consider the ladder of long exact sequences for $(X, X')$: \begin{align*} \cdots \to F^{n-1}(X') &\xrightarrow{\delta_F} F^n(X, X') \to F^n(X) \to F^n(X') \to \cdots \\ \Phi^{n-1}_{X'} \downarrow \quad &\quad \Phi^n_{(X, X')} \downarrow \qquad \Phi^n_X \downarrow \qquad \Phi^n_{X'} \downarrow \\ \cdots \to G^{n-1}(X') &\xrightarrow{\delta_G} G^n(X, X') \to G^n(X) \to G^n(X') \to \cdots \end{align*} The maps $\Phi_{X'}$ (by the inductive hypothesis) and $\Phi_{(X, X')}$ (by excision and the preceding argument) are isomorphisms. By the [Five Lemma](/theorems/???), $\Phi_X$ is an isomorphism in all degrees.[/step]

[guided]The induction proceeds by adding cells one at a time to build up $X$. At each stage, we have a CW complex $X'$ (for which the isomorphism is known) and we attach a single cell $D^m$ along its boundary $\partial D^m$. The pair $(X, X')$ has relative cohomology concentrated in a single degree (degree $m$, since $(X, X') \simeq (D^m / \partial D^m) = S^m$ by the quotient), but we do not need this simplification -- the Five Lemma handles all degrees simultaneously. Why does excision apply? For a CW pair $(X, X')$ where $X = X' \cup_\varphi D^m$, the interior of the attached cell is open in $X$, and excision in singular cohomology gives $H^n(X, X'; R) \cong H^n(D^m, \partial D^m; R)$. The product with $Y$ preserves this: $(X \times Y, X' \times Y)$ and $(D^m \times Y, \partial D^m \times Y)$ satisfy the same excision relationship because $(X \times Y) \setminus (X' \times Y) = (X \setminus X') \times Y$ is open in $X \times Y$. The Five Lemma argument works as follows. In the ladder of long exact sequences, four out of every five consecutive vertical maps are known to be isomorphisms (two from $\Phi_{X'}$ and two from $\Phi_{(X,X')}$), so the fifth ($\Phi_X$) must also be an isomorphism. More precisely, for each $n$, the five maps in the ladder are $\Phi^{n-1}_{X'}$, $\Phi^n_{(X,X')}$, $\Phi^n_X$, $\Phi^n_{X'}$, and $\Phi^{n+1}_{(X,X')}$; the first, second, fourth, and fifth are isomorphisms, so the Five Lemma forces the third to be an isomorphism as well.[/guided]

[step:Extend to infinite CW complexes via the limit over finite skeleta] For a CW complex $X$ with infinitely many cells, write $X = \bigcup_{m=0}^\infty X^m$ where $X^m$ is the $m$-skeleton. By the preceding step, $\Phi_{X^m}$ is an isomorphism for every $m$. Since singular cohomology of a CW complex satisfies $H^n(X; R) \cong \varprojlim_m H^n(X^m; R)$ (the cohomology of a CW complex is determined by its finite skeleta, as every singular chain has compact image and hence lands in some finite skeleton), we have \begin{align*} G^n(X) = H^n(X \times Y; R) \cong \varprojlim_m H^n(X^m \times Y; R) = \varprojlim_m G^n(X^m). \end{align*} Similarly, $H^k(X; R) \cong \varprojlim_m H^k(X^m; R)$, and since $H^l(Y; R)$ is finitely generated free, tensoring with it commutes with inverse limits (a finitely generated free module is finitely presented, and $\operatorname{Hom}$ from a finitely presented module commutes with direct limits; equivalently, $- \otimes_R R^{m_l} \cong (-)^{m_l}$ commutes with any limit). Therefore \begin{align*} F^n(X) = \bigoplus_{k+l=n} H^k(X; R) \otimes_R H^l(Y; R) \cong \varprojlim_m \bigoplus_{k+l=n} H^k(X^m; R) \otimes_R H^l(Y; R) = \varprojlim_m F^n(X^m). \end{align*} The maps $\Phi_{X^m}$ are compatible with the restriction maps in the inverse system (by naturality of the cross product), so they assemble into a map $\Phi_X = \varprojlim_m \Phi_{X^m}$. Since each $\Phi_{X^m}$ is an isomorphism, the inverse limit $\Phi_X$ is an isomorphism. [/step]

[step:Verify that $\Phi$ is a ring isomorphism]The preceding steps establish that $\Phi$ is an isomorphism of graded $R$-modules. It remains to verify that $\Phi$ respects the ring structures. The ring structure on $F^*(X) = H^*(X; R) \otimes_R H^*(Y; R)$ is the tensor product of graded rings: for $\alpha_1 \otimes \beta_1 \in H^k(X; R) \otimes_R H^l(Y; R)$ and $\alpha_2 \otimes \beta_2 \in H^{k'}(X; R) \otimes_R H^{l'}(Y; R)$, the product is \begin{align*} (\alpha_1 \otimes \beta_1) \cdot (\alpha_2 \otimes \beta_2) = (-1)^{l \cdot k'} (\alpha_1 \cup \alpha_2) \otimes (\beta_1 \cup \beta_2), \end{align*} where the sign $(-1)^{l \cdot k'}$ arises from the Koszul sign convention for graded tensor products: passing $\beta_1$ (degree $l$) past $\alpha_2$ (degree $k'$) incurs the sign $(-1)^{l \cdot k'}$. The ring structure on $G^*(X) = H^*(X \times Y; R)$ is the cup product. The cross product satisfies the multiplicative property \begin{align*} (\alpha_1 \times \beta_1) \cup (\alpha_2 \times \beta_2) = (-1)^{l \cdot k'} (\alpha_1 \cup \alpha_2) \times (\beta_1 \cup \beta_2). \end{align*} This identity holds at the cochain level: expanding the cross product via the Eilenberg-Zilber map and applying the cup product, the sign $(-1)^{l \cdot k'}$ arises from the same graded commutativity that governs the tensor product of graded rings. Therefore \begin{align*} \Phi\bigl((\alpha_1 \otimes \beta_1) \cdot (\alpha_2 \otimes \beta_2)\bigr) &= \Phi\bigl((-1)^{l \cdot k'} (\alpha_1 \cup \alpha_2) \otimes (\beta_1 \cup \beta_2)\bigr) \\ &= (-1)^{l \cdot k'} (\alpha_1 \cup \alpha_2) \times (\beta_1 \cup \beta_2) \\ &= (\alpha_1 \times \beta_1) \cup (\alpha_2 \times \beta_2) \\ &= \Phi(\alpha_1 \otimes \beta_1) \cup \Phi(\alpha_2 \otimes \beta_2), \end{align*} so $\Phi$ is a homomorphism of graded rings. Combined with the module isomorphism established above, $\Phi$ is an isomorphism of graded rings: \begin{align*} \times: H^*(X; R) \otimes_R H^*(Y; R) \xrightarrow{\cong} H^*(X \times Y; R). \end{align*}[/step]

[guided]The sign $(-1)^{l \cdot k'}$ in the multiplication rule for the tensor product of graded rings is dictated by the Koszul sign convention: whenever two elements of degrees $p$ and $q$ are transposed in a graded-commutative context, a sign $(-1)^{pq}$ is introduced. In the product $(\alpha_1 \otimes \beta_1) \cdot (\alpha_2 \otimes \beta_2)$, we need to "pass $\beta_1$ past $\alpha_2$" to collect the $\alpha$-terms and $\beta$-terms together, introducing the sign $(-1)^{\deg(\beta_1) \cdot \deg(\alpha_2)} = (-1)^{l \cdot k'}$. The fact that the cross product satisfies the same sign rule is not a coincidence -- it is a consequence of the graded commutativity of singular cohomology and the definition of the cross product via the Eilenberg-Zilber chain map. The Eilenberg-Zilber map $\nabla: C_*(X) \otimes C_*(Y) \to C_*(X \times Y)$ is a chain map that respects the graded algebra structure up to these signs, and the cross product is defined dually. The unit of $F^*(X)$ is $1_X \otimes 1_Y$ where $1_X \in H^0(X; R)$ and $1_Y \in H^0(Y; R)$ are the cohomological units. Under $\Phi$, this maps to $1_X \times 1_Y$, which equals the pullback of $1_X$ and $1_Y$ along the two projections. Since $\pi_X^*(1_X) \cup \pi_Y^*(1_Y) = 1_{X \times Y}$ (both are the unit in $H^0$), the map $\Phi$ preserves units as well.[/guided]