Consider a normal first course on category theory (say up to and including the statement and proof) of the adjoint functor theorem (AFT). What are the minimal assumptions for the definition of a set one needs to make in order that everything works? As far as I understand, up to and including the AFT there is very little one needs besides that fact that sets should have elements and that we have avoided Russell's paradox. So what is a minimal set of axioms allowing this to work?
$\begingroup$
$\endgroup$
17
-
3$\begingroup$ Is an underlying notion of set necessarily required at all? For example, do we need one in order to work with Grp, the category of groups? It doesn't seem so to me, but I'm not a professional mathematician. $\endgroup$– Alexis HazellAug 3, 2021 at 13:37
-
3$\begingroup$ Minimal assumptions is a big ask. But I think Mac Lane set theory + one weak universe should suffice. Mac Lane set theory + one universe is definitely enough. $\endgroup$– Zhen LinAug 3, 2021 at 13:52
-
9$\begingroup$ You can do category theory to your heart's desire even with Russell's paradox. In fact, it gets a lot easier. $\endgroup$– Andrej BauerAug 3, 2021 at 14:33
-
3$\begingroup$ Tim, @Andrej is jesting. If you theory is inconsistent, you can prove anything. $\endgroup$– Asaf Karagila ♦Aug 3, 2021 at 16:33
-
4$\begingroup$ @AndrejBauer Harder to publish though. :P $\endgroup$– Noah SchweberAug 3, 2021 at 18:39
|
Show 12 more comments
2 Answers
$\begingroup$
$\endgroup$
10
To complement Tom Leinster's answer, let me try to be specific:
To form the product category $\mathcal{C} \times \mathcal{D}$, we need ordered pairs, which we can get from the axiom of unordered pairs.
It's probably a good idea to have the empty set $\emptyset$, so that the initial category exists.
My experience from type theory leads me to believe that we want function extensionality, or else we cannot reasonably work with functors and natural transformations (which are functions). Function extensionalty is equivalent to set-theoretic extensionalty.
To form the hom-set $\mathrm{Hom}(A,B) = \{f \in \mathcal{C}_1 \mid \mathrm{dom}(f) = A \land \mathrm{cod}(f) = B\}$ we seemingly need bounded separation. It's a little more difficult to see whether we need unbounded separation (my guess would be that we can work pretty nicely without it).
To form functor categories, we need powersets. Indeed, given any set $A$, its powerset may be generated as the set of objects of the functor category $2^A$, where $2$ is the discrete category on two objects.
There are two functors form the terminal category $\mathbf{1}$ to the arrow category $\bullet \to \bullet$. If we think their coequalizer exists (in the category of small categories) then we believe in the axiom of infinity, because the coequalier is the monoid of natural numbers.
I am pretty sure the axiom of choice and excluded middle are not needed for general category theory, and foundation also seems quite irrelevant. How about union and replacement?
answered Aug 3, 2021 at 21:21
-
2$\begingroup$ Is there an elaboration of your point 6. available anywhere? (Preferably one for the categorically-challenged...) $\endgroup$ Aug 4, 2021 at 2:07
-
$\begingroup$ @AlexArvanitakis: which bit is not clear? The statement, how to get its proof, or both? It's one of those category-theoretic facts that are more easily verified than looked up, once you're hear about them. $\endgroup$ Aug 4, 2021 at 8:39
-
1$\begingroup$ Here is an outline proof for (6). The monoid $\mathbb{N}_0$ is a category with one object and one arrow for each $n \in \mathbb{N}_0$. The required coequalizer in the category of categories is, by definition, a category $C$, together with a functor $N : (a \rightarrow b) \rightarrow C$. Since the two functors $F_a$, $F_b$ from $\bullet$ to $(a \rightarrow b)$ satisfy $NF_a = NF_b$, we have $N(a) = N(b)$. Let $c = N(a) = N(b) \in C$. Then $Nf : c \rightarrow c$ is a morphism. It doesn't have to be the identity, nor does any power of it. So $C$ has the monoid $\mathbb{N}_0$ as a subcategory. $\endgroup$ Aug 4, 2021 at 9:41
-
1$\begingroup$ Usin @MarkWildon's notation, let $\mathbf{N}$ be the category with only object $*$ and morphisms natural numbers, composed by addition. Let $Q : (a \to b) \to \mathbf{N}$ be the functor sending $a \to b$ to $1 : * \to *$. We claim it's a coequalier. Given any functor $R : (a \to b) \to C$ which equalizes $F_a$ and $F_b$, it factors through $Q$ via $T : \mathbf{N} \to C$, defined by $T(*) = R(a) = R(b)$ and $T(n) = R(a \to b)^n$. The factorization is unique because it must take the generating morphism $1 : * \to *$ to $R(a \to b)$. $\endgroup$ Aug 4, 2021 at 9:57
-
4$\begingroup$ Doesn't a "normal first course" also need choice? (I take the quoted words to exclude courses based on HoTT, anafunctors, etc.) Apart from "full & faithful & ess surj on objs $\implies$ equivalence", consider adjunctions. Given a functor $G: B \to A$ such that each comma cat $a \downarrow G$ has an initial object, we want to deduce that $G$ has a left adjoint. How do you do that without choice? $\endgroup$ Aug 4, 2021 at 11:43
$\begingroup$
$\endgroup$
5
You ask what assumptions on sets are needed in a "normal first course on category theory". There are several possible kinds of answer, and this is an answer of the practical kind, i.e. from the empirical and pedagogical point of view. It's based on having assisted with the teaching of such courses by multiple other people, and having delivered such courses many times myself (though it's not for me to say whether my courses were "normal" :-) ). And, for that matter, having once upon a time been a student in a first course on category theory.
In all these courses, as far as I remember, no assumptions on sets were ever stated at all. The definition of category was given without mentioning sets. Some vague word such as "collection" may have been used, or perhaps the definition began "a category consists of objects...", or maybe the word "class" came into it (but in an informal way too).
At some point, there will have been some declaration such as "we make a naive distinction between small categories, in which the collection of all maps is a set, and large categories, where they don't". As you say, that's needed before one gets to the adjoint functor theorems. And there will have been some similarly phrased definition of locally small category, which is needed in order to state the Yoneda lemma. The definitions of small and locally small do rely on a notion of set, but in the courses I'm thinking of, no axioms on sets were stated. Just as in a course on representation theory or differential geometry or more or less anything else, students were simply assumed to know how sets behaved.
One can discuss whether this approach is good or bad. I'm not making a case here. I'm just stating the empirical fact that this is how category theory is often taught, and that generations of students have successfully learned category theory this way. In that sense, no assumptions on sets are needed. But as I said, there are other possible kinds of answer, for different interpretations of your question.
answered Aug 3, 2021 at 19:15
-
$\begingroup$ Ok, but implicitly you relied on things like: the ability to form ordered pairs, function extensionality (two maps are equal if they have equal values), to form a hom-set you probably need exponential sets or some such. Things which are probably not needed: replacement, choice, foundation, infinity, and let me throw in excluded middle for good measure. $\endgroup$ Aug 3, 2021 at 20:50
-
3$\begingroup$ For sure, yeah. The question wasn't very precise and I chose to interpret it the way I did, but there's at least one other answer of the kind you're saying. One thing that's clear from experience, though, is that no kind of axiomatic set theory is needed in order to successfully learn category theory. Most of my students haven't known any. $\endgroup$ Aug 3, 2021 at 21:00
-
2$\begingroup$ By the way, there is one mega-use of choice that probably appears in most first courses on category theory (as you know well, Andrej): the proof that a functor that's full, faithful and essentially surjective on objects is an equivalence. $\endgroup$ Aug 3, 2021 at 21:03
-
2$\begingroup$ Yeah, I hate that theorem. Except in HoTT, where it holds without choice by magic. $\endgroup$ Aug 3, 2021 at 21:23
-
3$\begingroup$ @AndrejBauer that why Makkai wrote Avoiding the axiom of choice in general category theory $\endgroup$– David Roberts ♦Aug 4, 2021 at 1:41