Distributivity of tensor products over direct sums for group representations I'm sure that tensor products for group representations are defined such that the typical properties are satisfied, but it would be nice to have an explicit proof, for group representations that:
$$A \otimes (B \oplus C) = (A \otimes B) \oplus (A \otimes C)$$
Where $A,B,C$ are group representations.
I would accept:


*

*A direct, explicit proof of this for group representations

*Alternatively, point out which properties in the definition for tensor product and direct sum for group representations ensures that this property holds, and how.

 A: For the best argument, see the comment by Qiaochu Yuan.
Here is an alternative argument: Let $R$ be a comutative ring. I assume that you already know that the tensor product of $R$-modules commutes with direct sums (see below for the isomorphism). Now let $G$ be a group and let $A,B,C$ be representations of $G$ over $R$, i.e. $R$-modules with an action of $G$. Then the isomorphism of $R$-modules
$f : (A \otimes B) \oplus (A \otimes C) \to A \otimes (B \oplus C), ~ f(a \otimes b)=a \otimes (b,0),~ f(a \otimes c)=a \otimes (0,c)$
is also $G$-equivariant, because $f(g(a \otimes b))=f(ga \otimes gb)=ga \otimes (gb,0)=ga \otimes g(b,0) = g f(a \otimes b)$ and likewise $f(g(a \otimes c))=g f(a \otimes c)$.
Actually, $f$ commutes with the $G$-actions simply because $f$ is a natural isomorphism. Even more abstractly, such a morphism $f$ exists in any monoidal category with coproducts, which is here the category ${}^G \mathsf{Mod}(R)$ of representations of $G$ over $R$. Therefore, actually no computation is needed at all.
Here is a generalization: Let $\mathcal{C}$ be a monoidal category and let $G$ be an arbitrary small category. Then the category ${}^G \mathcal{C}$ of functors $G \to \mathcal{C}$ is again monoidal, the tensor product is defined objectwise. If $\mathcal{C}$ has direct sums which commute with $\otimes$, then the same is true for ${}^G \mathcal{C}$, for trivial reasons: For $A,B,C \in {}^G \mathcal{C}$ there is a canonical morphism $(A \otimes B) \oplus (A \otimes C) \to A \otimes (B \oplus C)$ in ${}^G \mathcal{C}$. That it is an isomorphism, may be checked objectwise, and thereby reduced to $\mathcal{C}$.
