The traditional theory of topological spaces (as formalized by Bourbaki) starts with a set of points, then builds a structure on that. In contrast, the theory of locales starts with a frame of opens (open subspaces), identifying the points (if these are even needed) from that data. I once read something suggesting that we should do both: start with both a set of points and a frame of opens, then specify the relation between these. This was pretty speculative (and probably also being done constructively, but I'm not sure about that). Is there a developed theory of this, or at least a name that I can look up or ask about?
To give this question some mathematical weight, I'm going to write down some definitions of the sort of thing that I'm thinking of. Nevertheless, if you have an answer to the previous paragraph that disagrees in some details with what follows, then this is still an answer to my question! (But if it's nothing at all like what follows, then it's probably not what I'm looking for.)
A space $X$ consists of a set $|X|$ (the set of points of $X$), a frame $\mathcal{O}_X$ (the frame of opens of $X$), and a frame homomorphism from $\mathcal{O}_X$ to the power set $\mathcal{P}|X|$ of $|X|$. (I'm provocatively claiming the generic term ‘space’ because I hope that somebody will say that the proper term is _____ as found in _____'s paper _____, which would be a perfect answer to this question.)
As a function to a power set may be reinterpreted as a binary relation, so the frame homomorphism from $\mathcal{O}_X$ to $\mathcal{P}|X|$ may be reinterpreted in a more elementary way as a binary relation $\in_X$ between $|X|$ and (the underlying set of) $\mathcal{O}_X$ with these properties:
- for each point $a$ of $X$, $a \in_X \top_{\mathcal{O}_X}$;
- for each point $a$, open $U$, and open $V$ of $X$, $a \in_X U \wedge V$ iff $a \in_X U$ and $a \in_X V$; and
- for each point $a$ and collection $\mathcal{U}$ of opens of $X$, $a \in_X \bigvee \mathcal{U}$ iff, for some $V \in \mathcal{U}$, $a \in_X V$.
Given a space $X$ and a space $Y$, a (continuous) map $f$ from $X$ to $Y$ consists of a function $|f|$ from $|X|$ to $|Y|$ and a frame homomorphism $f^*$ from $\mathcal{O}_Y$ to $\mathcal{O}_X$ that makes the diagram $$ \matrix { \mathcal{O}_Y & \overset{f^*}\to & \mathcal{O}_X \\ \downarrow & & \downarrow \\ \mathcal{P}|Y| & \underset{|f|^{-1}}\to & \mathcal{P}|X| } $$ commute. Or in more elementary terms:
- for each point $a$ of $X$ and open $U$ of $Y$, $a \in_X f^*(U)$ iff $|f|(a) \in_Y U$.
Spaces and maps form a category $\mathrm{Sp}$.
A space $X$ is topological if the frame homomorphism from $\mathcal{O}_X$ to $\mathcal{P}|X|$ is monic. In elementary terms:
- for each open $U$ and open $V$ of $X$, if for each point $a$ of $X$, $a \in_X U$ iff $a \in_X V$, then $U = V$.
(It follows that $U \leq V$ iff $a \in_X U$ implies $a \in_X V$. Note that $a \in_X V$ if $a \in_X U \leq V$ in any space $X$.) The topological spaces (see what I did there?) form a full subcategory $\mathrm{Top}\,\mathrm{Sp}$ of $\mathrm{Sp}$. A subset $G$ of $|X|$ is open if it is in the image of the frame homomorphism from $\mathcal{O}_X$. In this way, every space gives rise to a topological space in the usual sense, and indeed we get a functor from $\mathrm{Sp}$ to the category of such spaces and the continuous functions between them. When restricted to $\mathrm{Top}\,\mathrm{Sp}$, this is an equivalence of categories.
A space $X$ is localic if the points of $\mathcal{O}_X$ (in the locale-theoretic sense) correspond to the points of $X$. Explictly:
- for each completely prime filter $\mathcal{F}$ in $\mathcal{O}_X$, for some unique point $a$ of $X$, for each open $U$ of $X$, $U \in \mathcal{F}$ iff $a \in_X U$.
(It follows that $U = V$ iff they have the same points. Note that in any space $X$, a point of $X$ defines a completely prime filter in this way, but we want all such filters to arise in this way and that different points generate different filters.) The localic spaces form a full subcategory $\mathrm{Loc}\,\mathrm{Sp}$ of $\mathrm{Sp}$. As $\mathcal{O}_X$ is a frame, every space gives rise to a locale, and indeed we get a functor from $\mathrm{Sp}$ to the usual category of locales. When restricted to $\mathrm{Loc}\,\mathrm{Sp}$, this is an equivalence of categories.
A space is sober if it is both topological and localic. The sober spaces form a full subcategory $\mathrm{Sob}\,\mathrm{Sp}$ of $\mathrm{Sp}$, which is thus equivalent both to the category of sober topological spaces in the usual sense and to the category of topological (aka spatial) locales.
