Possibly the correct answer to this question is simply a pointer towards some recent literature on Tannaka-Krein-type theorems. The best article I know on the subject is the excellent
- André Joyal and Ross Street, An introduction to Tannaka duality and quantum groups, Category Theory, Lecture Notes in Math, 1991 vol. 1488 pp. 412–492
from which I'm getting most of my facts.
Let me fix, once and for all, a field $\mathbb K$. I will denote by $\text{Vect}$ the usual category of all $\mathbb K$-vector spaces, and by $\text{FinVect}$ its full subcategory of dualizable objects. The notions of (coassociative, counital) coalgebra and (right, say, and coassociative and counital) comodule are standard; briefly, if $(\mathcal V,\otimes)$ is a monoidal category, a coalgebra in $\mathcal V$ is an object $A$ along with a map $A \to A \otimes A$ satisfying some axioms, and an $A$-comodule is an object $X$ and a map $X \to X\otimes A$ satisfying some axioms. Here's the fast way to say the axioms. Without telling you anything, it's clear what should be a homomorphism of comodules, namely a map $f: X\to Y$ so that the maps $X \overset f \to Y \to Y\otimes A$ and $X \to X\otimes A \overset{f\otimes {\rm id}}\to Y\otimes A$ agree. Then a coalgebra $A$ is coassociative iff the comultiplication $A\to A\otimes A$ is a homomorphism of $A$-comodules, and a comodule $X$ is coassociative iff $X\to X\otimes A$ is a homomorphism of comodules. (In both cases, the comodule structure on the right is just the comultiplication in the second factor.) I will abuse language so that all coalgebras and comodules are coassociative. Oh, and I haven't said anything about counits, but I want them as well. Given a coalgebra $A$, I will denote its category of right comodules by $\text{Comod}_A$, and of finite-dimensional right comodules by $\text{FinComod}_A$.
Let's say that a Tannakian category is a $\mathbb K$-linear (i.e. $\text{Vect}$-enriched) abelian category $\mathcal C$ along with a faithful exact $\mathbb K$-linear functor $F: \mathcal C \to \text{FinVect}$. (If this is not the most standard definition, let me know.) The fundamental theorem is the following:
Theorem (c.f. Op. cit.): Let $F: \mathcal C \to \text{FinVect}$ be any functor from any category. Then there is a coalgebra $\operatorname{End}^\vee(F) \in \text{Vect}$ given by a certain natural colimit (take the definition of the vector space of natural transformations and turn all arrows around; use the fact that the endomorphism of a finite-dimensional vector space is naturally a coalgebra). The functor $F$ factors through $\text{FinComod}_{\operatorname{End}^\vee(F)}$ (and its forgetful functor to $\text{FinVect}$), and $\operatorname{End}^\vee(F)$ is universal with respect to this property (if $F$ factors through $\text{forget}: \text{FinComod}_A \to \text{FinVect}$, then there is a map $\operatorname{End}^\vee(F) \to A$ inducing this). If $(\mathcal C,F)$ is Tannakian, then the map $\mathcal C \to \text{FinComod}_{\operatorname{End}^\vee(F)}$ is an equivalence of categories.
It follows from the above theorem that there is an equivalence of categories between:
$$ \{\text{Tannakian categories}, \text{strictly commuting triangles}\} \leftrightarrow \{\text{coalgebras}, \text{homomorphisms}\}$$
By a "strictly-commuting triangle" of Tannakian categories $(\mathcal C,F) \overset{f}\to (\mathcal D,G)$, I mean a functor $f: \mathcal C \to D$ so that we have strict equality $F = G\circ f$ as functors $\mathcal C \to \text{Vect}$.
But when talking about functors, etc., it's evil to think about strict equality. Rather, there should be some two-categories floating around. There is a natural two-category whose objects are coalgebras: the one-morphisms are bicomodules, the two-morphisms are homomorphisms of bicomodules, and the one-composition is cotensor product of bicomodules. There are, to my mind, a few different two-categories whose objects are Tannakian categories: perhaps the one-morphisms should be triangles that commute up to specified natural isomorphism ("strong"?), or up to specified natural transformation in one way or in the other ("lax" and "oplax"?).
All together, my question is as follows:
Question: What is the correct, non-evil two-category of Tannakian categories so that the last two sentences of the "Tannaka theorem" above expresses an equivalence of two-categories
$\{\text{Tannakian categories}\} \leftrightarrow \{\text{coalgebras}, \text{bicomodules}, \text{homomorphisms}\}$?
Is this two-category a full sub-two-category of some larger two-category whose objects are pairs
$(\mathcal C, F:\mathcal C \to \text{Vect})$ with no further conditions? If so, does the full theorem represent some sort of "Tannakaization" of such pairs?
If modifications need to be made (not quite the right two-category of coalgebras, not quite the right definition of Tannakian category for the question to have an answer, etc.) feel free to answer the corresponding question.
Best Answer
Your question is dealt with (in a slightly more general setting) in section 11 of Daniel Schäppi's paper, Tannaka duality for comonoids in cosmoi. Specializing to your setting, he shows that there is a biadjunction (a weak 2-categorical form of adjunction) between the 2-category of $k$-linear categories equipped with a functor to $\operatorname{FinVect}$, where morphisms are triangles commuting up to specified natural isomorphism, and the usual category of coalgebras (thought of as a 2-category with only identity 2-morphisms). I believe this biadjunction should restrict to a biequivalence on the sub-2-category of Tannakian categories (as you have defined them).
This biadjunction is useful because there is a nice tensor product on the 2-category of $k$-linear categories that turns this biadjunction into a monoidal biadjunction, which gives us a way of relating things like bialgebras and tensor categories.