You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I guess this is a pretty naïve question, but I'm wondering how the choice of set-theoretic foundations interacts with reasoning about the category .
In particular, if I didn't want to assume the axiom of choice, is there a way to just define a category , distinct from the category ? If so, can still use the axiom of choice when reasoning about the category ?
My guess is that I can't really do that, because there should be no statement I can make about that I can't also make about . So really they're the same category, it's just that I can say more about it in one case than in the other. But this is just a vague intuition, and I want to know if it can be pinned down a bit more precisely.
I guess the way I'd think about it is that you have two meta-theories: one with choice and one without. And the category of sets (defined the same way) behaves differently in each of these meta-theories. But there are probably other ways to think about it (two-level theories, etc.).
This is one of the things that one can do with topos theory. There are many toposes where the axiom of choice fails to hold internally, and these are like categories of sets without choice; we can do topos theory over any base topos by using only meta-theoretic principles valid in that topos. Deligne's completeness theorem is a result which uses reasoning about sites in the category of SetsWithChoice to deduce that all locally coherent toposes have enough points, but this is implicitly a result about "locally coherent toposes over the topos of SetsWithChoice", which when relativised to other toposes can fail to hold.
If you work in a foundational theory that includes the axiom of choice, like ZFC, then the category of sets will satisfy choice. If you work in a foundational theory that doesn't include the axiom of choice, like ZF, then the category of sets will not satisfy choice. (Once you fix your foundational theory, there is only one "category of sets".) You'll be able to prove strictly more in the former case, just because ZFC is ZF plus an extra axiom, and adding an extra axiom always means you can prove more.
However, as Morgan said, even once you fix your foundational theory, there are lots of categories that are like the category of sets in many ways, and this relates to forcing and independence proofs in set theory that are generally phrased instead as constructing models of the cumulative hierarchy. For instance, if your foundational theory is ZFC, then using categories of group actions (what set theorists call a "permutation model") you can construct a category that is like the category of sets but doesn't satisfy choice. And if your foundational theory is ZF, then the category of sets and functions in Godel's constructible universe L is like the category of sets but does satisfy choice.
This was the same question I was thinking about when I asked Is there a universal way to force the Axiom of Choice to be true?