Constructing a coresolution I am working through computing the homotopy of Thom spectra from Kochman's book.  Let $A$ be a coalgebra over a field $k$, and let $M$ be a right $A$-comodule.  Kochman constructs a coresolution $F$ of $M$ as follows:
Define $F_0=M \otimes A$ and $\eta_0=\psi_M$ (the coaction of $A$ on $M$). Inductively, if $F_n$ and $\eta_n: K_n \rightarrow F_n$ have been defined, we define $K_{n+1}$ to be the cokernel of $\eta_n$.  Then we define $F_{n+1}=K_{n+1} \otimes A$ and $\eta_{n+1}=\psi_{K_{n+1}}$ (the coaction of $A$ on $K_{n+1}$).  
We then get short exact sequences 
$$0 \rightarrow K_n \rightarrow F_n \rightarrow K_{n+1} \rightarrow 0$$
Which we may splice together into a coresolution of $M$ by the $F_n$.  Furthermore, this coresolution has the form $F=F' \otimes A$, which is important later when Kochman proves a change of rings proposition.
Question: In this construction, why does $F_n=K_n \otimes A$ have to be free? 
$K_n$ is the cokernel of $\eta_n: K_n \rightarrow K_n \otimes A$, and it is not clear to me why this cokernel should be a direct sum of copies of $A$. I am not very comfortable working with comodules and coresolutions, so any help here will be greatly appreciated.
 A: Let $V$ be a vector space.  Then $V\otimes A$ is a comodule under the coaction $V\otimes A\rightarrow (V\otimes A)\otimes A$ given by tensoring $V$ with the comultiplication $A\rightarrow A\otimes A$.  If we can show that $V\otimes A$ is a direct sum of copies of the comodule $A$, then taking $V=K_n$ will show $F_n$ is free.
First note that since V is a vector space, $V\cong \bigoplus_{\alpha} k $ where $\alpha$ ranges over some indexing set. Without loss of generality, we may assume that $V=\bigoplus_{\alpha}k$.  Then since the tensor product preserves colimits in $Vect$, we have $\bigoplus_{\alpha} A\cong\bigoplus_\alpha k\otimes A\cong(\bigoplus_{\alpha}k)\otimes A=V\otimes A $ as vector spaces.  The left side is a comodule via the map $\bigoplus_{\alpha}A\rightarrow\bigoplus_{\alpha} A\otimes A\cong (\bigoplus_{\alpha}A)\otimes A$ given by comultiplying each summand.  
All that remains is to show that the obvious map $\bigoplus_\alpha A\rightarrow V\otimes A$ is a comodule homomorphism, so that it will be a comodule isomorphism.  In other words, we must check the commutativity of a square involving this map, it's tensor product with $A$, and the coactions on both comodules.  This is easy to see by applying the naturality of the obvious transformation $\bigoplus_\alpha X\rightarrow (\bigoplus_\alpha k)\otimes X$ to the comultiplication $A\rightarrow A\otimes A$.  The resulting commutative square will be the one we want since the coaction on each comodule is induced by comultiplication; the only difficulty is to check that the map $\bigoplus_\alpha A\otimes A\rightarrow (\bigoplus_\alpha k)\otimes A\otimes A$ coming from the natural transformation agrees with the one given by tensoring the map $\bigoplus_\alpha A\rightarrow V\otimes A$ with $A$.  However, it is easy to check both maps agree on elements of the basis of $\bigoplus_\alpha A\otimes A$ induced by a basis of $A$.
