Right-right Hopf modules and coinvariants

Let $k$ be a field, $H$ a Hopf algebra over $k$, and $M$ a $k$-vector space. A right $H$-module structure on $M$ is a bilinear map $(m,h)\mapsto mh$ satisfying $(mh)g=m(hg)$ and $m{1}_H=m$. A right $H$-comodule structure is a linear map $\rho :M\to M\otimes H$ satisfying

$$(\rho \otimes {\mathrm{id}}_H)\rho =({\mathrm{id}}_M\otimes \mathrm{\Delta })\rho ,({\mathrm{id}}_M\otimes \epsilon )\rho ={\mathrm{id}}_M\mathrm{.}$$

Write $\rho (m)=\sum m_0\otimes m_1$ and $\mathrm{\Delta }(h)=\sum h_1\otimes h_2$, where each expression denotes a finite tensor sum. The pair of structures makes $M$ a right-right Hopf module if it satisfies

$$\rho (mh)=\sum m_0{h}_1\otimes m_1{h}_2(m\in M,h\in H)\mathrm{.}$$

A morphism of right-right Hopf modules is a linear map preserving both the right action and right coaction. The coinvariants are the subset

$$M^{\mathrm{co}H}:=\{m\in M:\rho (m)=m\otimes 1_H\}\mathrm{.}$$

The next lemma proves that this subset is a $k$-subspace. No finite-dimensionality of $H$ or $M$, and no bijectivity of the antipode, is part of the definition.