Setup: Let $X,Y$ be quasi-compact quasi-separated schemes defined over a field $k$. If necessary, you can also assume that $X,Y$ are noetherian, but I don't want to assume that $X,Y$ have the resolution property. Let $A,A'$ be quasi-coherent sheaves on $X$ and $B,B'$ quasi-coherent sheaves on $Y$. Assume that $A,B$ are of finite presentation (i.e. coherent in the noetherian case). Recall that the external tensor product is defined by $A \boxtimes B := \mathrm{pr}_X^* A \otimes_{\mathcal{O}_{X \times_k Y}} \mathrm{pr}_Y^* B$.
My question: Is there a natural isomorphism
$$\bigoplus_{p+q=n} \mathrm{Ext}^p_X(A,A') \otimes_k \mathrm{Ext}^q_Y(B,B') \cong \mathrm{Ext}^n_{X \times_k Y}(A \boxtimes B,A' \boxtimes B') ~ ?$$
I can prove this for $n=0$. It is also true when $A=\mathcal{O}_X$ and $B=\mathcal{O}_Y$ (see MO/34673), hence more generally when $A$ and $B$ are locally free of finite rank. For the general case, my idea is to take injective resolutions $I^*$ of $A'$ and $J^*$ of $B'$, and hope that the total complex of the double complex $I^* \boxtimes J^*$ is an injective or at least flasque resolution of $A' \boxtimes B'$ in order to apply Künneth's Theorem for complexes. But I'm not sure if the external tensor product of flasque sheaves is flasque. They can be chosen to be quasi-coherent in the noetherian case, which probably makes life easier.
In any case I think that this must be well-known. A reference would be appreciated. Interestingly, EGA III$_2$ §6 treats "Functeurs Tor locaux et globaux; formule de Künneth", but in EGA III$_1$ this was announced as "Foncteurs Tor et Ext locaux et globaux; formule de Künneth.".
Best Answer
The question asks if the map
$ RHom_X(A,A') \otimes_k RHom_Y(B,B') \simeq RHom_{X \times_k Y}(p_1^* A \otimes p_2^* B, p_1^* A' \otimes p_2^* B)$
via the product map. Here is an argument when $A$ and $B$ are coherent. It is probably false in general.
Assume first that $Y$ is separated. If $\{U_i\}$ is a Zariski open cover of $Y$ by affines indexed by a finite set $I$, then write $U_J = \cap_{j \in J} U_j$, where $J \subset I$ is a subset; these schemes are also affine if $J$ is non-empty by separatedness. One can calculate $RHom_Y(B,B')$ using $RHom_{U_J}(B_J,B'_J)$ for $J \neq \emptyset$ by an obvious construction, essentially Mayer-Vietoris applied to $\underline{RHom}_Y(B,B')$. The same formula also applies to compute $RHom_{X \times Y}(p_1^* A \otimes p_2^* B, p_1^* A' \otimes p_2^* B)$ in terms of the corresponding object over $X \times U_J$. The product map is compatible with this description, so you reduce to $Y$ affine. Repeating the argument, you reduce to $X$ affine. Then one may use the existence of (infinite) free resolutions with finite free terms ensured by coherence. To replace separatedness by quasiseparatedness, repeat the argument using the just proven separated case instead of the affine case.
[Alternatively: one can use approximation by perfect complexes to reduce to $A$ and $A'$ being perfect complexes, which makes it very easy as one can dualize and use the projection formula.]