= Solution
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> is
$$
\rho_{M\otimes N}=(1_M\otimes1_N\otimes m_H)(1_M\otimes c_{H,N}\otimes1_H)(\rho_M\otimes\rho_N),
$$
and the unit <coaction> is $j_H:I\to H$. If $f$ is also a <monoid morphism>, then $fm_H=m_K(f\otimes f)$ and $fj_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 $\varepsilon_H\otimes\varepsilon_H$ to their two underlying $H$ factors. The counit laws and <naturality> of the <braiding> remove those factors and leave
$$
fm_H=m_K(f\otimes f).
$$
Equality on the unit <comodule> similarly gives $fj_H=j_K$. Thus $f$ is a <monoid morphism>. \b[The criterion is exactly]
$$
\boxed{f_*\text{ is strict monoidal}\iff f\text{ preserves multiplication and unit}.}
$$
The regular-comodule argument uses only the counit laws; it requires no elementwise or finite-dimensional assumption on the ambient category.
Back to article page
