nLab essential sublocale




Essential sublocales are a generalization of locally connected sublocales.



A sublocale X jX_j of a locale XX, given by a nucleus j:π’ͺ(X)β†’π’ͺ(X)j : \mathcal{O}(X) \to \mathcal{O}(X), is called essential (sometimes also principal) if and only if the following equivalent conditions are satisfied:

  1. There is a monotone map b:π’ͺ(X)β†’π’ͺ(X)b : \mathcal{O}(X) \to \mathcal{O}(X) which is left adjoint to jj.
  2. The nucleus jj preserves arbitrary (not only finite) meets.
  3. For any u∈π’ͺ(X)u \in \mathcal{O}(X), there is a smallest v∈π’ͺ(X)v \in \mathcal{O}(X) such that uβͺ―j(v)u \preceq j(v).
  4. The pullback functor Sh(X)β†’Sh(X j)\mathrm{Sh}(X) \to \mathrm{Sh}(X_j) possesses a left adjoint (it always has a right adjoint).
  5. The geometric embedding Sh(X j)β†ͺSh(X)\mathrm{Sh}(X_j) \hookrightarrow \mathrm{Sh}(X) is an essential geometric morphism.
Proof of equivalence
  • The equivalence of (1) and (2) is by the adjoint functor theorem for complete lattices, which furthermore gives an explicit formula for the left adjoint bb, namely
    b(u)≔inf{v∈π’ͺ(X)|uβͺ―j(v)}. b(u) \coloneqq inf \{ v \in \mathcal{O}(X) \,|\, u \preceq j(v) \}.

    This also shows the equivalence of (1) and (3).

  • The equivalence of (4) and (5) is by definition.
  • Recall that the pullback of the representable sheaf Hom π’ͺ(X)(β‹…,u)Hom_{\mathcal{O}(X)}(\cdot,u) is Hom π’ͺ(X)(β‹…,j(u))Hom_{\mathcal{O}(X)}(\cdot,j(u)). Therefore continuity of the pullback functor translates to continuity of jj. This shows that (4) implies (2).
  • Conversely, assume (3). Then the explicit description of the pullback functor given below (which is valid under this assumption) shows that the pullback functor preserves arbitrary limits. By the adjoint functor theorem for Grothendieck toposes, statement (4) follows.

The left adjoint bb automatically satisfies b(u)βͺ―ub(u) \preceq u, b(b(u))=ub(b(u)) = u, j(b(u))=j(u)j(b(u)) = j(u), and b(j(u))=b(u)b(j(u)) = b(u) for all u∈π’ͺ(X)u \in \mathcal{O}(X). These relations follow from playing around with the adjunction.


  • Any open sublocale is essential: The nucleus for an open sublocale is of the form j=(uβ†’βˆ’)j = (u \rightarrow -). Its left adjoint is b=(βˆ’βˆ§u)b = (- \wedge u).

  • More generally, any locally connected sublocale is essential.


  • For a general sublocale i:X jβ†ͺXi : X_j \hookrightarrow X and a sheaf β„±\mathcal{F} on XX, the pullback i βˆ’1β„±i^{-1} \mathcal{F} is the sheafification of the presheaf u↦colim uβͺ―j(v)β„±(v)u \mapsto \colim_{u \preceq j(v)} \mathcal{F}(v). In the case that X jX_j is an essential sublocale, this presheaf is simply given by the formula u↦ℱ(b(u))u \mapsto \mathcal{F}(b(u)) and is already a sheaf, so sheafification is not necessary.

  • A sublocale of the one-point locale is essential if and only if it is open. This is because the extra Frobenius reciprocity condition demanded by openness is automatically satisfied (in classical mathematics and in impredicative constructive mathematics).

  • The lattice of essential sublocales of a given locale is complete. Suprema are calculated as in the lattice of all sublocales; infima, however, are not. There are counterexamples in (Kelly and Lawvere (1989)), however in the slightly different context of essential localizations of categories.

In the internal language

Let X jβ†ͺXX_j \hookrightarrow X be a sublocale. From the internal point of view of the topos Sh(X)Sh(X), this sublocale looks like a sublocale of the one-point locale and it’s interesting to compare the properties of X jX_j with this internal locale.


The following statements are equivalent:

  1. Sh(X)⊧X jβ†ͺ1is an essential sublocaleSh(X) \models X_j \hookrightarrow 1 \,\text{is an essential sublocale}.
  2. Sh(X)⊧X jβ†ͺ1is an open sublocaleSh(X) \models X_j \hookrightarrow 1 \,\text{is an open sublocale}.
  3. X jβ†ͺXX_j \hookrightarrow X is an open sublocale.

Note that none of these statements are equivalent to X jβ†ͺXX_j \hookrightarrow X being an essential sublocale.


Last revised on March 27, 2023 at 07:19:37. See the history of this page for a list of all contributions to it.