= Solution
An <opmonoidal monad> on a <monoidal category> is a <monad> $(T,\eta,\mu)$ whose endofunctor is an <opmonoidal functor> and whose <unit and multiplication of a monad> are <opmonoidal natural transformations>. Suppress only the canonical parentheses. Explicitly,
$$
T_2\eta_{X\otimes Y}=\eta_X\otimes\eta_Y,\qquad T_0\eta_I=1_I,
$$
$$
T_2(X,Y)\mu_{X\otimes Y}=(\mu_X\otimes\mu_Y)T_2(TX,TY)T(T_2(X,Y)),\qquad T_0\mu_I=T_0T(T_0).
$$
The composite <opmonoidal functor> $T^2$ has tensor comparison $T_2(TX,TY)T(T_2(X,Y))$ and unit comparison $T_0T(T_0)$, explaining the last two equations.
For two <algebras for a monad> $(X,a)$ and $(Y,b)$, define
$$
\boxed{(X,a)\otimes(Y,b)=\bigl(X\otimes Y,(a\otimes b)T_2(X,Y)\bigr),\qquad\mathbf I=(I,T_0).}
$$
Let $c=(a\otimes b)T_2(X,Y)$. The <unit law for a monad algebra> follows at once from the opmonoidality of $\eta$:
$$
c\eta_{X\otimes Y}=(a\eta_X)\otimes(b\eta_Y)=1.
$$
For the multiplication law, <naturality> of $T_2$, the algebra laws, and the opmonoidality of $\mu$ give
$$
\begin{aligned}
cT(c)&=(a\otimes b)(Ta\otimes Tb)T_2(TX,TY)T(T_2(X,Y))\\
&=(a\mu_X\otimes b\mu_Y)T_2(TX,TY)T(T_2(X,Y))\\
&=(a\otimes b)T_2(X,Y)\mu_{X\otimes Y}=c\mu_{X\otimes Y}.
\end{aligned}
$$
The two unit-comparison equations above similarly make $(I,T_0)$ a <algebra for a monad>. If $f,g$ are <morphisms of algebras for a monad>, <naturality> of $T_2$ shows that $f\otimes g$ is an algebra morphism.
For a third algebra $(Z,d)$, the base <associator> is also an algebra morphism: its intertwining equation is precisely the opmonoidal associativity axiom, followed by $a\otimes b\otimes d$. The two base <unitors> are algebra morphisms by the opmonoidal unit axioms. Their pentagon and triangle commute because they commute after the faithful <forgetful functor>, and the lifted maps have exactly the same underlying <morphisms>.
\b[The <Eilenberg-Moore category> is therefore monoidal], with these lifted constraints. Its <forgetful functor> $U:\mathcal C^T\to\mathcal C$ preserves the tensor product, unit object and constraints exactly, so it is a <strict monoidal functor>.
Back to article page
