Equivalence of categories and axiom of choice

Question

I don't understand much about set theory but nevertheless try to learn category theory. In books like Gelfand Manin, there is the well known theorem that a functor defines an equivalence of categories iff it is fully faithful and essentially surjective. The proof implicitely uses some kind of axiom of choice for proper classes, which, I guess, cannot be proved in ZFC.

From my mathematical education I am used to only use ZFC for proving theorems and even explicitely mention every use of the axiom of choice for sets. So from my mathematical education I would say, that the above theorem is simply "wrong" and should not be used by a any serious mathematician working outside of set theory, e.g. number theory or algebraic geometry.

As this theorem is stated in every place without comment (okay, Wikipedia has a very sloppy comment, which doesn't state which kind of axiom of choice in what kind of strange set theory is needed), I wonder if all the category theorists have as less clue about set theory than me and what parts of pure mathematics are "wrong" because of nobody cares? Or is there some good set theoretic argument in favour of this theorem.

Answer 1

When reasoning about arbitrary (large) categories, it's a good idea to use something more than ZFC - maybe you like Grothendieck universes (https://en.wikipedia.org/wiki/Grothendieck_universe), or some class theory such as NBG plus global choice (https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory). ZFC alone doesn't let us do very much. So my understanding is that, in general category theory, it is not unusual to assume a somewhat stronger foundational theory than ZFC.

Now, the way I see it, you have two primary worries: are these stronger foundations consistent, and - if so - are they true?

• As far as consistency goes, these stronger foundations are only very slightly stronger, generally. As it turns out, passing to a stronger foundational theory doesn't really take very much effort: for instance, NBG + global choice is consevative over ZFC, meaning that it won't prove any new statements about sets that ZFC didn't already. Similarly, although Grothendieck universes do add some strength to ZFC, they don't add very much (as measured by the large cardinal hierarchy, see ). So if you're comfortable with the consistency of ZFC, then (a) you're comfortable with the consistency of NBG and (b) you shouldn't be too uncomfortable about the consistency of Grothendieck universes.

• As to whether these stronger foundations are true - well, that gets into deeper waters. (For one thing, how do you know ZFC itself is "true," and what does "true" mean in this context, anyways?) I'm a formalist (usually), so I don't tend to spend too much time with this question, but there are plenty of places where the truth of large cardinals is defended. (As for NBG + global choice, I'm actually not aware of any strong partisans for its truth over mere NBG.)

This is all leaving aside the question of whether the passage to stronger foundations is even necessary for "ordinary" mathematics, even "ordinary" category theory - I believe the answer is a strong "no," but someone more knowledgeable should address that.

---

You'll notice that I have a pragmatic attitude towards foundations - "use what works." In general, I think that even ZFC is not to be taken for granted. In my opinion, all theorems that need any "real" set theory (don't ask me to define that :P) should be viewed in the context of the set theory used to prove them. Here there's no difference for me between, say, Borel determinacy, which can be proved in ZFC, but not much less(!), and the result you quote, which can be proved in ZFC + a bit more, but not ZFC alone. If I'm in a context where we're assuming a background theory strong enough to prove them, I can breezily say that they're true - but if I'm being really careful, I should at least tell you some natural sufficient axioms. We might disagree about the truth of those axioms - and hence about the truth of the theorems - but we won't disagree about the purely formal claim, "Such-and-such axioms prove such-and-such theorem."

Answer 2

The choice-free statement of the cited theorem is as follows:

If $F : \mathcal{C} \to \mathcal{D}$ is fully faithful and constructively essentially surjective on objects, i.e. there exist a map $G : \operatorname{ob} \mathcal{D} \to \operatorname{ob} \mathcal{C}$ and a map $\epsilon : \operatorname{ob} \mathcal{D} \to \operatorname{mor} \mathcal{D}$ such that each $\epsilon (D)$ is an isomorphism $F (G (D)) \to D$, then $F : \mathcal{C} \to \mathcal{D}$ is (half of) an equivalence of categories.

In the absence of choice, the hypotheses are strictly stronger, but they are often satisfied in practice – for example, $F$ might be the restriction of an adjunction, or something like that. There are similar problems with the definition of "complete category" etc. The trouble with giving constructively correct versions of all these general definitions and theorems is that it would just obscure the essential idea without much payoff. Thus, for clarity and convenience, we assume the axiom of (global) choice, universes, etc.

Incidentally, there is also a way to fix the naïve version of the cited theorem by changing the definition of "functor" – specifically, we could work with anafunctors instead of functors. This is related to the idea of formally inverting weak equivalences. I think you will agree that it is not at all helpful to introduce anafunctors to beginners in category theory.