2
$\begingroup$

Is there a Grothendieck topos $F$ such that, for any Grothendieck topos $E$, the category of geometric morphisms $$E\rightarrow F$$ is equivalent to the category of locales internal to $F$?


I suspect that such an $F$ doesn't exist, because the definition of locale doesn't look to me like it can be formalised as a geometric theory. But it would be nice if there was such a classifying space, since the locales internal to a topos are interesting objects. In particular, if $X$ is a locale then the locales internal to $\mathrm{Sh}(X)$ correspond bijectively with bundles over $X$, i.e. pairs $(Y,f)$ where $Y$ is a locale and $f:Y\to X$.

$\endgroup$
  • 1
    $\begingroup$ Excellent question. I too suspect that such an $F$ doesn't exist. If you're satisfied with essential surjectivity instead of equivalence, and if you're okay with switching to the dual category, then I can propose a substitute: the classifying topos of frame presentations. Every frame arises from a frame presentation, though not uniquely so. Details in frame presentations are for instance in a fine paper by Steve Vickers on the double powerlocale, Section 5, there called GRD system and cast in the language of geometric logic. $\endgroup$ – Ingo Blechschmidt Sep 28 '18 at 8:04
  • $\begingroup$ @IngoBlechschmidt The following occurred to me, I guess it must be well known. The internal locales do respect pullback: if $E\to F$ is a geometric morphism then we get a canonical functor from the category of locales internal to F to the category of locales internal to E. In other words we have a functor $\mathrm{Locale}:\mathbf{Topos}^\text{op}\to\mathbf{Cat}$. $\endgroup$ – Oscar Cunningham Oct 3 '18 at 11:09
  • $\begingroup$ @IngoBlechschmidt But $\mathbf{Topos}^\text{op}\to\mathbf{Cat}$ is the free cocompletion of $\mathbf{Topos}$, and $\mathbf{Topos}$ is already cocomplete. So there should be some sort of canonical "geometriztation" of $\mathrm{Locale}$ achieved by applying the functor $(\mathbf{Topos}^\text{op}\to\mathbf{Cat})\to\mathbf{Topos}$. Can we describe what this is? $\endgroup$ – Oscar Cunningham Oct 3 '18 at 11:09
  • $\begingroup$ Maybe there are size issues... $\endgroup$ – Oscar Cunningham Oct 4 '18 at 10:43
  • $\begingroup$ Ah, I see. The problem is that since $\mathbf{Topos}$ is large, it's free small-cocompletion isn't $\mathbf{Topos}^\text{op}\to\mathbf{Cat}$. $\endgroup$ – Oscar Cunningham Oct 5 '18 at 14:36
2
$\begingroup$

Points of a topos are always accessible, the categories of frames or locales are not.

$\endgroup$
  • $\begingroup$ That sounds right, but could you give a sketch proof or reference? $\endgroup$ – Oscar Cunningham Oct 7 '18 at 12:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.