Category Theory
Zulip Server
Archive

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.


Stream: learning: questions

Topic: Axiom of choice


view this post on Zulip Nathaniel Virgo (Dec 27 2022 at 03:30):

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 Set\mathbf{Set}.

In particular, if I didn't want to assume the axiom of choice, is there a way to just define a category SetsWithoutChoice\textbf{SetsWithoutChoice}, distinct from the category SetsWithChoice\textbf{SetsWithChoice}? If so, can still use the axiom of choice when reasoning about the category SetsWithoutChoice\textbf{SetsWithoutChoice}?

My guess is that I can't really do that, because there should be no statement I can make about SetsWithoutChoice\textbf{SetsWithoutChoice} that I can't also make about SetsWithChoice\textbf{SetsWithChoice}. 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.

view this post on Zulip Sam Speight (Dec 27 2022 at 10:15):

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.).

view this post on Zulip Morgan Rogers (he/him) (Dec 27 2022 at 15:38):

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.

view this post on Zulip Mike Shulman (Dec 28 2022 at 18:48):

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.

view this post on Zulip Mike Shulman (Dec 28 2022 at 18:51):

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.

view this post on Zulip Oscar Cunningham (Dec 28 2022 at 22:28):

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?