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 reals

Madeleine Birchfield (Feb 03 2024 at 04:35):

One and a half years ago Andrej Bauer put out a video where he says that there is a topos in which the Dedekind real numbers are countable: https://www.youtube.com/watch?v=4CBFUojXoq4

The definition of countable used in the video is that there is a surjection $\mathbb{N} \to \mathbb{R}$. But without countable choice, which is used to prove that $\mathbb{R}$ is uncountable, not every surjection out of the natural numbers has a section. Is it consistent that there is a split surjection $\mathbb{N} \to \mathbb{R}$ in constructive mathematics? Without countable choice one has to distinguish between surjections and split surjections, and I suppose between split surjections which there merely exists a section and split surjections which have a choice of section.

Madeleine Birchfield (Feb 03 2024 at 06:30):

Also, is the locale of real numbers in that topos still uncountable? There are typically more opens than points in the locale of real numbers unless the locale of real numbers is spatial.

Andrew Swan (Feb 03 2024 at 08:44):

You can show there is no split surjection $\mathbb{N} \to \mathbb{R}$ the same way you show there is no bijection. There cannot be both a surjection $\mathbb{N} \to \mathbb{R}$ and an injection $\mathbb{R} \to \mathbb{N}$. The injection is necessarily discontinuous, which lets you derive WLPO, which allows you to use one of the classical logic proofs that there is no surjection.

Morgan Rogers (he/him) (Feb 03 2024 at 09:23):

For anyone reading that isn't versed in (non-)constructive foundations, WLPO is a variant of the [[principle of omniscience]]. Does it let you do a diagonal argument @Andrew Swan or do you have to do something more subtle?

Andrew Swan (Feb 03 2024 at 12:10):

Yes, it's just a diagonal argument. E.g. WLPO gives you a decimal expansion of every natural number, so you can diagonalise against that.

Patrick Nicodemus (Feb 03 2024 at 13:04):

@James Hanson is one of the authors of this paper, maybe he can be of help

Andrew Swan (Feb 03 2024 at 13:53):

If I recall correctly you can show the points of the locale of real numbers are the Dedekind reals in fairly weak settings. Did you have proof/reference for when there are more?

Madeleine Birchfield (Feb 03 2024 at 14:49):

Andrew Swan said:

If I recall correctly you can show the points of the locale of real numbers are the Dedekind reals in fairly weak settings. Did you have proof/reference for when there are more?

By "more opens than points", I mean that there is a frame homomorphism $\mathcal{O}(\mathbb{R}) \to \mathcal{O}(\mathbb{R}_\mathrm{Loc})$
from the frame of open subsets of the set $\mathbb{R}$ of completely prime filters (i.e. Dedekind real numbers) of the locale $\mathbb{R}_\mathrm{Loc}$ to the frame of opens of the locale itself, which cannot in general be proven to be a frame isomorphism unless $\mathbb{R}_\mathrm{Loc}$ is spatial.

I probably should have said "more or equal" or something similar since there is a difference between not proving that the frame homomorphism is an isomorphism and proving that the frame homomorphism is not an isomorphism.

Madeleine Birchfield (Feb 03 2024 at 14:53):

Unless I am once again getting the direction of the arrows mixed up because locales are the opposite category of frames.

Andrew Swan (Feb 03 2024 at 15:44):

Okay, I think I see the idea, but I'm still not sure what you mean by the locale being uncountable. Are you asking if there can be an epimorphism in locales from $\mathbb{N}$ (with discrete topology) to $\mathbb{R}_{\mathrm{Loc}}$?

James Hanson (Feb 03 2024 at 16:08):

We don't really prove much about definitions of the reals other than the Dedekind reals. The Cauchy reals are still uncountable in the topos we build (and it's open whether they can be countable). It's already known that the MacNeille reals are always uncountable. This isn't in the paper, but I also came up with a constructive argument that given any sequence $(x_i)_{i \in \mathbb{N}}$ of lower real numbers, there is an upper real number $y \in [0,1]$ not equal to any of the $x_i$'s. Perhaps this tells you something about the locale?

Madeleine Birchfield (Feb 03 2024 at 16:29):

Andrew Swan said:

Okay, I think I see the idea, but I'm still not sure what you mean by the locale being uncountable. Are you asking if there can be an epimorphism in locales from $\mathbb{N}$ (with discrete topology) to $\mathbb{R}_{\mathrm{Loc}}$?

I think when I said the "locale being countable", I really meant that its frame of opens is uncountable, so really that there is a surjection $\mathbb{N}$ to $\mathcal{O}(\mathbb{R}_{\mathrm{Loc}})$.

Madeleine Birchfield (Feb 03 2024 at 16:32):

As an aside, does countable choice imply that the locale of real numbers is spatial?

Madeleine Birchfield (Feb 03 2024 at 17:02):

James Hanson said:

We don't really prove much about definitions of the reals other than the Dedekind reals. The Cauchy reals are still uncountable in the topos we build (and it's open whether they can be countable). It's already known that the MacNeille reals are always uncountable.

It's interesting, because in general, if one has a countable set $A$, it is not guaranteed that any subset $B \subseteq A$ is countable. So as of right now one would have to prove separately for each subfield $F$ of the Dedekind real numbers whether it is consistent that $F$ is countable.

Madeleine Birchfield (Feb 03 2024 at 17:29):

Alternatively, one could try to construct a topos in which every subfield $F$ of the Dedekind real numbers is countable, which would imply that it is consistent that the Cauchy real numbers, the real algebraic closure of the Cauchy real numbers, the initial Cauchy complete subfield of the Dedekind real numbers, etc are each individually countable.

Andrew Swan (Feb 03 2024 at 17:32):

For anything involving powersets it's usually easier to show uncountability. So for the case of open sets, I think you can just do this: given $f : \mathbb{N} \to \mathcal{O}(\mathbb{R}_\mathrm{Loc})$ you take $U$ to be the supremum of basic opens $(n - 1/3, n + 1/3)$ where $n \notin f(n)$. If $U = f(n)$, then we can't have either $n \in f(n)$ or $n \notin f(n)$.

Andrew Swan (Feb 03 2024 at 17:34):

Madeleine Birchfield said:

As an aside, does countable choice imply that the locale of real numbers is spatial?

The effective topos has countable choice, but $[0, 1]$ is very far from being compact, so I think that should prevent $\mathbb{R}_\mathrm{Loc}$ from being spatial. That raises the question what the internal topos on the locale of real numbers inside the effective topos looks like. I'm not sure if anyone has looked at it yet.

Morgan Rogers (he/him) (Feb 03 2024 at 17:45):

One can reach uncharted territory very quickly in topos theory :wink:

James Hanson (Feb 03 2024 at 18:21):

Andrew Swan said:

Madeleine Birchfield said:

As an aside, does countable choice imply that the locale of real numbers is spatial?

The effective topos has countable choice, but $[0, 1]$ is very far from being compact, so I think that should prevent $\mathbb{R}_\mathrm{Loc}$ from being spatial. That raises the question what the internal topos on the locale of real numbers inside the effective topos looks like. I'm not sure if anyone has looked at it yet.

A similar argument should work for the topos in our paper, although it's quite strange. There is an open cover $(U_i)_{i \in \mathbb{N}}$ with no finite subcover such that each $U_i$ is a countable union of rational open intervals, but any cover of $[0,1]$ by a sequence of rational open intervals has a finite subcover. (This isn't contradictory because countable choice fails.)

James Hanson (Feb 03 2024 at 18:24):

Madeleine Birchfield said:

Alternatively, one could try to construct a topos in which every subfield $F$ of the Dedekind real numbers is countable, which would imply that it is consistent that the Cauchy real numbers, the real algebraic closure of the Cauchy real numbers, the initial Cauchy complete subfield of the Dedekind real numbers, etc are each individually countable.

I actually suspect that you can explicitly construct an uncountable subfield of the Dedekind reals. My idea would be to build a Cantor set of pairwise algebraically independent real numbers and look at the field generated by that.

Madeleine Birchfield (Feb 03 2024 at 19:25):

James Hanson said:

I actually suspect that you can explicitly construct an uncountable subfield of the Dedekind reals. My idea would be to build a Cantor set of pairwise algebraically independent real numbers and look at the field generated by that.

Is this only in the topos that you construct in your paper, or in all possible toposes? Because that comment I made earlier was referring to the general case.

James Hanson (Feb 03 2024 at 19:27):

Madeleine Birchfield said:

James Hanson said:

I actually suspect that you can explicitly construct an uncountable subfield of the Dedekind reals. My idea would be to build a Cantor set of pairwise algebraically independent real numbers and look at the field generated by that.

Is this only in the topos that you construct in your paper, or in all possible toposes? Because that comment I made earlier was referring to the general case.

My intuition about this stuff is pretty heavily shaped by computability theory, so there's a decent chance that my idea would require Markov's principle or something, but I am envisioning it as a general construction, not something specific to the topos in our paper.