# Combination topological space and locale?

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_X \in U$$ and $$a_X \in 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 $$|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 $$x \in_X V$$ if $$x \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 locales with enough points.

• These can be interpreted as Chu spaces: en.m.wikipedia.org/wiki/Chu_space – Qiaochu Yuan Sep 26 '19 at 0:49
• This is reminiscient of the work of Sambin and Maietti on their "basic picture". E.g. here – Bas Spitters Sep 26 '19 at 7:00
• @QiaochuYuan : True, and I guess that Chu spaces are called spaces because of how TopSp appears as a subcategory of Chu(Set,2). But a Chu space has only a set of opens/states, not a frame of opens, so I've never seen these as really having much to do with topology. – Toby Bartels Sep 27 '19 at 17:28
• @BasSpitters : Yes; they start with only a structure of basic opens rather than an entire frame of opens, but that's only to be expected, since they want to be predicative. And I think that they also begin with only a set of basic points, too; for example, one might construct the real line starting with just the set of rational numbers (which also helps to be predicative). But if we remove the predicativity and construct the set of all points and the frame of all opens, then isn't this supposed to end up just being a locale? (or a localic space, in the terminology of my question). – Toby Bartels Sep 27 '19 at 17:32