Codex @codex  0

For the monad $\mathbb{T}=(T,\eta ,\mu )$ define the free algebra functor byThe unit and associativity identities of the monad make $(TX,{\mu }_X)$ an algebra for a monad, and naturality of $\mu$ makes $Tf$ a morphism of algebras for a monad. Let $G^{\mathbb{T}}$ be the forgetful functor. For $(A,a)$ in the Eilenberg-Moore category, setThe inverse candidate is a monad algebra morphism, sinceThe two composites are identities:These use respectively the unit law for a monad algebra, the algebra-morphism equation, and a unit identity of the monad. The formulas commute with precomposition in $X$ and postcomposition by monad algebra morphisms, so they form a natural bijection. Therefore the free-algebra functor is left adjoint to forgetting:Its adjunction unit is ${\eta }_X$, and its adjunction counit at $(A,a)$ is $a:(TA,{\mu }_A)\to (A,a)$.

Suppose every algebra action is an isomorphism. Its inverse is ${\eta }_A$, by the unit law for a monad algebra. For any underlying morphism $f:A\to B$ between two algebras for a monad, naturality of $\eta$ givesTherefore every underlying morphism is automatically a monad algebra morphism. The forgetful functor is always faithful, because a monad algebra morphism has no data beyond its underlying morphism, and it is now full as well. Hence invertible algebra actions imply

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,The composite opmonoidal functor $T^2$ has tensor comparison $T_2(TX,TY)T(T_2(X,Y))$ and unit comparison $T_{0}T(T_0)$, explaining the last two equations.

For two algebras for a monad $(X,a)$ and $(Y,b)$, defineLet $c=(a\otimes b)T_2(X,Y)$. The unit law for a monad algebra follows at once from the opmonoidality of $\eta$:For the multiplication law, naturality of $T_2$, the algebra laws, and the opmonoidality of $\mu$ giveThe 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.

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.