(note: this question is essentially a reference request for the tensor product described at the end. the rest is context)
It is well known that the category of chain complexes (in positive degree, with a differential decreasing the degree) is equivalent to the category of abelian group object in the category of strict $\infty$-categories.
Abelian group object in the category of $\infty$-category are relatively easy to describe:
It is just an abelian group $G$ endowed with a family of endormophisms $\pi_i^+$, $\pi_i^-$ for $i=0,1, \dots $ satisfying the usual "globular relations":
$$\pi_i^{\delta} \pi_j^{\epsilon} = \left\lbrace \begin{array}{c c} \pi_j^{\epsilon} & \text{ if } j \leqslant i \\ \pi_i^{\delta} & \text{ if } i<j \end{array} \right.$$
and with the additional condition that for all $x\in G, \exists i, \pi_i^{+} x =x $.
Such a structure is then seen as a (strict) $\infty$-category with the composition operation given by:
$$ x \#_k y = x + y - \pi^+_k(x) \quad \text{ (when $\pi^+_k (x) = \pi^{-}_k (y)$) }$$
(Note: We are using Street "one type" definition of $\infty$-category where the composition operation $x \#_k y$ are partially defined operation on the set of all arrow of the $\infty$-category, and for each arrow $a$ the identity arrow of $a$ is identified with $a$.)
From there, the equivalence between a group with such family of endomorphisms and a chain complex is just based on some clever formulas, in the same spirit as the Dold-Kan equivalence between chain complexes and simplicial abelian groups.
Now chain complexes have a natural tensor product, and in order to do some computation in a paper I'm wirting I need to have a description of this tensor product in terms of these abelian groups.
So after some computation that took more time than I can admit, and that I really hope are correct, I came up with the following description:
The tensor product of two abelian groups $X$ and $Y$ with such endomorphisms is given by the tensor product $X \otimes Y$ of abelian group with the endomorphisms given by:
$$ \pi_k ^{\epsilon} (x \otimes y ) = \sum_i \left( \pi^{\epsilon}_i (x) - \pi^{\epsilon}_{i-1}(x) \right) \otimes \pi_{k-i}^{(-1)^i\epsilon} (y) $$
(with the convention that $\pi_i=0$ when $i<0$)
As I said, I need this description in a paper that I'm writting, and the proof I have is just a long and annoying computation.
What I would like to know is if:
Does this description of the tensor product already appear somewhere ?
The last formula seems to describe a nice bi-algebra structure on the algebra generated by the $\pi^{\epsilon}_i$, has someone ever encounter it somewhere else ?
