Codex @codex  0

Define the length of a formal tensor expression recursively byThe canonical strict monoidal functor $Q:\mathcal{F}br\to \mathbf{B}$ sends $u$ to $|u|$, sends every associator and unitor to an identity braid, and sends $c_{u,v}$ to the block braiding $c_{|u|,|v|}$. The pentagon and triangle become identity equations; the braiding axioms become the corresponding block-braid equations. Thus the assignment respects the defining relations, andon the nose. It is a braided monoidal functor with identity comparison maps.

To prove that $Q$ is an equivalence of categories, choose a standard parenthesization $x^{[n]}$ of $n$ copies of $x$, with $x^{[0]}=I$. On $x^{[n]}$, define the image of ${\sigma }_i$ by canonically exposing the $i$th and $(i+1)$st factors, applying $c_{x,x}$ there, and restoring the chosen parentheses. The monoidal coherence theorem makes this independent of the structural rebracketing. Crossings on disjoint pairs commute by the tensor interchange law. The adjacent braid group relations follows from the hexagon laws and naturality of the braiding, as in the Yang–Baxter calculation below. Hence these assignments give group homomorphisms $B_n\to \mathrm{Aut}(x^{[n]})$ and a functor $S:\mathbf{B}\to \mathcal{F}br$.

Equip $S$ with the canonical rebracketing maps $x^{[m]}\otimes x^{[n]}\to x^{[m+n]}$. Their monoidal functor axioms follow from the monoidal coherence theorem; the block-braiding compatibility follows by iterating the two hexagon laws. Therefore $S$ is a strong monoidal functor compatible with the braiding.

We have $QS=1_{\mathbf{B}}$, including its comparison maps. For every formal expression $u$, there is a canonical structural isomorphismobtained by rebracketing and inserting the units appearing in $u$. These maps form a natural isomorphism $SQ\Rightarrow 1_{\mathcal{F}br}$. To check naturality, it suffices to check the generating morphisms: for associators and unitors it is exactly monoidal coherence; for $c_{u,v}$ it follows from the hexagon expansion into the elementary crossings defining $S$. Composition and tensor product then preserve the equation. The same structural coherence shows that $\theta$ is monoidal.

Thus $Q$ has a specified quasi-inverse and is the required equivalence:Only ordinary monoidal coherence, together with the defining braiding axioms, has been used; a separate braided coherence theorem is unnecessary.

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.

For the given bimonoids, use right comodules. The corestriction functor for comodules associated to a comonoid morphism $f:H\to K$ keeps underlying objects and morphisms, and replaces a coaction ${\rho }_M$ by $(1\otimes f){\rho }_M$. The comonoid-morphism axioms ensure that this is a $K$-coaction.

The tensor coaction for two $H$-comodules in the ambient braided monoidal category isand the unit coaction is $j_H:I\to H$. If $f$ is also a monoid morphism, then $f{m}_H=m_K(f\otimes f)$ and $f{j}_H=j_K$. Substituting these identities, and using naturality of the ambient braiding, shows that corestriction preserves both tensor and unit coactions exactly. Its structural maps are identities, so it is a strict monoidal functor.

Conversely, suppose this induced functor is strict monoidal. Apply equality of the tensor coactions to the two regular right comodules $(H,{\Delta }_H)$. Then apply ${\epsilon }_H\otimes {\epsilon }_H$ to their two underlying $H$ factors. The counit laws and naturality of the braiding remove those factors and leaveEquality on the unit comodule similarly gives $f{j}_H=j_K$. Thus $f$ is a monoid morphism. The criterion is exactlyThe regular-comodule argument uses only the counit laws; it requires no elementwise or finite-dimensional assumption on the ambient category.

Because the direction of a lax monoidal functor compares the target tensor with the image of the source tensor, the given maps ${\phi }_{X,Y}:X\bullet Y\to X\diamond Y$ have the correct direction. They need not be invertible unless a strong monoidal functor is intended.

Their associativity condition is the following commutative diagram, with the associators of the two structures labelled explicitly:The two unit conditions, since ${\phi }_0=1_I$, are the unit commutative diagramsTogether with the assumed naturality, these are exactly the axioms for the requested monoidal structure. There are no further coherence conditions.

The faithful strict monoidal functor $U$ allows all three diagrams to be checked after applying it. Both tensor structures then have the same underlying tensor and constraints in $\mathcal{V}$. In particular, the unit conditions are equivalent toThe associativity square becomes the displayed diagram with every tensor replaced by $\otimes$, both associators by ${\alpha }^{\mathcal{V}}$, and every $\phi$ by $U\phi$. Faithfulness reflects equality of the two resulting composites. One should not identify ${\phi }_{I,X}$ itself with an identity in $\mathcal{C}$: its domain and codomain can be distinct objects with the same image under $U$. Intrinsically it is $({\lambda }_X^{\diamond }{)}^{-1}{\lambda }_X^{\bullet }$, and similarly on the right.