Let $X$ be a smooth, compact, quasi-projective, complex algebraic variety and let $K(X)=K_0(X)=K_0(\mathrm{Coh}(X))$ be the Grothendieck group of coherent sheaves on $X$. There are several notions of tensor product in this setting. My question is about compatibility between two of them. The setup is exactly that of Chriss-Ginzburg's Representation Theory and Complex Geometry, chapter 5. I actually want everything $G$-equivariant but I think it's not essential to my question.
The external tensor product $\boxtimes\colon K(X)\otimes_\mathbb{Z} K(X)\to K(X\times X)$
is given by $[\mathcal{F}]\boxtimes[\mathcal{G}]:=[p_1^*\mathcal{F}\otimes_{X\times X}p_2^*\mathcal{G}]$, where the $p_i$ are the obvious projections $X\times X\to X$ and $p_i^*$ means pullback of $\mathcal{O}_X$-modules. The $p_i$ are flat, hence the above definition makes sense. (Note that $\boxtimes$ defines an exact functor between the relevant categories of coherent sheaves, so its a matter of taste where to put the brackets.)
The tensor product on $K(X)$ is the map $\otimes\colon K(X)\otimes_\mathbb{Z} K(X)\to K(X)$ given by $[\mathcal{F}]\otimes[\mathcal{G}]:=\Delta^*([\mathcal{F}]\boxtimes[\mathcal{G}])$, where $\Delta\colon X\to X\times X$ is the diagonal and
$$
\Delta^*[\mathcal{F}]=\sum_i(-1)^i[\mathcal{H}^i(\Delta_*\mathcal{O}_X\otimes_{\mathcal{O}_{X\times X}}\mathcal{F}^\bullet)]
$$
where $\mathcal{F}^\bullet\to\mathcal{F}$ is a finite locally-free resolution of $\mathcal{F}$.
My question is: is it true that for $\mathcal{F}_i,\mathcal{G}_i$ on $X$, the following is true in $K(X\times X)$:
$$
([\mathcal{F}_1]\boxtimes[\mathcal{G}_1])\otimes([\mathcal{F}_2]\boxtimes[\mathcal{G}_2])=
([\mathcal{F}_1]\otimes[\mathcal{F}_2])\boxtimes([\mathcal{G}_1\otimes[\mathcal{G}_2])?
$$
If not, is there another formula? On one hand I know that $\otimes$ agrees with convolution given the hypotheses on $X$, contradicting my guessed formula, but also I think I remember someone telling me that this formula was correct.
Edit: $\otimes$ agreeing with convolution here would make convolution commutative, , and there are definitely examples of that not being true.
Best Answer
It seems that the bounty is insufficient to attract an answer, so I will answer myself based on what I came up with myself.
It's slightly easier to work not in the setup of K-theory as in Chriss-Ginzburg but to really view these calculations in K-theory of the triangulated category $D^b\mathrm{Coh}(X)$. Either way it turns out that the formula I ask about is true, and it is indeed a formality. The key is the following diagram, in which every map that isn't a diagonal map is projection onto the labelled factor.
Now we expand each side of the claim.
The left hand side gives
\begin{align*} (\mathcal{F}_1\boxtimes\mathcal{G}_1)\otimes_{\mathcal{O}_{Y\times Y}}(\mathcal{F}_2\boxtimes\mathcal{G}_2)&= \Delta^*\left((\mathcal{F}_1\boxtimes\mathcal{G}_1)\boxtimes(\mathcal{F}_2\boxtimes\mathcal{G}_2)\right)\\ &\simeq \Delta^*\left(p_1^*(\mathcal{F}_1\boxtimes\mathcal{G}_1)\otimes_{\mathcal{O}_{Y^4}}p_2^*(\mathcal{F}_2\boxtimes\mathcal{G}_2)\right)\\ &\simeq \Delta^*\left(p_1^*(q_1^*\mathcal{F}_1\otimes_{\mathcal{O}_{Y^2}}q_2^*\mathcal{G}_1)\otimes_{\mathcal{O}_{Y^4}}p_2^*(r_1^*\mathcal{F}_2\otimes_{\mathcal{O}_{Y^2}}r_2^*\mathcal{G}_2)\right)\\ &\simeq \Delta^*\left((p_1^*q_1^*\mathcal{F}_1\otimes_{\mathcal{O}_{Y^4}}p_2^*r_2^*\mathcal{G}_1)\otimes_{\mathcal{O}_{Y^4}}(p_1^*q_1^*\mathcal{F}_2\otimes_{\mathcal{O}_{Y^4}}p_2^*r_2^*\mathcal{G}_2)\right)\\ &\simeq \Delta^*p_1^*q_1^*\mathcal{F}_1\otimes_{\mathcal{O}_{Y^2}}\Delta^*p_2^*r_2^*\mathcal{G}_1\otimes_{\mathcal{O}_{Y^2}}\Delta^*p_1^*q_1^*\mathcal{F}_2\otimes_{\mathcal{O}_{Y^2}}\Delta^*p_2^*r_2^*\mathcal{G}_2), \end{align*}
whereas the right hand side gives
\begin{align*} \pi_1^*\left(\mathcal{F}_1\otimes_{\mathcal{O}_Y}\mathcal{F}_2\right)\otimes_{\mathcal{O}_Y^2}\pi_2^*\left(\mathcal{G}_1\otimes_{\mathcal{O}_Y}\mathcal{G}_2\right) &\simeq \pi_1^*\left(\Delta_1^*(\mathcal{F}_1\boxtimes\mathcal{F}_2)\right)\otimes_{\mathcal{O}_{Y^2}}\pi_2^*\left(\Delta_2^*(\mathcal{G}_1\boxtimes\mathcal{G}_2)\right)\\ &\simeq \pi_1^*\left(\Delta_1^*(\alpha_1^*\mathcal{F}_1\otimes_{\mathcal{O}_{Y^2}}\alpha_2^*\mathcal{F}_2)\right)\otimes_{\mathcal{O}_Y^2}\pi_2^*\left(\Delta_2^*(\beta_1^*\mathcal{G}_1\otimes_{\mathcal{O}_{Y^2}}\beta_2^*\mathcal{G}_2)\right)\\ &\simeq \pi_1^*\Delta_1^*\alpha_1^*\mathcal{F}_1\otimes_{\mathcal{O}_{Y^2}}\pi_1^*\Delta_1^*\alpha_2^*\mathcal{F}_2\otimes_{\mathcal{O}_{Y^2}}\pi_2^*\Delta_2^*\beta_1^*\mathcal{G}_1\otimes_{\mathcal{O}_{Y^2}}\pi_2^*\Delta_2^*\beta_2^*\mathcal{G}_2\\ &\simeq \Delta^*p_1^*q_1^*\mathcal{F}_1\otimes_{\mathcal{O}_{Y^2}}\Delta^*p_2^*r_2^*\mathcal{G}_1\otimes_{\mathcal{O}_{Y^2}}\Delta^*p_1^*q_1^*\mathcal{F}_2\otimes_{\mathcal{O}_{Y^2}}\Delta^*p_2^*r_2^*\mathcal{G}_2). \end{align*}
As to my question about tensor product agreeing with convolution giving a contradiction: The issue is that tensor product agrees with convolution on $X$ viewed as the diagonal in $X\times X$, but convolution depends on the ambient variety, and of course in general these is no notion of convolution of (objects of the derived category of) coherent sheaves on just an arbitrary smooth compact variety.