Locale Basics

22 May 2022 - Tags: locale-basics

This quarter I’ve been running a reading group for some undergraduates on pointless topology. I want to take some time to write down a summary of the basics of locales (which are the object of study of pointless topology), both so that my students can have a reference for what we’ve covered, and also because I think there’s still space for a really elementary presentation of some of these topics, with a focus on concrete examples.

In particular, it took me a long time to find examples of how people actually build a locale (that doesn’t obviously come from a geometric theory). Hopefully this post will help fill that gap! In the near future, I’d like to write a follow-up post about how we can build new locales from old ones too, but that’s a problem for another day.

Enough build up, though! Let’s get to it ^_^

---

Our first few weeks were a crash course on the kind of category theory that I usually assume my readers know already, with a focus on partial orders and lattices¹. After spending time getting to adjoint functors, we defined a topological space, and then observed that the lattice of open sets has a certain algebraic structure:

• Opens are closed under finite intersection
• Opens are closed under arbitrary union

We quickly abstracted this into a definition²:

Now, inspired by the fact that continuous maps of topological spaces $(X,\tau) \to (Y,\sigma)$ are in bijection with frame homomorphisms from $\sigma \to \tau$, we define the category of Locales to be opposite the category of frames.

Of course, there’s no sense in having a definition without examples!

---

Geometric Examples

The first important class of examples are the “geometric” ones. Every topological space⁴ is specified in terms of either a base or a subbase, and we can imitate these constructions exactly in the world of locales.

Let’s do the real numbers to start. These have a basic open for each interval $(a,b)$. Classically we can take all such intervals, but constructively it’s more hygienic to take only the intervals with rational endpoints. Obviously these generate the same topology, so we’re not losing anything by doing this.

Now, the intervals $(a,b)$ form a meet semilattice where we define

\[(a,b) \wedge (a', b') = (\max(a,a'), \min(b,b'))\]

with the convention that $(a,b) = \bot$ whenever $b \lt a$.

This is telling us that our open intervals really are a basis in the strong sense that the intersection of two basic opens is basic open.

From here, we want to define a topology by declaring an open set to be an arbitrary union of the basic opens. In the locale-theoretic world, we take this meet-semilattice and (freely) close it under arbitrary joins!

To do that, we recall the adjunction

where (as usual) $U$ is the forgetful functor and $\mathcal{D}$ is the downset functor, which sends a poset $P$ to the free (sup)lattice $\mathcal{D} P$ whose elements are the downwards-closed subsets of $P$⁵. The unit of this adjunction sends $p \in P$ to \(\downarrow \! p = \{ x \in P \mid x \leq p \}\).

Then, at the end of the day, we can define the locale $\mathbb{R}$ to be generated by the basic opens $(a,b)$ with $a \lt b \in \mathbb{Q}$. These assemble into a meet-semilattice $P$, and the downset lattice $\mathcal{D} P$ is a frame.

Of course, there’s nothing special about $\mathbb{R}$ here!

Given any meet-semilattice of basic open sets⁶ $(M, \wedge)$, the downsets $\mathcal{D}M$ form a locale where every open is the union of basic opens in $m$ (here, as usual, we identify $m \in M$ with the principal downset \(\downarrow \! m \in \mathcal{D}M\)).

Edit: Thanks to Graham Manuell from the CT Zulip for catching a small bug here! It’s not enough to take the downset lattice of intervals. We also need to quotient to make sure $\bigvee_{n} \left (a + \frac{1}{n}, b - \frac{1}{n} \right ) = (a,b)$, for instance. More generally we say that the join of all intervals contained in $(a,b)$ should be $(a,b)$ itself. This is actually a special case of a Coverage, which we’ll discuss more later on!

---

For another example of building locales from a geometric space, let’s build $S^1$ together! We have a few options for how to do this.

In practice, we use the fact that $S^1$ as a topological space is hausdorff, thus sober. Then we appeal to an important theorem⁷ that the full subcategory of sober topological spaces is equivalent to the full subcategory of “spatial locales”.

In particular, the usual topology on $S^1$, viewed as a frame, gives a locale for $S^1$ with no changes necessary.

If we need to, though, we can also build $S^1$ by hand. After all, we can describe the open arcs and their intersections as basic opens, then take downsets just as we did for $\mathbb{R}$.

However, it would be nice if we could somehow define $S^1$ to be $\mathbb{R} / \mathbb{Z}$. I’ve never actually seen anybody talk about how to do this, so this blog post seems like a perfect place!

If $\mathbb{Z}$ is acting on $\mathbb{R}$ by translation, that means we have an action of $\mathbb{Z}$ on the frame of opens of $\mathbb{R}$, where a basic open $(p,q)$ pulls back to the basic open $(p-1,q-1)$.

Since locales are dual to frames, a quotient locale (that is, an epimorphism) should correspond to a subframe (that is, a monomorphism), and a moment’s meditation on the quotient topology shows that we want to consider the sublocale of open sets fixed by the $\mathbb{Z}$ action. So a typical open in this sublocale looks like

\[\bigvee_{n \in \mathbb{Z}} (p-n, q-n)\]

Intuitively, we’re identifying an open set of $S^1$ with its preimage in $\mathbb{R}$, which lets us identify the frame of opens of $S^1$ with a subframe of the opens of $\mathbb{R}$.

---

But what, I hear you asking, if our basic opens are just basic in the usual sense? For instance, how can we describe a locale associated to a general metric space?

The answer, dear reader, is Sites⁸.

Johnstone (in section II.2.11 of Stone Spaces) requires his sites to be meet semilattices, but this is still not as general as I would like⁹. After all, the open balls in a metric space are very rarely closed under intersection! It took me a surprisingly long time to find a satisfying construction, but Vickers (in Compactness in Locales and in Formal Topology) gives the following definition, which does exactly what I want:

Then the frame presented by a flat site is

\[\mathcal{D}P \Bigg / p \leq \bigvee A \text{ (for every $p \vartriangleleft A$)}\]

That is, we we force the coverage relation $p \vartriangleleft A$ to become an actual covering in the frame¹⁰.

---

Logical Examples

Of course, locale theory (like most of my interests) has a dual nature as a geometirc subject and a logical subject. The previous section was about locales which arise from geometric objects, but what about locales arising logically?

Let’s start with the notion of a (propositional) geometric theory.

There is a sequent calculus for geometric logic, which, for those in the know, is exactly what you expect¹¹. All that we need to know is that it lets us derive the truth of certain sequents in a way that formally mirrors the way we prove things as mathematicians. For instance, one can derive the sequent $\varphi \land \psi \vdash \psi \land \varphi$, which tells us that $\land$ is commutative.

This is important because the language¹² \(L(\{ P_\alpha \})\) is a preorder if we define $\varphi \leq \psi$ by $\varphi \vdash \psi$. Intuitively, elements “higher up the poset” are “more true”, with $\top$ and $\bot$ as the top and bottom elements.

If we then quotient by the equivalence relation of $x \leq y \leq x$ (so we consider two provably-equivalent formulas to be “the same”) then we get a frame, where the lattice operations are given by the logical ones¹³! In fact, this construction gives the free frame generated by the set ${ P_\alpha }$ of primitive propositions.

Now, given a theory $\mathcal{T}$ with primitive propositions ${ P_\alpha }$, we define the Lindenbaum Algebra $\mathcal{L}[\mathbb{T}]$ to be the frame of formulas in ${ P_\alpha }$ modulo the relations

\[\varphi_1, \ldots, \varphi_n \leq \psi\]

for each $\big ( \varphi_1 \ldots, \varphi_n \vdash \psi \big ) \in \mathbb{T}$.

This is again a frame, which we should think of as the formulas in \(L(\{P_\alpha\})\) up to provable equivalence, where now we may use the sequents in $\mathbb{T}$ as axioms in our proofs¹⁴! In the case we view this frame as a locale, we call it the Classifying Locale of $\mathbb{T}$.

This was all very abstract, so let’s see some concrete examples:

---

Let $X$ be a set, and consider a theory $\mathbb{T}$ with one primitive proposition $\sigma_{x,y}$ for each $x,y \in X$, and axioms

\[\begin{align} \top &\vdash \bigvee_{y \in X} \sigma_{x,y} &&\text{(for each $x \in X$)} \\ \sigma_{x,y}, \sigma_{x,z} &\vdash \bot && \text{(for $y \neq z \in X$)} \\ \sigma_{x,y} &\vdash \sigma_{y,x} \end{align}\]

What’s the use of this theory? Well recall a (classical) model of a (propositional) theory $\mathbb{T}$ is exactly a frame homomorphism \(\mathcal{L}[\mathbb{T}] \to \{ \bot, \top \}\).

Now, a model of this theory assigns each $\sigma_{x,y}$ to $\bot$ or $\top$, thus a model is really picking out a subset of $X \times X$ – namely those pairs $(x,y)$ so that $\sigma_{x,y} = \top$.

Through this lens, the first two axioms express that for every $x$, there is exactly one $y$ with $\sigma_{x,y} = \top$, so that our model is naming a function (which I’ll call $f_\sigma : X \to X$). The last axiom is asserting that $f_\sigma(x) = y$ implies $f_\sigma(y) = x$. That is, $f_\sigma$ should be an involution!

So (classical) models of $\mathbb{T}$ are exactly $\mathbb{Z}/2$ actions on $X$.

We can push this further, though!

Consider a theory $\mathbb{T}$ with primitive propositions $\theta_{n,x}$ for $n \in \mathbb{N}$ and $x \in \mathbb{R}$, and the axioms

\[\begin{align} \top &\vdash \bigvee_{x \in \mathbb{R}} \theta_{n,x} && \text{(for each $n \in \mathbb{N}$)} \\ \theta_{n,x}, \theta_{n,y} &\vdash \bot && \text{(for $x \neq y \in \mathbb{R}$)} \\ \top &\vdash \bigvee_{n \in \mathbb{N}} \theta_{n,x} && \text{(for each $x \in \mathbb{R}$)} \end{align}\]

---

The locales $\mathcal{L}[\mathbb{T}]$ are surprisingly flexible. For instance, say $B$ is a seminormed space. Then we can describe its (localic) dual space by considering a geometric theory with primitive propositions “$\varphi(a) \in (r,s)$” for each $a \in B$, $r,s \in \mathbb{Q}$. These should satisfy axioms:

\[\begin{align} \top &\vdash \varphi(0) \in (r,s) && \text{(for $r \lt 0 \lt s$)} \\ \varphi(0) \in (r,s) &\vdash \bot && \text{(otherwise)} \\ \varphi(a) \in (r,s) &\vdash \varphi(-a) \in (-s,-r) \\ \varphi(a) \in (r,s) &\vdash \varphi(ta) \in (tr, ts) && \text{(for $t > 0 \in \mathbb{Q}$)} \\ \varphi(a) \in (r,s), \varphi(a') \in (r',s') &\vdash \varphi(a + a') \in (r+r', s+s') \\ \varphi(a) \in (r,s) &\vdash \varphi(a) \in (r,s') \lor \varphi(a) \in (r', s) && \text{(whenever $r \lt r' \lt s' \lt s$)} \\ \top &\vdash \varphi(a) \in (-1,1) && \text{(whenever $\lVert a \rVert \lt 1$)} \\ \varphi(a) \in (r,s) &\vdash \bigvee_{r \lt r' \lt s' \lt s} \varphi(a) \in (r',s') \\ \bigvee_{r \lt r' \lt s' \lt s} \varphi(a) \in (r',s') &\vdash \varphi(a) \in (r,s) \end{align}\]

Then a (classical) model of this theory is exactly the graph of a norm-decreasing linear functional on $B$! Moreover, if we use this formulation of the dual space of $B$, we can get a completely constructive proof of the Hahn-Banach theorem¹⁵!

---

Now, we’ve said that this is a very flexible appraoch for building locales… but just how flexible is it?

Well, it turns out that every locale arises in this way! That is, for each locale $L$, there is a geometric theory which it classifies¹⁶.

As our primitive propositions, we’ll take the elements $U_\alpha \in L$ (viewed as a frame). Then our theory will be exactly the “cayley table” of $L$. As axioms, we’ll take \(U_1 \wedge U_2 \vdash U_3\) whenever $U_3$ is the meet of $U_1$ and $U_2$ in $L$. Similarly, we’ll add axioms saying that \(\bigvee U_\alpha \vdash U^*\) whenever $U^*$ really is the join of the $U_\alpha$ as computed in $L$.

Now, tautologically, it’s clear that the lindenbaum algebra for this theory is $L$, as desired.

---

Points

You’ve probably heard locale theory referred to as “pointless topology” (especially since I called it that at the start of the post!). But what does that mean?

Well, in topological spaces, we can identify points of $X$ with maps \(\{ \star \} \to X\), since these maps are completely determined by the point $f(\star) \in X$ (and conversely, every point determines a map).

Then we perform a tried and true maneuver, used by mathematicians everywhere: we take a theorem in the old setting, and turn it into a definition in our new setting! So for us, a Point of a locale $L$ is a continuous map $1 \to L$, where $1$, the terminal locale, is the one point space (that is, the locale whose frame of opens is \(\{ \bot, \top \}\))

Now we get to one of the most important punchlines in locale theory!

If you recall, the lattice \(\{\bot, \top\}\) showed up before too… We saw that frame homomorphisms \(\mathcal{L}[\mathbb{T}] \to \{\bot, \top\}\) were exactly classical models of the theory $\mathbb{T}$!

But turning the arrows around, we see that (classical) models of $\mathbb{T}$ are nothing but points of $\mathcal{L}[\mathbb{T}]$!

In this way, we can view $\mathcal{L}[\mathbb{T}]$ as the “space of models” of $\mathbb{T}$. Of course, some theories don’t have any classical models: for instance, the theory of surjections \(\mathbb{N} \to \mathbb{R}\) that we built earlier. In this case, our locale has no points! But nonetheless it has nontrivial topological structure.

One way to see that this nontrivial structure is interesting is by considering more general kinds of point. For instance, instead of assigning each primitive proposition the value $\bot$ or $\top$, you might assign them values in some other frame $F$. These “$F$-valued models” are interesting already, but they really shine when we see the analogue in topos theory¹⁷.

Again, though, we dualize, and for a locale $X$ we say that the “$X$-valued points of $L$” (equivalently the $X$-valued models of $\mathbb{T}$) are exactly the continuous maps $X \to L$ (equivalently $X \to \mathcal{L}[\mathbb{T}]$).

---

So now we have two different ways of thinking about a continuous map $f : X \to Y$. The first way is just what it is: a continuous map.

But logically, we know that we can think of these as $\mathbb{T}$ models in a world with more than two truth values. Is there some geometric interpretation of this idea?

The answer is “yes”!

For each point $p : 1 \to X$, we get a map $fp : 1 \to Y$. So then we might think of $f$ as giving us points in $Y$ which vary continuously in $X$. That is, “points” $p_x$ of $Y$ which continuously depend on a parameter from $x$. This seems like a kind of silly thing to do, but it turns out to be a very useful way of thinking.

But there’s another, third way of viewing a map $f : X \to Y$ – namely as a bundle. For each point $y$ of $Y$ we get a pullback

here $X_y = f^{-1}(y)$ is a locale (since the category of locales is complete), and we think of $X$ as being a family of locales $X_y$ which varies continuously in $Y$. This is another very fruitful idea which I’ll probably talk about in a future blog post¹⁸.

---

Ok, this was a long one, but I think there’s a lot to say about frames and locales. I’m surprised how difficult it is to find concrete examples of certain calculations on frames, and ways of building them (though maybe I’m just not sure where to look). Either way, I hope my students find this a useful (if somewhat fleshed out) review of the localic material we’ve covered so far, and I hope that future readers find this an approachable introduction to the basics of locale theory.

Take care, everyone, and I’ll see you soon ^_^

---

PS: I’ve been reading a lot of locale theory lately, particularly while looking for references that showcase either explicit constructions or interesting use cases. I usually include references either in the text or in footnotes, but I’ll actually include a short bibliography here for the papers that I found particularly insightful:

• Anel, Mathieu, and André Joyal. “Topo-Logie.” In New Spaces in Mathematics, edited by Mathieu Anel and Gabriel Catren, 1st ed., 155–257. Cambridge University Press, 2021. https://doi.org/10.1017/9781108854429.007.
• Banaschewski, Bernhard, and Christopher J. Mulvey. “A Constructive Proof of the Stone-Weierstrass Theorem.” Journal of Pure and Applied Algebra 116, no. 1 (March 28, 1997): 25–40. https://doi.org/10.1016/S0022-4049(96)00160-0.
• ———. “A Globalisation of the Gelfand Duality Theorem.” Annals of Pure and Applied Logic 137, no. 1 (January 1, 2006): 62–103. https://doi.org/10.1016/j.apal.2005.05.018.
• Blechschmidt, Ingo. “Generalized Spaces for Constructive Algebra.” ArXiv:2012.13850 [Math], December 26, 2020. http://arxiv.org/abs/2012.13850.
• Borceux, Francis. Categories of Sheaves. Digitally printed version. Handbook of Categorical Algebra / Francis Borceux 3. Cambridge: Cambridge Univ. Press, 2008.
• Chen, Xiangdong. “On Binary Coproducts of Frames,” n.d., 14.
• Day, B. J. “Locale Geometry.” Pacific Journal of Mathematics 83, no. 2 (August 1, 1979): 333–39. https://doi.org/10.2140/pjm.1979.83.333.
• He, Wei, and MaoKang Luo. “Completely Regular Proper Reflection of Locales over a given Locale.” Proceedings of the American Mathematical Society 141, no. 2 (June 5, 2012): 403–8. https://doi.org/10.1090/S0002-9939-2012-11329-2.
• Isbell, John. “Product Spaces in Locales.” Proceedings of the American Mathematical Society 81, no. 1 (1981): 116–18. https://doi.org/10.2307/2044000.
• ———. “Atomless Parts of Spaces.” MATHEMATICA SCANDINAVICA 31 (June 1, 1972): 5. https://doi.org/10.7146/math.scand.a-11409.
• Johnstone, Peter T. Stone Spaces. Paperback ed., Repr. Cambridge Studies in Advanced Mathematics 3. Cambridge: Cambridge Univ. Press, 1992.
• Pelletier, Joan Wick. “Locales in Functional Analysis.” Journal of Pure and Applied Algebra 70, no. 1 (March 15, 1991): 133–45. https://doi.org/10.1016/0022-4049(91)90013-R.
• Picado, Jorge, and Aleš Pultr. Frames and Locales: Topology without Points. Frontiers in Mathematics. Basel: Birkhäuser, 2012.
• ———. “Notes on the Product of Locales.” Mathematica Slovaca 65, no. 2 (April 1, 2015): 247–64. https://doi.org/10.1515/ms-2015-0020.
• Vickers, Steven. “Geometric Logic in Computer Science.” In Theory and Formal Methods 1993, edited by Geoffrey Burn, Simon Gay, and Mark Ryan, 37–54. Workshops in Computing. London: Springer London, 1993. https://doi.org/10.1007/978-1-4471-3503-6_4.
• ———. “Compactness in Locales and in Formal Topology.” Annals of Pure and Applied Logic 137, no. 1–3 (January 2006): 413–38. https://doi.org/10.1016/j.apal.2005.05.028.
• ———. “Continuity and Geometric Logic.” Journal of Applied Logic, Logic Categories Semantics, 12, no. 1 (March 1, 2014): 14–27. https://doi.org/10.1016/j.jal.2013.07.004.

---