11
$\begingroup$

What is a reference for "the equivalence between geometric theories and frames internal to the free topos"? [1] This seems to be an extremely interesting theorem.

[1] André Joyal, “A crash course in topos theory: the big picture”, lectures at Topos à l'IHÉS, 2015.

$\endgroup$
1

2 Answers 2

11
$\begingroup$

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. I will take a bit of a different narrative to Simon's, implicitly assuming a good understanding of classifying topoi, blurring the distinction between a topos and the geometric theory it classifies, $$\mathcal{E} \simeq \text{Set}[\mathbb{T}] .$$

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}$,

$$\text{Topoi}(\mathcal{E}, \text{Set}[\mathbb{O}]) \simeq \text{Cocontlex}( \text{Set}[\mathbb{O}], \mathcal{E}) \simeq \text{Cocontlex}( \text{Set}^{\text{Fin}}, \mathcal{E})\simeq \text{Lex}(\text{Fin}^\circ, \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!

Remark (Topoi are geometric theories, generators are their presentation). Following Thm 2.1.1 in Caramello's Theories, Sites, Toposes, we see that a generator, or a site, is essentially the same of a linguistic presentation of the geometric theory classified by the topos.

Theorem (Internal locales are localic geometric morphisms). There is a biequivalence of categories between the $2$-category of internal locales in $\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)

Remark (On the emergence of Lawvere-like doctrines). When one spells out what a locale internal to $ \text{Set}[\mathbb{O}]$ is, one discovers that it is nothing but a functor $$\mathbb{P}: \text{Fin} \to \text{Frames}$$ verifying the Beck-Chevalley condition and Frobenius reciprocity (see Lemma C.1.6.9 and Cor. C.1.6.10 in Sketches of an Elephant). Suddenly we see how doctrine-like objects emerge in the representation of theories! That's beautiful in my opinion. $\text{Fin}$ acts as a fact as a set of variables, while $\mathbb{P}(n)$ gives us the poset (a frame in fact) of formulas on those $n$-variables.

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. WTopoi is really much more a $2$-category of sites, together with a relational notion of morphism of sites, rather than a $2$-category of topoi.

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 objects, 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}.$$

$\endgroup$
20
  • 1
    $\begingroup$ @DavidRoberts I was thinking about Grothendieck topoi the whole time. $\endgroup$ Commented Feb 9, 2022 at 11:51
  • 2
    $\begingroup$ Similarly, you are asking for a proof of Morely categoricity theorem in Model theory, but you want it to be completely elementary and not mentioning saturated models and Lachlan's theorem? I mean, it's not in-accessible, but "One does not simply walk into Mordor". $\endgroup$ Commented Feb 9, 2022 at 13:01
  • 1
    $\begingroup$ Firstly, I didn't ask about Hahn-Banach. Secondly, prebounds don't occur in the statement I asked about. Thirdly, you don't need to know about Banach spaces to state and prove the Hahn-Banach theorem. I really don't get your analogy. $\endgroup$ Commented Feb 9, 2022 at 13:02
  • 2
    $\begingroup$ The forgetful functor Topoi $\to \text{Cat}^\text{op}$ is representable and has a left adjoint. Set$[\mathbb{O}]$ is the free object on $1$. $\endgroup$ Commented Feb 9, 2022 at 13:42
  • 2
    $\begingroup$ @IvanDiLiberti I just want to say thanks again for all your help and sorry that I was a bit overwhelmed at first. I will come back to your answer again and again as I keep learning more topos theory! $\endgroup$ Commented Feb 9, 2022 at 16:21
10
$\begingroup$

When you think about it the right way the idea is fairly simple :

Here the "Free topos" means the "object classifier", that is the classifying topos of the theory with just one sort (one type) and no axioms. A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want (so in particular, you can emulate function symbol using functional relations).

So frames in the free topos corresponds exactly to one-sorted geometric theory (with propositions and functions). In practice any geometric theory is (Morita) equivalent to a one-sorted one, so you can describe any theory like this. But the presentation as a frame in the free topos depends on what you chose as this sort.

I do not know a reference that present things exactly this way. But if you look in P.T.Johnstone Sketches of an elephant, you should find a good approximation to it as Theorem D3.2.5. The theorem might not be exactly what you are after, but it contains all the key elements. (Also using that localic geometric morphisms corresponds to internal frames of course)

$\endgroup$
11
  • $\begingroup$ Why is it appropriate to call the object classifier the "free topos"? (I know that usually that refers to Lambek's initial elementary topos.) $\endgroup$ Commented Feb 9, 2022 at 12:39
  • $\begingroup$ "A Frame in this topos hence corresponds to a purely propositional geometric theory on top of this theory with one sort and no axiom, so you end-up with exactly a geometric theory with a single sort and as many propositions and geometric axioms as you want" - Can you explain that? I don't understand the "hence". What you are claiming is exactly the theorem I ask about. $\endgroup$ Commented Feb 9, 2022 at 12:42
  • 1
    $\begingroup$ @IvanDiLiberti I don't understand your answer. $\endgroup$ Commented Feb 9, 2022 at 12:53
  • 3
    $\begingroup$ @user1022117 The part of th D3.2.5 you want is the equivalence between $T$ classifies a one sorted geometric theory (with generic model B) and the morphism $ T \to Set[O]$ corresponding to $B$ is localic. You then have to combined this with the fact that localic geometric morphism $ E \to T$ corresponds to internal frame in $T$. (Ivan gave a reference for this. I couldn't find a reference for this in the Elephant, except section C1.6 which deals with the case where $T$ is localic... ) $\endgroup$ Commented Feb 9, 2022 at 14:09
  • 4
    $\begingroup$ @user1022117 : I didn't "learn at the right place" either. I learned topos theory on my own (from books) when I was a PhD student. If you want to learn start from one of the classical textbooks like MacLane and Moerdijk Sheaves in geometry and logic, or volume 3 of Borceux's handbook of categorical algebra. I also like McLarty's Elementary categories, Elementary topos if you want to learn directly through the lens of internal logic. The Elephant is a very valuable resource, but it was never meant to be a textbook : It is an encyclopedia. $\endgroup$ Commented Feb 9, 2022 at 14:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .