Can the fact that the square of an integer is a natural number be categorified?

Question

If $a$ and $b$ are natural numbers, then $a-b$ is an integer and so the square $(a-b)^2$ is a natural number. In particular

$$ (a-b)^2 \geq 0. \qquad (1)$$

Combining this fact with the identity

$$ ab + ba + (a-b)^2 = a^2 + b^2 \qquad (2)$$

we obtain the inequality

$$ ab + ba \leq a^2 + b^2 \qquad (3)$$

which can be viewed as a special case of either the arithmetic mean-geometric mean inequality or the Cauchy-Schwarz inequality.

Of course this argument can be generalised; for instance, if $v, w$ are elements of a (real or complex) inner product space, then

$$ \langle v-w, v -w \rangle \geq 0 \qquad (1')$$

and by combining this with the identity

$$ \langle v, w \rangle + \langle w, v \rangle + \langle v-w, v-w \rangle = \langle v,v \rangle + \langle w, w \rangle \qquad (2')$$

we conclude the inequality

$$ \langle v, w \rangle + \langle w, v \rangle \leq \langle v, v \rangle + \langle w, w \rangle \qquad (3')$$

which is closely related to the Cauchy-Schwarz inequality (indeed one can amplify (3') to the Cauchy-Schwarz inequality, as discussed in this blog post of mine).

The inequalities (3) or (3') can be interpreted in various categories. For instance, (3) in the category of finite sets becomes

Theorem 1. Let $A, B$ be finite sets. Then there exists an injection from $(A \times B) \uplus (B \times A)$ to $(A \times A) \uplus (B \times B)$.

while (3) in the category of finite-dimensional vector spaces becomes

Theorem 2. Let $V, W$ be finite-dimensional vector spaces. Then there exists an injective linear map from $(V \otimes W) \oplus (W \otimes V)$ to $(V \otimes V) \oplus (W \otimes W)$.

In the category of unitary representations of a compact (or finite) group $G$, a little character theory (or complete reducibility together with Schur's lemma) allows one to similarly interpret (3') in this category:

Theorem 3. Let $V, W$ be finite-dimensional unitary representations of a compact group $G$. Then there exists an injective $G$-equivariant linear map from $(V \otimes W) \oplus (W \otimes V)$ to $(V \otimes V) \oplus (W \otimes W)$.

Theorem 3. Let $V, W$ be finite-dimensional unitary representations of a compact group $G$. Then there exists an injective linear map from $\operatorname{Hom}_G(V,W) \times \operatorname{Hom}_G(W,V)$ to $\operatorname{Hom}_G(V,V) \times \operatorname{Hom}_G(W,W)$.

One can presumably state similar theorems for modules of semisimple algebras over an algebraically closed field, or for various types of vector bundles (or finite covers) over a fixed base space, although I won't attempt to do so here.

Anyway, these results suggest that there may be a way to categorify the inequalities (1), (3), (1'), (3') and/or the identities (2), (2'), for instance by finding a bijective proof (or perhaps an "injective proof") of Theorem 1. However, despite the simplicity of these inequalities and identities this seems to be a surprisingly difficult task. In the ordered case in which one knows that $a=b+k$ or $b=a+k$ for some natural number $k$, one can interpret $(a-b)^2$ as $k^2$, so it is not difficult to categorify Theorem 1 if one possesses an injection from $A$ to $B$ or vice versa, and similarly for Theorem 2 and Theorem 3. From this and the trichotomy of order one can finish off Theorem 1 or Theorem 2, though this is an argument which requires one to make a number of arbitrary choices (as the injections here are not canonical) and so one might consider this to be an incomplete categorification. And in any event, this trick does not seem to recover the full strength of Theorem 3, since there need not be an injective $G$-equivariant map from $V$ to $W$ or vice versa. So I'm wondering if there is another way to categorify these results? For the vector space results (Theorem 2 and Theorem 3) it seems natural to try to use K-theory somehow to achieve this goal (since K-theory already has a formalism for taking formal differences of vector spaces), but I don't know enough K-theory to take this idea further.

[Closely related questions to these were discussed some years ago at the n-category cafe here and here regarding the categorification of the Cauchy-Schwarz inequality, but the results of the discussion were inconclusive, although David Speyer did show that there was an obstruction to categorifying Theorem 3 in the case $G = Z/2Z$ in that the injection could not be natural.]

Answer 1

Probably the most natural thing to ask for Theorem 1 is as follows. Let $\mathcal{A}$ be the category whose objects are pairs of finite sets, and whose morphisms are pairs of bijections. Let $\mathcal{B}$ be the category of finite sets and functions. (Allowing more morphisms in $\mathcal{A}$ or fewer morphisms in $\mathcal{B}$ would make the problem harder.) We have functors $F,G:\mathcal{A}\to\mathcal{B}$ given by $F(A,B)=(A\times B)\uplus(B\times A)$ and $G(A,B)=(A\times A)\uplus(B\times B)$. We then ask whether there is a natural injective map $j:F\to G$. I think the answer is negative. Indeed, the subset $j^{-1}(A\times A)\subseteq F(A,B)$ would have to be preserved by the action of $\text{Aut}(A)\times\text{Aut}(B)$ on $F(A,B)$, so it would have to be $(A\times B)$ or $(B\times A)$, wlog the former. Now $j$ gives an $\text{Aut}(A)\times\text{Aut}(B)$-equivariant map from $A\times B$ to $A\times A$, which consists of two equivariant maps $p,q:A\times B\to A$. For fixed $b$ we have an $\text{Aut}(A)$-equivariant map $p(-,b):A\to A$, and (provided that $|A|>2$) the only possibility is $p(a,b)=a$. Similarly $q(a,b)=a$, and we see that $j$ cannot be injective.

[Added later]

This whole story may be related to Thomason's paper "Beware the phony multiplication on Quillen's $\mathcal{A}^{-1}\mathcal{A}$". Here $\mathcal{A}$ is a symmetric bimonoidal category (like the category of finite-dimensional vector spaces, under $\oplus$ and $\otimes$). From this Quillen constructed a new category $\mathcal{A}^{-1}\mathcal{A}$. The objects are pairs $(A,B)$, where $A$ and $B$ are objects of $\mathcal{A}$. I won't spell out the morphisms except to say that $(A,B)$ is supposed to represent the "formal difference" $A-B$, and everything is guided by that. It is reasonable to hope that there should be a tensor product on $\mathcal{A}^{-1}\mathcal{A}$ compatible with the original tensor product on $\mathcal{A}$. However, Thomason showed that several purported constructions of such a tensor product contain subtle errors, and that a wide class of approaches are doomed to fail.