Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Pretopos theory

John Baez (Sep 29 2026 at 11:02):

In his excellent paper with the very bland title Matrices, relations and group presentations, marred only by the use of equations where there should be string diagrams, Aurelio Carboni proves (among other things) that the opposite of the category of separable algebras in any compact closed, additive category with coequalizers is a boolean [[pretopos]].

I don't know much about pretopoi except the definition: they're extensive categories that are regular where every internal equivalence relation is a kernel pair. But the name 'pretopos' makes me want to ask: is there some standard way to turn a pretopos into a topos, and is this a useful thing to do?

Joshua Wrigley (Sep 29 2026 at 11:19):

Yes, to turn a pretopos into a (Grothendieck) topos, you take the category of sheaves with the finite coverage topology.

Joshua Wrigley (Sep 29 2026 at 11:36):

Is this a useful thing to do? Pretopoi classify theories of coherent logic, i.e. positive finitary first-order logic, up to bi-interpretability $^ \dagger$. Topoi classify geometric logic, so turning a pretopos into a topos can be understood as viewing a coherent theory as a geometric theory, and then taking the corresponding classifying topos.

To elaborate further -- morphisms between pretopoi correspond to interpretations $^ \dagger$ between theories; that is, the sorts of one theory can be interpreted as definable quotients in the second. Meanwhile, geometric morphisms correspond to geometric interpretations, where we can take definable quotients of arbitrary disjoint unions of definable sets. This means interpretations, a syntactic consideration, and semantics can be handled uniformly.

I like the following example. Let $I$ denote the theory of the singleton set, and let $T$ be any other theory. What are the interpretations of $T$ inside $I$? And now what are the geometric interpretations of $T$ inside $I$? The latter are able to express all models of $T$. Indeed, this is just saying that geometric morphisms $\mathbf{Set} \to \mathbf{Set}[T]$ to the classifying topos of $T$ correspond to set-based models of $T$.

$^ \dagger$ There is a little bit of subtlety being elided here, which effectively can be reduced to noting the difference between the exact completion and pretopos completion. For the purposes of this comment, for most theories encountered in classical logic, there is no difference, but in weaker systems there might be. See the discussion in Section 8 of this article.

John Baez (Sep 29 2026 at 12:57):

Thanks very much! Your puzzle is interesting because an interpretation of a positive finitary first-order theory $T$ in the theory $I$ of a one-element set sounds trivial: it seems like there should be at most most one way to put a $T$-structure on a 1-element set, and maybe for positive theories there's exactly one since I don't see a way to express something like "false". But then you seem to be saying the geometric interpretations of $T$ inside $I$ are geometric morphisms $\mathsf{Set}[I] = \mathsf{Set} \to \mathsf{Set}[T]$, which are set-based models of $T$ - very interesting. This makes me think I have an arrow backward when I'm saying an interpretation of a positive finitary first-order theory $T$ in the theory $I$ of a one-element set sounds trivial.

David Michael Roberts (Sep 29 2026 at 13:06):

One of my favourite pretopos is the syntactic category of ZF, so that the objects are (formulae encoding) possibly proper classes.
Another one is the category of small presheaves that arises after trying to do forcing on a large partial order that is the limit of an ORD-sequence of posets (conditions apply).
The category of condensed sets is a(n infinitary) pretopos

So to my mind, a pretopos can be "bigger" than a topos. But I wrote a blog post about the third item above, and Peter Scholze emailed me and we had a short discussion and he revealed that he thinks of a pretopos as the category of coherent objects in a Grothendieck topos, and so "smaller" than a topos.

Now I think there's a real difference between a vanilla pretopos and an infinitary pretopos, in that the former can be a small category, and the internal logic in the latter really should be stronger.

Joshua Wrigley (Sep 29 2026 at 13:15):

John Baez said:

This makes me think I have an arrow backward when I'm saying an interpretation of a positive finitary first-order theory $T$ in the theory $I$ of a one-element set sounds trivial.

No, this arrow is going in the correct direction. The point is that given a set-based model $M$ of $T$, we can construct a geometric interpretation corresponding to the model by taking the coproduct $\coprod_{x \in M} 1$.

Joshua Wrigley (Sep 29 2026 at 13:17):

David Michael Roberts said:

So to my mind, a pretopos can be "bigger" than a topos.

When I described the sheaf construction on a pretopos earlier, I was implicitly assuming that the pretopos was small, or at least small-generated. If we relax this requirement, then indeed there are more pretopoi than there are pretopoi of coherent objects in a Grothendieck topos (since the latter are small-generated by assumption).