A Hopf-Galois extension of commutative rings, as defined by Montgomery here, is a morphism of commutative rings $\phi:A\to B$ with a Hopf-algebra $H$ coacting on $B$ by a ring map $c:B\to B\otimes H$ such that the following two maps are bijections:
- The canonical inclusion of cofixed points $A\hookrightarrow B^{coH}$ is a bijection, where $B^{coH}=\{b\in B:c(b)=b\otimes 1_H\}$.
- The "Galois" or "torsor" map $\tau:B\otimes_AB\to B\otimes H$ given by $(b_1\otimes b_2)\mapsto\mu_B(b_1,c(b_2))$ is a bijection, where $\mu_B(-,-)$ is the $A$-algebra structure morphism on $B$.
Question: Should any of these maps have more structure? For instance, should the coaction be a map of $A$-algebras rather than just rings? Should the map in 2. be an isomorphism of comodules or corings or something along these lines?
The description I've given above is the way these definitions are given in the sources I've seen, but it seems like they probably could be strengthened in a lot of cases. Does anyone know about this or have a lot of experience with this structure to possibly confirm this?