Künneth formula for Ext groups 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.".
 A: 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.]
A: Here is a non-Noetherian example.
Let $X = Spec(A)$ where $A$ is an algebra which is infinite-dimensional over $k$, and let $Y = Spec(B)$ where $B = k[x_i | i]/(x_i x_j)$ as $i$ ranges over natural numbers.  I will let both of my quasi-coherent sheaves on $X$ be $A$, and let both (finitely presented) quasi-coherent sheaves on $B$ be $B/(x_1)$.
Then your question asks whether there is a natural isomorphism
$$
A \otimes Ext^q_B(B/(x_1),B/(x_1)) \cong Ext^q_{A \otimes B}(A \otimes B/(x_1), A \otimes B/(x_1)),
$$
with tensor products taken over $k$.
I'm going to assume that the desired map is the natural base change map from the left to the right.
There is a resolution of $B$-modules
$$
\cdots \to \bigoplus_{i,j} B \stackrel{\oplus_i(\oplus x_j)}{\to} \bigoplus_i B \stackrel{\oplus x_i}{\to} B \stackrel{x_1}{\to} B \to B/(x_1) \to 0
$$
which remains exact upon tensoring with $A$, by the flatness that you mention.  We can use this to calculate $Ext^2$ in both cases.  Unless I have made a mistake, the map we are analyzing is the map $A \otimes \prod k \to \prod A$, where the product is infinite, and this is not an isomorphism unless $A$ is finite-dimensional over $k$.
(I have to go -- if the Ext calculation needs elaboration, please ask.)
A: First, if $A$ and $B$ are locally free of finite rank, one can rewrite $Ext^p(A,A') = H^p(X,A^*\otimes A')$, and similarly for other parts, and deduce this case from the case for $A = O_X$, $B = O_Y$. 
Now, if $A$ and $B$ are finitely presented on a noetherian scheme, you can write down (possibly infinite) locally free resolutions for $A$ and $B$ and use them to write down spectral sequences computing the LHS and the RHS. The first pages of these spectral sequences will coincide by the previous step, hence the general case.
