What's the point of a point-free locale?

Question

In [1, example C.1.2.8], a locale $Y$ (dense in another locale $X$) without any point is given. I fail to understand the point of such point-less locale - Why can't we identify those as the trivial locales, and what's so great about considering locales that have no points?

Anyway, here's the construction of $X$ and $Y$ (taken from [1]). Let $A$ be an uncountable nonempty set (e.g. $\mathbb{R}$) (equipped with the discrete topology), and let $X$ be the set of all functions $\mathbb{N} \to A$, equipped with the Tychonoff topology. For each $a \in A$, let $X_a$ be the subspace $\{f \in X \,|\, a \in im(f)\}$, and let $$ Y = \bigcap_{a\in A} X_{a}.$$ Now the point set $Y_p$ of $Y$ is empty because there is no onto map from $\mathbb{N}$ to $\mathbb{R}$.

In [2, section 5], Johnstone demonstrates why considering such locales could be useful. The main argument is that topoi are nice things to consider. However, at the point of writing, the (external) applications of topos theory seem lacking. Hopefully the situation has changed in mathematics in recent years. Thus the second question: How does the consideration of pointless locales help topos theory, and how does that in turn applies (externally) to mathematics?

Reference

• [1] Sketches of an Elephant: A Topos Theory Compendium [Peter T. Johnstone]

• [2] The point of pointless topology-[Peter T. Johnstone]

Answer 1

A good answer to both questions is provided by the following variant of the Gelfand duality for commutative von Neumann algebras, which shows that the following categories are equivalent:

• The category CSLEMS of compact strictly localizable enhanced measurable spaces;

• The category HStonean of hyperstonean spaces and open maps.

• The category HStoneanLoc of hyperstonean locales and open maps.

• The category MLoc of measurable locales, defined as the full subcategory of the category of locales consisting of complete Boolean algebras that admit sufficiently many continuous valuations.

• The opposite category CVNA^op of commutative von Neumann algebras, whose morphisms are normal *-homomorphisms of algebras in the opposite direction.

The first category, despite the rather complicated name, is essentially the correct category for measure theory: it incorporates equality almost everywhere, a (generalized) σ-finiteness property, and an abstract variant of the Radon measure property, which eliminate pathological measurable (and measure) spaces for which some of the most basic theorem of measure theory (such as the Riesz representation theorem or the Radon–Nikodym theorem) fail.

Of particular interest is the fourth category MLoc of mesurable locales. It is a full subcategory of the category of locales, which quite interesting: it demonstrates that both point-set general topology (as implemented by the category of topological spaces) and point-set measure theory (as implemented by the above category CSLEMS) are a part of pointfree general topology, implemented by full subcategory of the category of locales.

These parts (i.e., general topology and measure theory) are almost disjoint: locales corresponding to topological spaces are spatial, i.e., have enough points. On the other hand, points in a measurable locale are in a bijective correspondence with atoms in the original measure space. In particular, atomless measure spaces (i.e., what is typically used in practice) correspond to locales that have no points at all.

Returning to topos theory: working in the topos of sheaves of sets on a measurable locale amounts to doing ordinary mathematics in measurable families over a measurable space. For example, doing internal linear algebra in such a topos corresponds to working with measurable vector bundles, etc.