A sublocale is a subspace of a locale.

It is important to understand that, even for a topological locale XX (which can be identified with a sober topological space), most sublocales of XX are not topological. Specifically, we have an inclusion function SubTop(X)SubLoc(X)Sub Top(X) \hookrightarrow Sub Loc(X) which, while injective, is usually far from surjective.


Let LL be a locale, which (as an object) is the same as a frame.

A sublocale of LL is a regular subobject of LL in Loc, the category of locales. Equivalently, it is a regular quotient of LL in Frm, the category of frames.

A sublocale is given precisely by a nucleus on the underlying frame. This is a function jj from the opens of LL to the opens of LL satisfying the following identities:

  1. j(UV)=j(U)j(V)j(U \cap V) = j(U) \cap j(V),
  2. Uj(U)U \subseteq j(U),
  3. j(j(U))=j(U)j(j(U)) = j(U).

In other words, a sublocale of LL is given by a meet-preserving monad on its frame of opens.

The precise reasons why nuclei correspond to quotient frames (and hence to sublocales) is given at nucleus. But the interpretation of the operation jj is this: we identify two opens if they ‘agree on the sublocale’. Given an open UU, there will always be a largest open that is identified with UU, so we can also describe a subspace of a locale as an operation that maps each open to its largest representative open in the sublocale. This map is the nucleus jj.

Special cases

Of course, every locale LL is a sublocale of itself. The corresponding nucleus is given by

j L(U)U, j_L(U) \coloneqq U ,

so every open is preserved in this sublocale. Conversely, every locale has an empty sublocale, given by

j (U)L.j_\empty(U) \coloneqq L .

Suppose that UU is an open in the locale LL. Then UU defines an open subspace of LL, also denoted UU, given by

j U(V)UV, j_U(V) \coloneqq U \Rightarrow V ,

so j U(V)j_U(V) is the largest open which agrees with VV on UU. UU also defines a closed subspace of LL, denoted UU' (or any other notation for a complement), given by

j U(V)UV, j_{U'}(V) \coloneqq U \cup V ,

so j U(V)j_{U'}(V) is the largest open which agrees with VV except on UU. If LL is topological, then every open sublocale of LL is also topological; the same goes for closed sublocales, assuming excluded middle. Even in constructive mathematics, however, open and closed sublocales are complements in the lattice of sublocales.

The double negation sublocale of LL, denoted L ¬¬L_{\neg\neg}, is given by

j ¬¬(U)¬¬U. j_{\neg\neg}(U) \coloneqq \neg{\neg{U}} .

This is always a dense subspace; in fact, it is the smallest dense sublocale of LL. (As such, even when LL is topological, L ¬¬L_{\neg\neg} is rarely topological; in fact, its only points are the isolated point?s of LL.)


Revised on December 4, 2016 04:03:58 by Toby Bartels (