Skip to main content
3 of 13
added 4 characters in body
Ivan Di Liberti
  • 9.1k
  • 1
  • 27
  • 66

Simon essentially answered the question already, but I will expand some of the parts that may not be clear to the experts. Sketches of an elephant is a good reference for everything I am going to say.

Def (Prebounds). Let $\mathcal{E}$ be a topos. A prebound $e \in \mathcal{E}$ is an object such that the subobjects of its finite powers $m: a \to e^n$ are a generator for the topos. Such an object always exist and can be obtained by manipulating a generator (or a site).

Construction (From prebounds to localic geometric morphisms). Given a couple $(\mathcal{E},e)$ where $\mathcal{E}$ is a topos and $e$ is a prebound, we can construct a localic geometric morphism $$f_e: \mathcal{E} \to \text{Set}[\mathbb{O}]. $$ Of course, this is the same of a cocontinuous left exact functor $f_e^*: \text{Set}[\mathbb{O}] \to \mathcal{E}$, which is the same of a lex functor $\text{Fin}^\circ \to \mathcal{E}$. The latter, is given by sending $n \mapsto e^n$. The geometric morphism obtained in this way is localic by definition of prebound. This construction appeared for the first time in Freyd's All topoi are localic.

Remark. If you think about it, I am just spelling out in categorical terms what Simon suggested in somewhat mystical language.

Remark (Morita-like phenomena). Notice that each prebound (and we can construct a prebound from any site) gives a different localic morphism, thus we have many localic representation for the same topos!

Theorem (Internal locales are localic geometric morphisms). There is a biequivalence of categories between the $2$-category of internal locales in $\text{Loc}(\text{Set}[\mathbb{O}])$ and the $2$-category of localic geometric morphisms over $\text{Set}[\mathbb{O}]$, $$\text{Loc}(\text{Set}[\mathbb{O}]) \leftrightarrows \text{Topoi}_{\text{loc} / \text{Set}[\mathbb{O}]}. $$

Proof. Lemma 1.2 in Johnstone, Factorization theorems for geometric morphisms. Cahiers, 22, no1 (1981)

Def (Well presented topoi). The $2$-category WTopoi of well presented topoi has objects $(\mathcal{E},e)$ where $\mathcal{E}$ is a topos and $e$ is a prebound and morphism geometric morphisms whose left adjoint preserve the prebuound.

Remark. This notion does not appear in the literature (to my knowledge), I just need it as an intermediate notion. A good intuition for it is that the topos is specified together with a precise language generator of the geometric theory it classifies.

Remark (Every topos can be well presented). Of course, the WTopoi is not the same of Topoi but the forgetful functor $$\mathsf{U}: \text{WTopoi} \to \text{Topoi} $$ is essentially surjective on objectd and on morphisms (!).

Theorem (Internal locales are well presented topoi and vice versa). There is a biequivalence of categories $$\text{Loc}(\text{Set}[\mathbb{O}]) \leftrightarrows \text{Topoi}_{\text{loc} / \text{Set}[\mathbb{O}]} \leftrightarrows \text{WTopoi}.$$

Ivan Di Liberti
  • 9.1k
  • 1
  • 27
  • 66