Details in applying the Barr-Beck monadicity theorem to Tannakian reconstruction
Solution 1:
The Barr-Beck part of the proof is the following.
Theorem: Let $C$ be an essentially small abelian $k$-linear category and let $\omega : C \to \text{Vect}_f$ be an exact faithful functor from $C$ to the category of finite-dimensional $k$-vector spaces. Then this functor exhibits $C$ as the category of finite-dimensional comodules over a coalgebra $A$.
What we would like to do is to show 1) that $\omega$ is comonadic and 2) that the comonad is given by tensoring with a coalgebra $A$, so that coalgebras over the comonad correspond to $A$-comodules.
However, the difference between "comodule" and "finite-dimensional comodule" is extremely important here: it is in fact not possible to apply Barr-Beck directly to $\omega$ because $\omega$ in fact fails to have a right adjoint in general, as soon as $A$ is infinite-dimensional.
The fix is to pass to Ind categories on both sides, and so to consider, not $\omega$, but
$$\text{Ind}(\omega) : \text{Ind}(C) \to \text{Vect}.$$
These ind categories are locally presentable, so the locally presentable form of the adjoint functor theorem applies, and $\text{Ind}(\omega)$ has a right adjoint iff it preserves colimits. It preserves coequalizers because $\omega$ is exact, and it preserves filtered colimits by construction (I think; I haven't checked this carefully).
I am actually not sure how to complete the proof from here. I think one has to show that the right adjoint also preserves colimits, so that the corresponding comonad on $\text{Vect}$ preserves colimits. From here it is an exercise to show, e.g. using the Eilenberg-Watts theorem, that colimit-preserving comonads on $\text{Vect}$ are the same thing as coalgebras, and coalgebras over them are the same thing as comodules.