Right-right Hopf modules are equivalent to vector spaces

Let ${\mathsf{H}\mathsf{o}\mathsf{p}\mathsf{f}\mathsf{M}\mathsf{o}\mathsf{d}}_H^{r,r}$ have right-right Hopf modules as objects and linear maps preserving action and coaction as morphisms; let ${\mathsf{V}\mathsf{e}\mathsf{c}\mathsf{t}}_k$ have vector spaces and linear maps. Define $C(M)=M^{\mathrm{co}H}$ and $C(f)=f{\mathrm{\mid }}_{M^{\mathrm{co}H}}$. If $n$ is coinvariant, then $\rho (f(n))=(f\otimes \mathrm{id})\rho (n)=f(n)\otimes 1_H$, so this restriction is well defined; identities and composites restrict to identities and composites. Hence $C$ is a functor.

Define $T(V)=V\otimes H$ with [F2]'s structure and $T(g)=g\otimes {\mathrm{id}}_H$ for a linear map $g:V\to W$. On elementary tensors, $T(g)$ preserves the right action and coaction by the formulas in [F2]; tensor functoriality gives $T(\mathrm{id})=\mathrm{id}$ and $T(g^{\mathrm{\prime }}f)=T(g^{\mathrm{\prime }})T(f)$. Thus $T$ is a functor.

The maps ${\eta }_V(v)=v\otimes 1_H$ and ${ϵ}_M(n\otimes h)=nh$ are the isomorphisms in [F4] and [F3], respectively. They are natural: for linear $g:V\to W$, $(g\otimes \mathrm{id})(v\otimes 1_H)=g(v)\otimes 1_H$; for a Hopf-module morphism $f:M\to N$, $f(nh)=f(n)h$ on $n\otimes h$. By linearity these equalities give both naturality squares.

For $v\otimes h\in T(V)$, $T({\eta }_V)(v\otimes h)=(v\otimes 1_H)\otimes h$, so ${ϵ}_{T(V)}T({\eta }_V)(v\otimes h)=(v\otimes 1_H)h=v\otimes h$. Therefore ${ϵ}_{T(V)}\circ T({\eta }_V)={\mathrm{id}}_{T(V)}$.

For $n\in C(M)$, $C({ϵ}_M){\eta }_{C(M)}(n)={ϵ}_M(n\otimes 1_H)=n{1}_H=n$. Hence $C({ϵ}_M)\circ {\eta }_{C(M)}={\mathrm{id}}_{C(M)}$. The unit and counit are natural isomorphisms satisfying both triangle identities, so $C$ and $T$ are inverse equivalences.