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: Countable unions of countable sets

Madeleine Birchfield (Feb 04 2024 at 14:39):

Without countable choice, is a countable union of countable sets still countable if all the surjections in the definition of countable set were required to be split?

Andrew Swan (Feb 04 2024 at 15:09):

No. Even with classical logic, you can countable families of sets with exactly 2 elements (so not only split but in bijection with a known set), but with no choice function.

Andrew Swan (Feb 04 2024 at 15:10):

(of course there is no canonical way to choose the bijections with 2)

Madeleine Birchfield (Feb 04 2024 at 15:23):

Andrew Swan said:

No. Even with classical logic, you can countable families of sets with exactly 2 elements (so not only split but in bijection with a known set), but with no choice function.

Does that still hold if the surjection of the index set of the union is also required to be split as well?

Madeleine Birchfield (Feb 04 2024 at 15:28):

Actually, I think it still might not hold, since the usual definition of a split surjection is mere existence of a section, rather than a choice of section.

Madeleine Birchfield (Feb 04 2024 at 15:36):

what I probably want is a completely untruncated version of the theorem, something like,

Given a set $A$ with a function $f_A:\mathbb{N} \to A$ and a choice of section $g_A:A \to \mathbb{N}$ of the function $f_A$, and given a family of sets $B(a)$ such that each $B(a)$ comes with a function $f_B(a):\mathbb{N} \to B(a)$ and a choice of section $g_B(a):B(a) \to \mathbb{N}$ of the function $f_B(a)$, one can construct a function $f:\mathbb{N} \to \bigcup_{a \in A} B(a)$ with choice of section $g:\left(\bigcup_{a \in A} B(a)\right) \to \mathbb{N}$ of the function $f$.

Andrew Swan (Feb 04 2024 at 16:28):

If there's no truncation at all then choice isn't necessary - it's just the provable "type theoretic axiom of choice." In this case there is one implicit truncation, in the definition of union, which makes it not provable, but also it's not really about countable choice. As stated, this implies that every surjection $\mathbb{N} \to X$ splits, by considering the special case where every $B(a)$ is a singleton and $f = 1_\mathbb{N}$, which implies the law of excluded middle.