Does the Tannaka-Krein theorem come from an equivalence of 2-categories?

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.

• I'm not an expert, but I thought that the faithful exact functor---the fibre functor, right?---was not part of the definition of a Tannakian category, and what you have defined above is a neutral Tannakian category. – Kevin Buzzard Jul 3 '10 at 20:59
• @Kevin Buzzard: Oh, maybe. Then what's a Tannakian category? Just a category with a functor to Vect? Wikipedia, in its "formal definition" section, only lists "neutral Tannakian category", but it also demands monoidal rigid, or some such, so that the reconstructed coalgebra is actually a Hopf algebra. I figured that was what the adjective "neutral" was doing. – Theo Johnson-Freyd Jul 4 '10 at 3:24
• @Theo: let me again say that I am not an expert. I thought the idea was that a neutral Tannakian category was one with a fibre functor, and was hence equivalent to the category of representations of a group, and a Tannakian category was one that admitted a fibre functor, but you weren't going to fix any one in particular, so it's slightly weaker than the cat of reps of a group. It's like the difference between the fundamental group and the fundamental groupoid I think, the idea being that choosing a fibre functor is like choosing a point of a top space (and hence getting a stalk where pi1 acts – Kevin Buzzard Jul 4 '10 at 19:10
• @Kevin: Your definitions are historically accurate (and indeed still actively in use), but in my opinion, somewhat outmoded. The notion of Tannaka duality has expanded to include a host of structures other than Hopf algebras and algebroids. For instance, results of Hayashi and Szlachányi show that any sufficiently finite tensor category (i.e., a multi-fusion category) is a category of finite dimensional representations of a quasi-Hopf algebra. This fact, combined with the general difficulty of determining when a category is "Tannakian" in the original sense, make the term misleading at best. – Evan Jenkins Jul 4 '10 at 20:34
• @Theo et al. --- well, you could try looking up the definition in Catégories Tannakiennes (Saavedra 1972, Deligne 1990) or Tannakian Categories (Deligne and ... 1982, Breen 1994) or .. A Tannakian category over a field $k$ is neutral if it admits a fibre functor over $k$. In general, it only admits a fibre functor over an extension of $k$. There are various expressions of Tannaka duality in 2-category terms in Saavedra, e.g., III 2.3.2, p180. – JS Milne Jul 7 '10 at 3:38

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.