nLab sublocale




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.

Sublocales can also be defined for formal topologies.


There are multiple equivalent ways to formally define this concept.

In terms of regular monomorphisms of locales

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.

Equivalently, a sublocale of LL can be described as a morphism of frames LSL\to S whose underlying map of sets is surjective.

In terms of subsets of opens

Given a regular monomorphism i:SLi\colon S\to L, it induces an adjunction f *f *f^*\dashv f_* between the underlying posets. The direct image map

f *:SLf_*: S\to L

is an injection on underlying sets such that if we equip its image f *(S)f_*(S) with the induced order, it becomes a locale itself, and the inclusion f *(S)Lf_*(S)\to L is a localic map, i.e., it has a left adjoint that preserves finite meets.

Thus, sublocales of LL can be defined as subsets SS of LL such that SS is a locale once we equip it with the order induced from LL, and the left adjoint to the inclusion SLS\to L exists and preserves finite meets. (Proposition 2.2 in Picado and Pultr.)

(The inclusion SLS\to L need not preserve joins, so in particular, the lattice structure on SS may be different from that of LL, only the ordering is the same.)

Equivalently, sublocales of LL can also be described (2.1) as subsets SS of LL that are closed under all meets and for any sSs\in S and xLx\in L, we have (xs)S(x\to s)\in S.

Equivalence of these two definitions

Given a surjective morphism of frames h:LSh\colon L\to S, the subset h *(S)h_*(S) is a sublocale of LL.

Given a subset SS of a locale LL that is a sublocale, the left adjoint j *:LSj^*\colon L\to S to the inclusion j *:SLj_*\colon S\to L is a surjective morphism of frames.

In terms of nuclei

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.

Equivalence of nuclei and other definitions

Given a nucleus jj on a frame LL, we construct a congruence on LL given by the equivalence relation EE consisting of all pairs (x,y)(x,y) (x,yLx,y\in L) such that j(x)=j(y)j(x)=j(y). The quotient map LL/EL\to L/E is a surjective morphism of frames.

Vice versa, given a congruence EE on LL, define j(x)= y:(x,y)Eyj(x)=\bigvee_{y\colon (x,y)\in E}y. Then jj is the nucleus corresponding to the sublocale LL/EL\to L/E.

Given a nucleus jj, we can restrict its codomain to its set-theoretical image, obtaining a surjective morphism of frames Lj(L)L\to j(L).

Vice versa, given a surjective morphism of frames h *:LSh^*\colon L\to S, the composition h *h *:LLh_* h^*\colon L\to L is a nucleus on LL.

Given a nucleus j:LLj\colon L\to L, the subset j(L)j(L) is a sublocale.

Vice versa, given a subset SLS\subset L that is a sublocale, the corresponding nucleus j:LLj\colon L\to L is given by the formula j(a)={sSas}j(a)=\bigwedge\{s\in S\mid a\le s\}.

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 points of LL.)

Relation to topological subspaces

The underlying locale of a topological space will typically have many sublocales that are not spatial, i.e., do not come from any topological space.

However, any subset SS of a topological space XX can be equipped with the induced topology, which turns it into a subspace, whose underlying locale is a sublocale of Ω(X)\Omega(X). This can be most easily seen in the language of surjective morphisms of frames, since open sets in the induced topology are by definition intersections of SS and an open subset of XX.

Thus, we have a canonical map from the set of (topological) subspaces of XX to the set of spatial sublocales of ΩX\Omega X.

This map is a bijection if XX satisfies the separation axiom T DT_D, e.g., is a Hausdorff space (VI.1.2 in PP).

This map is a surjection if XX is a sober space (Proposition VI.2.2.1 in PP).


Last revised on May 23, 2023 at 22:58:02. See the history of this page for a list of all contributions to it.