The fundamental theorem of right-right Hopf modules

The function $(n,h)\mapsto nh$ is bilinear on $M^{\mathrm{co}H}\times H$, since the action is bilinear and the coinvariants form a subspace [F2]. The tensor-product universal property therefore gives a unique linear map $\alpha :M^{\mathrm{co}H}\otimes H\to M$ with $\alpha (n\otimes h)=nh$.

Define $\beta :=(P\otimes {\mathrm{id}}_H)\rho$. Since $P$ has range in $M^{\mathrm{co}H}$ by [F3], the tensor map has codomain $M^{\mathrm{co}H}\otimes H$; thus $\beta$ is well defined and is exactly $\sum P(m_0)\otimes m_1$. This range argument uses the map $P$, not a claim that each individual Sweedler summand is coinvariant.

By coassociativity of the coaction and the definition of $P$, $(\alpha \beta )(m)=\sum P(m_0)m_1=\sum (m_{0}S(m_1))m_2=\sum m_0\epsilon (m_1)=m$. The third expression uses the right antipode identity in [F6] and the right-module associativity; the last uses the counit identity. Hence $\alpha \beta ={\mathrm{id}}_M$.

For $n\in M^{\mathrm{co}H}$ and $h\in H$, apply compatibility twice and anti-multiplicativity in [F5] to obtain $\beta (nh)=\sum n_0{h}_{1}S(n_1{h}_2)\otimes n_2{h}_3=\sum n_0{h}_{1}S(h_2)S(n_1)\otimes n_2{h}_3$. Coassociativity and $\rho (n)=n\otimes 1_H$ give $\sum n_0\otimes n_1\otimes n_2=n\otimes 1_H\otimes 1_H$, so this reduces to $\sum n{h}_{1}S(h_2)\otimes h_3$. The identity $\sum h_{1}S(h_2)\otimes h_3=1_H\otimes h$, derived from [F6] followed by the counit equation, makes this $n\otimes h$. Pure tensors span, so $\beta \alpha ={\mathrm{id}}_{M^{\mathrm{co}H}\otimes H}$.

The map $\alpha$ is right $H$-linear: $\alpha ((n\otimes h)g)=n(hg)=(nh)g=\alpha (n\otimes h)g$. It is right $H$-colinear because $(\alpha \otimes \mathrm{id})\rho (n\otimes h)=\sum n{h}_1\otimes h_2=\rho (nh)$, where the final equality is compatibility and $\rho (n)=n\otimes 1_H$. These equalities hold on pure tensors and therefore on the full tensor product.

Steps 1.3 and 2.1 show that $\alpha$ and $\beta$ are inverse linear maps. Since $\alpha$ preserves action and coaction by step 2.2, its inverse preserves them too: apply ${\alpha }^{-1}$ to the action identity, and apply ${\alpha }^{-1}\otimes {\mathrm{id}}_H$ to the coaction identity. Thus both maps are Hopf-module morphisms and $\alpha$ is the asserted isomorphism. The proof uses $S$ but nowhere uses $S^{-1}$.