A locale is, intuitively, like a topological space that may or may not have enough points (or even any points at all). It contains things we call open subspaces but there may or may not be enough points to distinguish between open subspaces. An open subspace in a locale can be regarded as conveying a bounded amount of information about the (hypothetical) points that it contains.
For example, there is a locale of all surjections from natural numbers (thought of as forming the discrete space ) to real numbers (forming the real line ). This locale has no points, since there are no such surjections, but it contains many nontrivial open subspaces; these open subspaces are generated by a family parametrised by and ; the basic open associated to and may be described as .
Every topological space can be regarded as a locale (with some lost information if the space is not sober). The locales arising this way are the topological or spatial locales. Conversely, every locale induces a topology on its set of points, but sometimes a great deal of information is lost; in particular, there are many different locales whose set of points is empty.
One motivation for locales is that since they take the notion of open subspace as basic, with the points (if any) being a derived notion, they are exactly what is needed to define sheaves. The notion of sheaf on a topological space only refers to the open subspaces, rather than the points, so it carries over word-for-word to a definition of sheaves on locales. Moreover, passage from locales to their toposes of sheaves is a full and faithful functor, unlike for topological spaces.
Another advantage of locales is that they are better-behaved than topological spaces in alternative foundations of mathematics, including mathematics without the axiom of choice, more generally constructive mathematics, or mathematics internal to an arbitrary topos. For example, constructively the topological space need not be compact, but the locale is always compact (in a suitable sense). It follows that the locale , and hence also the locale of real numbers, is not necessarily spatial. When it fails to be spatial, because there are “not enough real numbers,” the locale or real numbers is generally a better-behaved object than the topological space of real numbers.
Note: By the adjoint functor theorem (AFT) for posets, a frame also has all meets (at least assuming that it is a small set, or more generally that we allow impredicative quantification over it), but a frame homomorphism need not preserve them. Similarly, by the AFT, a frame is automatically a Heyting algebra, but again a frame homomorphism need not preserve the Heyting implication.
That is, a locale “is” a frame, which we often write as and call “the frame of open subspaces of ”, and a continuous map of locales is a frame homomorphism . If you think of a frame as an algebraic structure (a lattice satisfying a completeness condition), then this is an example of the duality of space and quantity.
It is also possible to think of a continuous map as a map of posets : a function that preserves all meets (and therefore is monotone and has a left adjoint ) and such that the left adjoint preserves all finite meets. This has the arrow pointing in the “right” direction, at the cost of a less direct definition. (In predicative mathematics, we must explicitly add into this definition that has a left adjoint; compare the definition of geometric morphism one level up.)
This category is naturally enhanced to a 2-category:
(See for instance Johnstone, C1.4, p. 514.)
Given a locale , the elements of the frame are traditionally thought of as being the open subspaces of and are therefore called the opens (or open subspaces, open parts, or open sublocales) of . However, one may equally well view them as the closed subspaces of and call them the closeds (or closed subspaces, closed parts, or closed sublocales) of . When viewed as closed subspaces, the opposite containment relation is used; thus is the frame of opens of , while the opposite poset is the coframe of closeds of .
An open subspace may be thought of as a potentially verifiable property of a hypothetical point of the space . Thus we may verify the intersection of two open subspaces by verifying both properties, and we may verify the union of any family of open subspaces by verifying at least one of them; but it may not necessarily make sense to verify the intersection of infinitely many open subspaces, because this would require us to do an infinite amount of work. (The meet of an arbitrary family of open subspaces does exist, but the construction is impredicative, and it does not match the meet within the lattice of all subspaces.)
Dually, a closed subspace may be thought of as a potentially refutable property. Thus we may refute the union of two closed subspaces by refuting both of them, and we may refute the intersection of any family of closed subspaces by refuting at least one of them; but it may not necessarily make sense to refute the union of infinitely many closed subspaces. (Again, the join of an arbitrary family of closed subspaces does not work right.)
If one views an element of as a subspace of , one usually means to view it as an open subspace, but we have seen that one may also view it as a closed subspace. This is given by two different maps (one covariant and a frame homomorphism, one contravariant and a coframe homomorphism) from to the lattice of all subspaces of . See sublocale for further discussion.
As a locale, the abstract point is the locale whose frame of opens is the frame of truth values (classically ). This is the terminal object in , since we must have (for ) and (and most generally , since ).
Given a locale , a concrete point of may be defined in any of the following equivalent ways:
Definition (3) is simpler than (2), being an element of satisfying a finitary condition rather than a subset of satisfying an infinitary condition. However, it doesn't work in constructive mathematics, which provides much (but by no means all) of the motivation for studying locales.
See localic geometric morphism for more.
This appears as Johnstone, theorem C1.6.3.
For every morphism of locales the sheaf topos is equivalent as a topos over to the topos of internal sheaves over the internal locale
This appears as Johnstone, scholium C1.6.4.
Every topological space has a frame of opens , and therefore gives rise to a locale . For every continuous function between topological spaces, the inverse image map is a frame homomorphism, so induces a continuous map of locales. Thus we have a functor
Conversely, if is any locale, we define a point of to be a continuous map . Here is the terminal locale, which can be defined as the locale corresponding to the terminal space. Explicitly, we have , the powerset of (the initial frame, the set of truth values, which is classically or in a Boolean topos). Since a frame homomorphism is determined by the preimage of (the true truth value), a point can also be described more explicitly as a completely prime filter: an upwards-closed subset of such that ( denotes the top element of ), if then , and if then for some .
The elements of induce a topology on the set of points of in an obvious way, thereby giving rise to a topological space . Any continuous map of locales induces a continuous map of spaces, so we have another functor
One finds that is left adjoint to .
In fact, this is an idempotent adjunction:
A locale with is called spatial or topological; one also says that it has enough points.
This appears for instance as (MacLaneMoerdijk, corollary IX.3 4).
Consequently, we often identify a sober topological space and the corresponding topological locale.
The analogous result for toposes involves a bit of set theory: under ZFC plus the existence of a strong inaccessible cardinal , the foundational assumption of MacLane in Categories for the Working Mathematician, call a category moderate if its set of morphisms has size . For example, is moderate.
These results emphasize frames/toposes as algebras, where the morphisms are left exact left adjoints. The right adjoints to such morphisms are called geometric morphisms, and emphasize locales/toposes as spaces. This analogy, which plays an important but mostly tacit role in Joyal and Tierney, can be developed further along the following lines.
See for instance (MacLaneMoerdijk, section 5).
For a locale, write
This appears for instance as MacLaneMoerdijk, section IX.5 prop 2.
The functor has a left adjoint
This appears for instance as MacLaneMoerdijk, section IX.5 prop 3.
The functor here is also called localic reflection.
In fact this is even a genuine full sub-2-category:
This appears as (Johnstone, prop. C1.4.5).
A monomorphism of sheaves is a natural transformation that is degreewise a monomorphism of sets (an injection). Therefore the subobjects of the terminal sheaf (that assigns the singleton set to every object) are precisely the sheaves of this form.
We may think of a frame as a Grothendieck (0,1)-topos. Then localic reflection is reflection of Grothendieck toposes onto -toposes and is given by -truncation: for a locale, the corresponding localic topos and any Grothendieck topos we have a natural equivalence
An introduction to and survey of the use of locales instead of topological spaces (“pointless topology”) is in
This is, in its own words, to be read as the trailer for the book
Other dedicated textbooks are
where the latter develops topology from the point of view of its internal logic.
An introductory survey is
Plenty of material is also in part C (volume 2) of
Locales are also discussed in section IX.1 of
Lex totality is the subject of an article of Street,
The connection between locales and toposes via lex totality plays a tacit role throughout the influential monograph