Right comodules are rational modules over the dual algebra

For $f,g\in C^{\ast }$, the map $c\mapsto (f\otimes g)(\mathrm{\Delta }(c))$ is a linear functional, and the formula is $k$-bilinear in $f$ and $g$, so it defines a $k$-bilinear convolution product. For $f,g,h\in C^{\ast }$ and $c\in C$, the values $((f\ast g)\ast h)(c)$ and $(f\ast (g\ast h))(c)$ are evaluations of $f\otimes g\otimes h$ on $(\mathrm{\Delta }\otimes \mathrm{id})\mathrm{\Delta }(c)$ and $(\mathrm{id}\otimes \mathrm{\Delta })\mathrm{\Delta }(c)$, respectively; these tensors agree by [F1], so convolution is associative. The two counit equations in [F1] give $(\epsilon \ast f)(c)=f(c)=(f\ast \epsilon )(c)$ for every $c$, so $\epsilon$ is a two-sided unit. Thus $a\mapsto a\epsilon$ is a unital ring homomorphism $k\to C^{\ast }$ and is central, since $(a\epsilon )\ast f=a(\epsilon \ast f)=af=f\ast (a\epsilon )$. This gives the existing $k$-vector-space structure on $C^{\ast }$ as a $k$-algebra.

Given a right comodule $(M,\rho )$, the map $C^{\ast }\times M\to M$, $(f,m)\mapsto (\mathrm{id}\otimes f)\rho (m)$, is bilinear. Writing $\rho (m)=\sum m_0\otimes m_1$, coassociativity gives $f\cdot (g\cdot m)=\sum m_{0}f(m_{1,1})g(m_{1,2})=\sum m_0(f\ast g)(m_1)=(f\ast g)\cdot m$. The counit equation gives $\epsilon \cdot m=\sum m_0\epsilon (m_1)=m$. Hence this is a left $C^{\ast }$-module.

For every $m$, the existing tensor $\rho (m)\in M\otimes C$ represents the entire orbit because $(\mathrm{id}\otimes f)\rho (m)=f\cdot m$ for every $f$. This proves rationality without AC. To establish the separation used below, first assume [A1] and let $X$ be any vector space and $T\in X\otimes C$. Write $T={\sum }_s{x}_s\otimes d_s$ as a finite tensor by [F4], and put $D=\mathrm{span}\{d_s\}$. By [F6], choose a finite ordered basis $c_1,\dots ,c_q$ of $D$ and re-expand $T={\sum }_i{y}_i\otimes c_i$. By [F5], choose a complement $E$ with $C=D\oplus E$. For each $i$, let ${\lambda }_i:D\to k$ be the $i$th coordinate function in the basis $c_1,\dots ,c_q$, which is linear by [F9], and define $f_i(d+e)={\lambda }_i(d)$ for $d\in D$ and $e\in E$. The unique direct-sum decomposition makes $f_i$ a linear functional on $C$, so $f_i\in C^{\ast }$ by [F8], and $({\mathrm{id}}_X\otimes f_i)(T)=y_i$. Thus if every $f\in C^{\ast }$ annihilates $T$, every $y_i=0$ and $T=0$. If $C$ is finite-dimensional, [F6] gives a finite ordered basis $c_1,\dots ,c_n$ of $C$; re-expanding $T={\sum }_i{y}_i\otimes c_i$ and evaluating against its coordinate functionals recovers each $y_i$, so the same separation conclusion holds without [A1]. In either branch, if $t,t^{\mathrm{\prime }}\in M\otimes C$ both represent the orbit of $m$, then every $f\in C^{\ast }$ annihilates $t-t^{\mathrm{\prime }}$, and the applicable separation argument gives $t=t^{\mathrm{\prime }}$.

Suppose now $C$ is finite-dimensional, without using AC. By [F6] let $c_1,\dots ,c_n$ be a finite ordered basis, with coordinate functionals $c_1^{\ast },\dots ,c_n^{\ast }$ from [F9]. For any $f\in C^{\ast }$, the functionals $f$ and ${\sum }_{i}f(c_i)c_i^{\ast }$ agree on every basis vector and hence on all of $C$. For a left $C^{\ast }$-module vector $m$, put $t_m={\sum }_{i=1}^n(c_i^{\ast }\cdot m)\otimes c_i$. Then $(\mathrm{id}\otimes f)t_m={\sum }_{i}f(c_i)(c_i^{\ast }\cdot m)=f\cdot m$, so every module vector is rational. Any tensor in $M\otimes C$ can be re-expanded as ${\sum }_i{y}_i\otimes c_i$, and evaluating against $c_j^{\ast }$ recovers $y_j$; therefore the representing tensor is unique. This finite-coordinate argument uses no basis extension or arbitrary choice.

Now let $M$ be a rational left $C^{\ast }$-module. For each $m$, existence in [F3] and separation in step 1.3 make its representing tensor unique in the applicable branch; define $\rho (m)$ to be that unique tensor. Unique existence defines this function without an additional choice. For $m,n$ and $a\in k$, the tensors $\rho (m+n)$ and $\rho (m)+\rho (n)$ have the same evaluation under every $f\in C^{\ast }$ because the action is bilinear; the same holds for $\rho (am)$ and $a\rho (m)$. The separation proved in step 1.3 gives $\rho (m+n)=\rho (m)+\rho (n)$ and $\rho (am)=a\rho (m)$, so $\rho$ is linear.

Evaluation at the unit functional $\epsilon$ gives $(\mathrm{id}\otimes \epsilon )\rho (m)=\epsilon \cdot m=m$ by the module unit law. Thus $\rho$ is counital.

Fix $m$ and write $\rho (m)={\sum }_i{m}_i\otimes c_i$. Set $T=(\rho \otimes \mathrm{id})\rho (m)-(\mathrm{id}\otimes \mathrm{\Delta })\rho (m)\in M\otimes C\otimes C$. For any $f,g\in C^{\ast }$, evaluation of the first term by ${\mathrm{id}}_M\otimes f\otimes g$ is ${\sum }_{i}g(c_i)(f\cdot m_i)=f\cdot (g\cdot m)$, while evaluation of the second term is ${\sum }_i(f\ast g)(c_i)m_i=(f\ast g)\cdot m$. The module associativity law makes these equal. Hence every such pairing annihilates $T$. For fixed $g$, the tensor $({\mathrm{id}}_{M\otimes C}\otimes g)(T)\in M\otimes C$ is annihilated by every ${\mathrm{id}}_M\otimes f$, so it is zero by the separation in step 1.3. Since this holds for every $g$, a second application of that separation result to the last $C$ factor gives $T=0$. Thus $\rho$ is coassociative.

If $u:M\to N$ is a comodule map, then $f\cdot u(m)=({\mathrm{id}}_N\otimes f){\rho }_N(u(m))=({\mathrm{id}}_N\otimes f)(u\otimes \mathrm{id}){\rho }_M(m)=u(f\cdot m)$ for every $f,m$, so $u$ is a module map. Conversely, let $u$ be a $C^{\ast }$-module map. It is $k$-linear because $u(am)=u((a\epsilon )\cdot m)=(a\epsilon )\cdot u(m)=au(m)$, using the $k$-bilinear module action and the unit law. Then $({\mathrm{id}}_N\otimes f)({\rho }_N(u(m))-(u\otimes \mathrm{id}){\rho }_M(m))=f\cdot u(m)-u(f\cdot m)=0$ for every $f$. The difference is a finite tensor in $N\otimes C$, so the separation in step 1.3 makes it zero. Hence $u$ is a comodule map.

In the finite-dimensional case, re-expanding the second factors of any finite tensor in a basis $c_1,\dots ,c_n$ gives ${\sum }_i{x}_i\otimes c_i$, and evaluation against $c_i^{\ast }$ recovers each $x_i$. For a tensor in $X\otimes C\otimes C$, re-expand both $C$ factors to obtain ${\sum }_{i,j}{x}_{ij}\otimes c_i\otimes c_j$; evaluations against $c_i^{\ast }$ and $c_j^{\ast }$ recover every coefficient. These finite-coordinate arguments are exactly the choice-free separation branch established in step 1.3, so the separation uses in steps 2.1, 3.2, and 3.3 need no AC when $C$ is finite-dimensional. Together with step 1.4, this proves the full object and morphism correspondence in that branch without AC.

Steps 1.1–1.3 construct a rational module from every right comodule and recover its unique original coaction; steps 2.1, 3.1, and 3.2 construct a right coaction from every rational module; step 3.3 proves the correspondence on maps. Steps 1.4 and 4.1 prove the full correspondence without AC when $C$ is finite-dimensional.