Info on the locale of surjections from the Natural Numbers to the Real Numbers

Question

On the nlab page for locales, it states that there is locale for the surjections from the Naturals to the Reals. This locale has no points (i.e. elements), since there are no such surjections, but the locale is still nontrivial.

What are some of the properties of this locale? Where can I learn more about it? The nlab page only mentioned it in passing.

Answer 1

Ingo Blechschmidt gives a presentation of the locale in a comment on this MO question. I reproduce the comment here, almost word by word.

The locale of surjections $\mathbb N\to\mathbb R$ is freely generated by opens $U_{n,x}$ for $n\in\mathbb N$ and $x\in\mathbb R$ ($U_{n,x}$ is meant to be thought of as the open $U_{n,x}\subseteq L$ of surjections $f:\mathbb N\to\mathbb R$ with $f(n)=x$), subject to the following relations:

• for all $n\in\mathbb N$ set $$\bigvee_x U_{n,x}=\top$$ (read as: "$f(n)$ has a value"),
• for all $n\in\mathbb N$, $x,y\in\mathbb R$ set $$U_{n,x}\wedge U_{n,y}=\bot$$ whenever $x\neq y$, (read as: "$f(n)$ has a single value"),
• for all $x\in\mathbb R$ set $$\bigvee_n U_{n,x}=\top$$ for all $x\in\mathbb R$, (read as: "$f$ is surjective").

This construction can be found in Peter Johnstone's Sketches of an elephant, C1.2, example 1.2.8.