[proofplan] We compare de Rham cohomology with singular cohomology over $\mathbb{R}$ by the de Rham integration isomorphism, use the singular cohomology [Künneth theorem](/theorems/2274) over the field $\mathbb{R}$, and then identify the resulting cross product with the exterior product of differential forms. The absence of a torsion term is exactly the fact that all tensor products are over a field. Naturality and multiplicativity of the de Rham isomorphism show that the algebraic Künneth isomorphism corresponds to the displayed map. [/proofplan] [step:Define the exterior product map on cohomology classes] For each pair of integers $p,q \geq 0$, define \begin{align*} E_{p,q}: \Omega^p(M) \times \Omega^q(N) &\to \Omega^{p+q}(M \times N),\\ (\alpha,\beta) &\mapsto \pi_M^*\alpha \wedge \pi_N^*\beta . \end{align*} Here $\Omega^r(X)$ denotes the real [vector space](/page/Vector%20Space) of smooth differential $r$-forms on a smooth manifold $X$. If $\alpha \in \Omega^p(M)$ and $\beta \in \Omega^q(N)$ are closed, then \begin{align*} d(\pi_M^*\alpha \wedge \pi_N^*\beta) &= d(\pi_M^*\alpha)\wedge \pi_N^*\beta + (-1)^p \pi_M^*\alpha \wedge d(\pi_N^*\beta)\\ &= \pi_M^*(d\alpha)\wedge \pi_N^*\beta + (-1)^p \pi_M^*\alpha \wedge \pi_N^*(d\beta)\\ &=0. \end{align*} If $\alpha=d\gamma$ for some $\gamma \in \Omega^{p-1}(M)$ and $\beta$ is closed, then \begin{align*} \pi_M^*\alpha \wedge \pi_N^*\beta &= \pi_M^*(d\gamma)\wedge \pi_N^*\beta\\ &= d(\pi_M^*\gamma)\wedge \pi_N^*\beta\\ &= d(\pi_M^*\gamma \wedge \pi_N^*\beta), \end{align*} because $d(\pi_N^*\beta)=0$. The same calculation, with the Koszul sign, applies when $\beta$ is exact and $\alpha$ is closed. Therefore $E_{p,q}$ descends to a well-defined bilinear map \begin{align*} H^p_{\mathrm{dR}}(M) \times H^q_{\mathrm{dR}}(N) &\to H^{p+q}_{\mathrm{dR}}(M \times N). \end{align*} By the universal property of the [tensor product](/page/Tensor%20Product) and summing over all $p+q=k$, this gives the stated map $\kappa_k$. [/step] [step:Compare de Rham cohomology with singular cohomology] For a smooth manifold $X$, let $C_r^{\mathrm{sm}}(X;\mathbb{R})$ denote the real vector space generated by smooth singular $r$-simplices $\sigma:\Delta^r \to X$, and define the smooth singular cochain space by \begin{align*} C^r_{\mathrm{sm}}(X;\mathbb{R}) := \operatorname{Hom}_{\mathbb{R}}(C_r^{\mathrm{sm}}(X;\mathbb{R}),\mathbb{R}). \end{align*} Define the smooth singular coboundary operator $\delta:C^r_{\mathrm{sm}}(X;\mathbb{R})\to C^{r+1}_{\mathrm{sm}}(X;\mathbb{R})$ by \begin{align*} (\delta c)(\sigma) := \sum_{i=0}^{r+1}(-1)^i c(\sigma\circ \iota_i), \end{align*} where $c\in C^r_{\mathrm{sm}}(X;\mathbb{R})$, $\sigma:\Delta^{r+1}\to X$ is a smooth singular $(r+1)$-simplex, and $\iota_i:\Delta^r\to\Delta^{r+1}$ is the inclusion of the $i$-th oriented face. Define the de Rham integration map \begin{align*} \mathcal{I}_X^r: \Omega^r(X) &\to C^r_{\mathrm{sm}}(X;\mathbb{R}),\\ \omega &\mapsto \left(\sigma \mapsto \int_{\Delta^r} \sigma^*\omega \, d\mathcal{L}^r\right), \end{align*} where $\mathcal{L}^r$ is Lebesgue measure on the standard oriented simplex $\Delta^r \subset \mathbb{R}^r$. By [Stokes' theorem](/theorems/1530), $\mathcal{I}_X^\bullet$ is a cochain map from the de Rham complex $(\Omega^\bullet(X),d)$ to the smooth singular cochain complex $(C^\bullet_{\mathrm{sm}}(X;\mathbb{R}),\delta)$. By the [de Rham theorem](/theorems/3596) for smooth singular cochains and the canonical comparison isomorphism from smooth singular cohomology to ordinary singular cohomology, the composite induces an isomorphism \begin{align*} \mathcal{I}_{X,*}^r: H^r_{\mathrm{dR}}(X) &\longrightarrow H^r_{\mathrm{sing}}(X;\mathbb{R}) \end{align*} for every $r \geq 0$. Applying this to $X=M$, $X=N$, and $X=M\times N$, we obtain natural isomorphisms between the de Rham cohomology groups in the statement and the corresponding singular cohomology groups with real coefficients. [/step] [step:Apply the singular Künneth theorem over $\mathbb{R}$] The singular cohomology cross product is the bilinear map \begin{align*} \times: H^p_{\mathrm{sing}}(M;\mathbb{R}) \times H^q_{\mathrm{sing}}(N;\mathbb{R}) &\to H^{p+q}_{\mathrm{sing}}(M\times N;\mathbb{R}). \end{align*} By the preceding step, $H^r_{\mathrm{sing}}(M;\mathbb{R})$ is isomorphic to $H^r_{\mathrm{dR}}(M)$ and $H^r_{\mathrm{sing}}(N;\mathbb{R})$ is isomorphic to $H^r_{\mathrm{dR}}(N)$ for every $r\geq 0$. The theorem statement assumes that the de Rham cohomology groups of $M$ and $N$ are finite-dimensional in each degree, so the corresponding singular cohomology groups with real coefficients are finite-dimensional in each degree. Since $\mathbb{R}$ is a field, every real vector space is flat over $\mathbb{R}$, and these finite-type hypotheses are exactly the hypotheses needed for the cohomological singular Künneth theorem over a field to identify the cross-product map with an isomorphism and to eliminate any torsion correction term. Hence, for each $k \geq 0$, the map \begin{align*} K_k: \bigoplus_{p+q=k} H^p_{\mathrm{sing}}(M;\mathbb{R}) \otimes_{\mathbb{R}} H^q_{\mathrm{sing}}(N;\mathbb{R}) &\longrightarrow H^k_{\mathrm{sing}}(M\times N;\mathbb{R}),\\ a \otimes b &\longmapsto a \times b \end{align*} is an isomorphism. This is the finite-type singular cohomology Künneth theorem over a field. [/step] [step:Identify the singular cross product with the exterior product of forms] Use the singular cohomology cross product defined from the Alexander-Whitney diagonal together with the Eilenberg-Zilber chain equivalence, with the standard Koszul sign convention for cochains. With this convention, the de Rham integration isomorphism is multiplicative with respect to products: for every $\alpha \in \Omega^p(M)$ and $\beta \in \Omega^q(N)$ with $d\alpha=0$ and $d\beta=0$, one has \begin{align*} \mathcal{I}_{M\times N,*}^{p+q} \left([\pi_M^*\alpha \wedge \pi_N^*\beta]\right) = \mathcal{I}_{M,*}^p([\alpha]) \times \mathcal{I}_{N,*}^q([\beta]). \end{align*} This is the multiplicativity part of the de Rham theorem, proved by comparing integration over product simplices with the Eilenberg-Zilber cross product and tracking the standard orientation signs (citing a result not yet in the wiki: multiplicativity of the de Rham isomorphism). Therefore the diagram \begin{align*} \bigoplus_{p+q=k} H^p_{\mathrm{dR}}(M)\otimes_{\mathbb{R}} H^q_{\mathrm{dR}}(N) &\xrightarrow{\ \kappa_k\ } H^k_{\mathrm{dR}}(M\times N)\\ \downarrow\scriptstyle{\bigoplus(\mathcal{I}_{M,*}^p\otimes \mathcal{I}_{N,*}^q)} &\qquad\qquad \downarrow\scriptstyle{\mathcal{I}_{M\times N,*}^k}\\ \bigoplus_{p+q=k} H^p_{\mathrm{sing}}(M;\mathbb{R})\otimes_{\mathbb{R}} H^q_{\mathrm{sing}}(N;\mathbb{R}) &\xrightarrow{\ K_k\ } H^k_{\mathrm{sing}}(M\times N;\mathbb{R}) \end{align*} commutes. [/step] [step:Conclude that the exterior product is an isomorphism] The left vertical map in the preceding diagram is an isomorphism because it is the direct sum of tensor products of de Rham isomorphisms over $\mathbb{R}$. The right vertical map is an isomorphism by the de Rham theorem. The bottom horizontal map $K_k$ is an isomorphism by the singular Künneth theorem over $\mathbb{R}$. Since the diagram commutes and three of its four arrows are isomorphisms, the remaining arrow $\kappa_k$ is an isomorphism. Hence, for every $k \geq 0$, \begin{align*} \kappa_k: \bigoplus_{p+q=k} H^p_{\mathrm{dR}}(M) \otimes_{\mathbb{R}} H^q_{\mathrm{dR}}(N) &\longrightarrow H^k_{\mathrm{dR}}(M\times N) \end{align*} is an isomorphism, which is precisely the Künneth formula for de Rham cohomology. [/step]