Right comodules, comodule maps, and subcomodules

Use the convention of Scalars, tensor powers, the empty tensor, opposite algebras and finite sums: $k$ is a field and every tensor product is over $k$, with parentheses in iterated tensors suppressed only through Associator naturality, pentagon, unit triangle and symmetry hexagons on elementary tensors.

Let $C$ be a coalgebra over $k$ with comultiplication $\mathrm{\Delta }:C\to C\otimes C$ and counit $\epsilon :C\to k$ as in Coalgebra and coalgebra map over a field. A right $C$-comodule is a $k$-vector space $M$ with a $k$-linear map, called its coaction, ${\rho }_M:M⟶M\otimes C,$ such that $({\rho }_M\otimes {\mathrm{id}}_C){\rho }_M=({\mathrm{id}}_M\otimes \mathrm{\Delta }){\rho }_M,({\mathrm{id}}_M\otimes \epsilon ){\rho }_M={\mathrm{id}}_M\mathrm{.}$ In the second equality the target $M\otimes k$ is identified with $M$ by the unit isomorphism in the tensor conventions. The direction is part of the convention: a right comodule has its coalgebra factor on the right.

If $(M,{\rho }_M)$ and $(N,{\rho }_N)$ are right $C$-comodules, a right-comodule map is a linear map $f:M\to N$ satisfying ${\rho }_{N}f=(f\otimes {\mathrm{id}}_C){\rho }_M\mathrm{.}$

A subcomodule of $M$ means an injective right-comodule map $i:N\to M$, considered up to isomorphism over $M$. We identify $N$ with its image as a subspace only when the induced coaction on that image has been constructed. This definition does not silently assume that tensoring an arbitrary vector-space inclusion preserves injectivity.

The draft supplier Coalgebra and coalgebra map over a field is present in batch 1. It specifies the coalgebra equations using the same associator and unit maps fixed above.