Info on the locale of surjections from the Natural Numbers to the Real Numbers 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.
 A: Disclaimer: I'm not completely sure what I've done is the correct way to go about it, since I wasn't able to find whatever the nlab's source was, but the idea seems reasonable and this question deserves an answer. If someone comes by who knows better comes along, please feel free to correct me.
The usual trick when struggling with contradictory properties of functions is to study the poset of partial functions. The problem is that it's not clear what it means for a partial function to be surjective. The key idea is to use locale theory itself.
A function from $\mathbb{N}$ to $\mathbb{R}$ can be thought of as a continuous map of topological spaces, where $\mathbb{N}$ has the discrete topology. Thus a "surjection" from $\mathbb{N}$ to $\mathbb{R}$ is a continuous "surjection".
Using locales, these "surjections" correspond to injective maps of frames $\mathcal{O}(\mathbb{R}) \rightarrow \mathcal{P}(\mathbb{N})$.
None of these "injections" exist either. But the point is that we are now able to consider partial functions: it makes a lot more sense to ask for a partial function to be injective than it does to ask for it to be surjective. We are therefore now able to define the locale of surjections.
The objects of the locale of surjections are injective maps of frames from some subframe of $\mathcal{O}(\mathbb{R})$ to $\mathcal{P}(\mathbb{N})$. Nontrivial such maps exist: for example, for any open set $U$ of $\mathbb{R}$ there are many maps of frames with domain $\{\bot < U < \top \}$. All that needs to be done now is to understand the ordering of these elements and confirm that it is a frame.
Edit: There's also almost certainly some order reversal going on here: i.e. the locale of surjections has the opposite order of the order given by the partial functions.
The way to see this is to consider the case where the sets are chosen so that there are surjections. In that case a total map of frames (i.e. a maximal element of the poset of partial maps) corresponds to a single given surjection (a minimal element in the poset of sets of surjections).
A: 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.
