History[edit]
The first approaches to topology were geometrical, where one started from Euclidean space and patched things together. But Marshall Stone's work on Stone duality in the 1930s showed that topology can be viewed from an algebraic point of view (lattice-theoretic). Apart from Stone, Henry Wallman was the first person to exploit this idea. Others continued this path till Charles Ehresmann and his student Jean Bénabou (and simultaneously others), made the next fundamental step in the late fifties. Their insights arose from the study of "topological" and "differentiable" categories.[2]
Ehresmann's approach involved using a category whose objects were complete lattices which satisfied a distributive law and whose morphisms were maps which preserved finite meets and arbitrary joins. He called such lattices "local lattices"; today they are called "frames" to avoid ambiguity with other notions in lattice theory.[3]
The theory of frames and locales in the contemporary sense was developed through the following decades (John Isbell, Peter Johnstone, Harold Simmons, Bernhard Banaschewski, Aleš Pultr, Till Plewe, Japie Vermeulen, Steve Vickers) into a lively branch of topology, with application in various fields, in particular also in theoretical computer science. For more on the history of locale theory see Johnstone's overview.[4]
Formal definitions[edit]
The basic concept is that of a frame, a complete lattice satisfying the general distributive law above. Frame homomorphisms are maps between frames that respect all joins (in particular, the least element of the lattice) and finite meets (in particular, the greatest element of the lattice). Frames, together with frame homomorphisms, form a category.
The opposite category of the category of frames is known as the category of locales. A locale is thus nothing but a frame; if we consider it as a frame, we will write it as . A locale morphism from the locale to the locale is given by a frame homomorphism .
Every topological space gives rise to a frame of open sets and thus to a locale. A locale is called spatial if it isomorphic (in the category of locales) to a locale arising from a topological space in this manner.
As mentioned above, every topological space gives rise to a frame of open sets and thus to a locale, by definition a spatial one.
Given a topological space , we can also consider the collection of its . This is a frame using as join the interior of the closure of the union, and as meet the intersection. We thus obtain another locale associated to . This locale will usually not be spatial.
regular open sets
For each and each , use a symbol and construct the free frame on these symbols, modulo the relations
The theory of locales[edit]
We have seen that we have a functor from the category of topological spaces and continuous maps to the category of locales. If we restrict this functor to the full subcategory of sober spaces, we obtain a full embedding of the category of sober spaces and continuous maps into the category of locales. In this sense, locales are generalizations of sober spaces.
It is possible to translate most concepts of point-set topology into the context of locales, and prove analogous theorems. Some important facts of classical topology depending on choice principles become choice-free (that is, constructive, which is, in particular, appealing for computer science). Thus for instance, arbitrary products of compact locales are compact constructively (this is Tychonoff's theorem in point-set topology), or completions of uniform locales are constructive. This can be useful if one works in a topos that does not have the axiom of choice.[5] Other advantages include the much better behaviour of paracompactness, with arbitrary products of paracompact locales being paracompact, which is not true for paracompact spaces, or the fact that subgroups of localic groups are always closed.
Another point where topology and locale theory diverge strongly is the concepts of subspaces versus sublocales, and density: given any collection of dense sublocales of a locale , their intersection is also dense in .[6] This leads to Isbell's density theorem: every locale has a smallest dense sublocale. These results have no equivalent in the realm of topological spaces.
