A locale is a structure which captures the relations between possible observations. This fact is an important insight into why topological spaces show up so often when thinking about artificial intelligence. In particular, this gives us to key to understanding why computable functions are continuous.

They are very similar to topological spaces -- the open sets of any topology form a locale. However, they have better properties than topologies in many contexts. For example, they're easier to work with when constructive math is required. See Peter Johnstone's The point of pointless topology for an overview of these benefits.

Why locales?

Locales model observations, and thus turn up in a very wide variety of contexts. In particular, they model affirmable observations - observations which, if true, can be affirmed by a witness. For example, "Some crows are black" is an affirmable observation, since we could affirm it by the existence of a black crow. On the other hand, "All crows are black" is not an affirmable observation. The locale is a system of affirmable observations which we call opens. ^[1]

Observations can have more or less information. This gives them a poset structure. We say that the more specific open refines the more generic open. To say refines $B$ , we write $A \leq B$ . A witness affirming $A$ will also affirm $B$ .

Observations can be combined to make a higher information observation. We call this combination the meet of our observations, and write it as $⋀ A_{i}$ or $A \land B$ . Think of this as $A$ and $B$ . If incompatible observations are combined, we get the bottom element of the poset: $⊥$ -- representing false. We can only combine a finite number of observations -- that's because we are modeling observations that can be computably affirmed, we can't really observe something if it takes an infinite amount of time to observe it.

Observations can cover an arbitrary set of observations as specific possibilities. We call this the join of our opens, and write it as $⋁ A_{i}$ or $A \lor B$ . Think of this as $A$ or $B$ . Together with finite meets, this gives the locale a lattice structure. The top element of the poset $⊤$ represents true, and is the most generic observation. We can observe the join of an infinite number of opens because to affirm this join, we only need to have a witness from one of the opens in the join.

Joins and meets must be compatible with each other. In particular, they must satisfy the distributive law: $A \land ⋁ A_{i} = ⋁ (A \land A_{i})$ . Again, this is modeling the natural logic of how combining information from observations works.

So are locales the one right way to model observations?

There are some ontological commitments that locales make: that the order of observations doesn't matter, and that observations don't affect the world. Quantales generalize locales to remove these commitments! Are quantales the one right way? Well, it's hard to notice what other commitments we might be implicitly making. Also, quantales are a lot harder to work with, which means we try to avoid using them if we don't need them. In general, there isn't a single right way to model something -- it depends a lot on what exactly you're trying to do with it.

Points

Observations represent the kinds of information we can have about where something is. A point is then an exact place where something can be. In a topological space, observations correspond to sets of points, but in a locale, we can be more flexible. We also don't have to worry about points that have no possible observations that can distinguish them. ^[2]

If a locale has enough points so that we can define the opens as sets of points, we say the locale is spatial. Typically, the locales we are interested in will be spatial.

Category perspective

A poset can be considered as a category, the elements are the objects, and the order relation defines the morphisms: $A \leq B$ implies there's a morphism $A \to B$ . The meet is then the product, and the join is the coproduct! Initial object of course is $⊥$ , and final object is $⊤$ . Morphisms can also be interpreted as logical implication!

Locales themselves can be the object of a category. In fact, they are the objects of multiple important categories!

Morphisms

What is a morphism of locales? Let's think about this in terms of observations. Say we have locales $A$ and $B$ , and a computable process $f$ which takes points in $A$ to points in $B$ . ^[3]

For concreteness, say that $A$ is a locale representing the space in a glass slide, $B$ is a locale representing a computer monitor, and $f$ is a microscope which can look at the slide and project its view to the monitor.

An observation which we make on the monitor gives us (via $f$ the microscope) an observation on the slide. More generally, we can map opens of $B$ to opens of $A$ .

Now consider what happens if combine a set $S$ of opens on $B$ . We don't expect our computable process to effect how the observations combine. So in other words, we expect $f (\lor S) = \lor f (S)$ , and if $S$ is finite, $f (\land S) = \land f (S)$ .

We call a morphism $f : A \to B$ satisfying these properties a continuous map. If our locales are spatial, this corresponds exactly to a continuous function between topological spaces!

Examples

The locale of real numbers

Opens are generated by rational intervals.

More examples

The 3D space that we live in

The open sets of any topology

Logical propositions

Important concepts

Sublocale

Separation
- Regularity is the most natural separation axiom, not Hausdorff (which can be defined for locales)

Compactness

Fundamental groupoid
- Much intuitively clearer to define and use!

How do we use them?

Conceptual clarity

I've found that replacing topological spaces with locales typically brings about conceptual clarity when working on something. This effect seems to be stronger the less obvious it is to make the replacement. Topological spaces bring lots of baggage with them, with all the sets and the axiom of choice. Once these have been dropped, it becomes easier to see what's actually going on, to move! Think of this as analogous to replacing Roman numerals with Arabic numerals - it's not really that you can do anything that you couldn't do before, it just becomes significantly easier to do things!

Constructive analysis

The real line always felt like such a complicated thing to drag into the laws of physics; there must be something better! In order to do physics with that something, we'd better be able to do analysis. Luckily, locales are very promising in this regard!

Heine-Borel

Constructive Tychonoff!

References

Topology via Logic by Stephen Vickers

Stone Spaces by Peter Johnstone

Locale - nLab

^{^︎}
The example "All crows are black" is however a refutable observation, since the existence of a white crow would refute it. Refutable observations are called closeds, and are also a part of the locale structure. We incorporate them by identifying them with their negations, which are affirmative!
^{^︎}
i.e. locales are automatically $T_{0}$ separated.
^{^︎}
The locales don't need to be spatial for this to work, but it's easier to motivate the definition if we can reference points.