the base category:

\[thm:mon\_cat\_of\_check\_G\_comodules\] Consider a right multiplier bicomonad $G$ on a monoidal category $\C$. Then the $G$-comodules of Definition \[def:G\_check\_comodule\] and their morphisms constitute a monoidal category such that the evident forgetful functor to $\C$ is strict monoidal.

The monoidal unit $I$ is a $G$-comodule via the composite $$\xymatrix{
I.G(-)\ar[r]^-\cong &
G \ar[r]^-\cong &
G(I.-)}$$ of the unit isomorphisms. For $G$-comodules ${\overrightarrow}v:V.G(-)\to G(V.-)$ and ${\overrightarrow}w:W.G(-)\to G(W.-)$, also $V.W$ is a $G$-comodule via $$\xymatrix{
V.W.G(-)\ar[r]^-{1.{\overrightarrow}w}&
V.G(W.-)\ar[r]^-{{\overrightarrow}v}&
G(V.W.-).}$$ The monoidal product of $G$-comodule morphisms, as well as the unit and associativity isomorphisms, are evidently morphisms of $G$-comodules.

\[ex:EM\_comodule\] We claim that applying Definition \[def:G\_check\_comodule\] to the right multiplier bicomonad $G$ in Example \[ex:G\_check\_from\_bicomonad\], we obtain a category of comodules which is equivalent (in fact, isomorphic) to the usual Eilenberg-Moore category of comodules (or coalgebras). Therefore Theorem \[thm:mon\_cat\_of\_check\_G\_comodules\] generalizes the well-known result [@McCrudden] that the monoidal structure of the base category lifts to the Eilenberg-Moore category of a monoidal comonad.

Consider the category of $G$-comodules in Definition \[def:G\_check\_comodule\] and the forgetful functor to $\C$ sending $(V,{\overrightarrow}v)$ to $V$. We shall show that for a right multiplier bicomonad $G$ as in Example \[ex:G\_check\_from\_bicomonad\], the forgetful functor $U$ has a right adjoint $F$ such 