Product of monoids

I've been interested in studying bialgebras more abstractly, in the form of a bimonoid internal to a symmetric monoidal category, but I'm getting stuck on the compatibility conditions for bimonoids. Allow me to first introduce the definitions.

Let $(\mathcal{C}, \otimes, I)$ be a monoidal category, then a monoid internal to $\mathcal{C}$ is an object $M$ along with a unit map $u: I \to M$ and a multiplication map $m: M \otimes M \to M$ such that some associativity and unit axioms hold, i.e. the relevant diagrams commute. A comonoid internal to $\mathcal{C}$ is an object $C$ along with a counit map $\varepsilon: C \to I$ and a comultiplication map $\Delta: C \to C \otimes C$ such that some coassociativity and counit axioms hold (exactly the reverse of the diagrams for a monoid). For example, in the category of $k$-modules, where $k$ is a commutative ring, a monoid is exactly an associative unital $k$-algebra, and a comonoid is exactly a coassociative counital $k$-coalgebra.

Suppose that we have an object $B$ in the category $\mathcal{C}$ which is both a monoid with maps $(u, m)$ and a comonoid with maps $(\varepsilon, \Delta)$. For $B$ to be a bimonoid, we require some further compatibility between these maps: namely that $(u, m)$ are comonoid homomorphisms, and $(\varepsilon, \Delta)$ are monoid homomorphisms. To check that $\Delta: B \to B \otimes B$ is a monoid homomorphism, we need to be able to put a monoidal structure on $B \otimes B$.

Here is a guess at what the monoidal structure on $B \otimes B$ is meant to be. Suppose $\mathcal{C}$ is now symmetric monoidal, and we have two monoids $(X, u_X, m_X)$ and $(Y, u_Y, m_Y)$ in $\mathcal{C}$.Then $X \otimes Y$ has some candidate maps for making it a monoid. The unit is the following composite:

$$u_{X \otimes Y} = \left(I \xrightarrow{\sim} I \otimes I \xrightarrow{u_X \otimes u_Y} X \otimes Y\right)$$

and the multiplication uses the flip map $T_{Y, X}: Y \otimes X \to X \otimes Y$ coming from the symmetric monoidal structure.

$$m_{X \otimes Y} = \left( X \otimes Y \otimes X \otimes Y \xrightarrow{1 \otimes T_{Y, X} \otimes 1} X \otimes X \otimes Y \otimes Y \xrightarrow{m_X \otimes m_Y} X \otimes Y \right)$$

Question 1: Do these maps make $X \otimes Y$ into a monoid in $\mathcal{C}$?

I can prove the above in special cases (such as the category of $k$-modules), but I am having trouble proving it in an arbitrary symmetric monoidal category, and feel like I might have missed some extra compatibility between the flip map and the multiplication. And to follow up with another question:

Question 2: If there is no natural monoidal structure on $X \otimes Y$, how should I interpret the statement "$\Delta: M \to M \otimes M$ must be a morphism of monoids"?

• Yes, tensor products of monoids are monoids in a symmetric monoidal category. I believe this is false in a monoidal category, and you should be able to find counterexamples where compositions of monads are not monads. According to the nLab the definition of a bimonoid in a monoidal category is difficult to write down, and in fact the nLab doesn’t give such a definition. – Qiaochu Yuan Nov 16 '17 at 23:17
• @QiaochuYuan Thanks for clarifying that. I'm quite happy to stick to symmetric monoidal categories - in this case, do you know where I might find a proof of the fact that $X \otimes Y$ is a monoid? I'm having trouble finding anything on the internet, and on my own I'm struggling to verify even one of the unit axioms. – Joppy Nov 16 '17 at 23:53

It's just naturality of $T$. This is relatively easy to see from a string diagram. Basically, you just slide one of the underlying multiplications through a crossing, then apply associativity, then slide back. Below is a much more opaque equational representation.
For associativity, we want to show that $m_{X\otimes Y} \circ (m_{X\otimes Y}\otimes id_{X\otimes Y}) = m_{X\otimes Y} \circ (id_{X\otimes Y}\otimes m_{X\otimes Y})$. Expanding out the definition we get: \begin{align} & m_{X\otimes Y} \circ (m_{X\otimes Y}\otimes id_{X\otimes Y}) \\ =\ & (m_X\otimes m_Y)\circ(id_X\otimes T\otimes id_Y)\circ (((m_X\otimes m_Y)\circ(id_X\otimes T\otimes id_Y))\otimes id_{X\otimes Y}) \\ =\ & (m_X\otimes m_Y)\circ(id_X\otimes T\otimes id_Y)\circ (m_X\otimes m_Y\otimes id_{X\otimes Y})\circ(id_X\otimes T\otimes id_{Y\otimes X\otimes Y}) \\ =\ & (m_X\otimes m_Y)\circ(m_X\otimes id_X\otimes m_Y\otimes id_Y)\circ (id_{X\otimes X}\otimes T\otimes id_Y)\circ(id_X\otimes T\otimes id_{Y\otimes X\otimes Y}) \\ =\ & (m_X\circ(m_X\otimes id_X))\otimes (m_Y\circ(m_Y\otimes id_Y))\circ (id_{X\otimes X}\otimes T\otimes id_Y)\circ(id_X\otimes T\otimes id_{Y\otimes X\otimes Y}) \\ =\ & (m_X\circ(id_X\otimes m_X))\otimes (m_Y\circ(id_Y\otimes m_Y))\circ (id_{X\otimes X}\otimes T\otimes id_Y)\circ(id_X\otimes T\otimes id_{Y \otimes X\otimes Y}) \\ =\ & (m_X\otimes m_Y)\circ(id_X\otimes m_X\otimes id_Y\otimes m_Y)\circ (id_{X\otimes X}\otimes T\otimes id_Y)\circ(id_X\otimes T\otimes id_{Y\otimes X\otimes Y}) \\ =\ & (m_X\otimes m_Y)\circ(id_X\otimes m_X\otimes id_Y\otimes m_Y)\circ (id_X\otimes T\otimes id_{Y \otimes Y})\circ(id_{X\otimes Y\otimes X}\otimes T\otimes id_Y) \\ =\ & (m_X\otimes m_Y)\circ(id_X\otimes T\otimes id_Y)\circ (id_{X\otimes Y}\otimes m_X\otimes m_Y)\circ(id_{X\otimes Y\otimes X}\otimes T\otimes id_Y) \\ =\ & (m_X\otimes m_Y)\circ(id_X\otimes T\otimes id_Y)\circ (id_{X\otimes Y}\otimes ((m_X\otimes m_Y)\circ(id_X\otimes T\otimes id_Y))) \\ =\ & m_{X\otimes Y}\circ (id_{X\otimes Y}\otimes m_{X\otimes Y}) \end{align}
The first equation expands definitions, then functoriality of $\otimes$ in the left parameter is used, then naturality of $T$, then bifunctoriality of $\otimes$, then associativity of $m_X$ and $m_Y$, and then we do the previous steps in reverse, with a rewrite of the permutation represented by the left hand composite along the way. That can be understood by rewriting via $T_{X,Y\otimes Y} = (T_{X,Y}\otimes id_Y)\circ(id_Y\circ T_{X,Y})$ and applying laws like $T\circ T = id$ and naturality, but really I just rewrote those arrows by utilizing the fact that the point of the coherence laws for the symmetry is that any arrow defined in terms of the symmetry that produces the same permutation is the same arrow. There should also be a bunch of associators and unitors unless the symmetric monoidal structure is stict, but that was too much of a hassle and you don't seem to be concerning yourself with it.