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: learning: questions

Topic: What does a slice topos classify?

finegeometer (Jun 30 2023 at 00:08):

Every Grothendieck topos classifies some geometric theory. A slice category of a Grothendieck topos is a Grothendieck topos. Therefore, for any set X, Set/X classifies some geometric theory.

What is an explicit presentation of such a theory, in terms of sorts, functions, relations, and axioms?

This feels like it should be well-known, but two search engines and the nlab have failed to provide an answer.

Max New (Jun 30 2023 at 00:13):

Well Set / X is equivalent to Set ^ X which is a presheaf category and presheaf categories classify flat functors. There's probably a further simplification

John Baez (Jun 30 2023 at 00:25):

Given a bunch of Grothendieck topoi $\mathsf{T}_i$ ($i \in X$) that are the classifying topoi for various theories, what theory is

$\prod_{i \in X} \mathsf{T}_i$

the classifying topos for? If I knew this I could answer @finegeometer's question, since

$\mathsf{Set}/X \cong \prod_{i \in X} \mathsf{Set}$

as Max pointed out, and $\mathsf{Set}$ itself is the classifying topos for "the empty theory", meaning there's just one model of this theory in any topos: $\mathsf{Set}$ is the terminal Grothendieck topos.

finegeometer (Jun 30 2023 at 00:42):

Max New said:

Well Set / X is equivalent to Set ^ X which is a presheaf category and presheaf categories classify flat functors. There's probably a further simplification

I just tried this. After significant simplification, I ended up with the following theory:

• One sort for each element of $X$.
• No function symbols or relations.
• An axiom $\top \vdash \bigvee_{x \in X} \exists x : X. \top$.
• For each $x, y \in X$, an axiom $\top \vdash_{a:x,b:y} \bigvee_{\_ : x = y} a=b$

In other words, a theory with X-many sorts, with exactly one element between them!

Maybe this example should be on the nlab somewhere, so we don't have to rederive it in the future?

John Baez (Jun 30 2023 at 00:50):

What's a model of this theory in some topos, as concretely as possible? It's got to be something very simple but I'm confused about what it is.

finegeometer (Jun 30 2023 at 00:55):

I believe all models in Set come from the following construction:

Fix $a \in X$. Let the sort associated with $x \in X$ be the subsingleton set $\{\star | x = a\}$.

John Baez (Jun 30 2023 at 01:01):

I'm having trouble understanding this. What do I need to specify to specify a model in Set, exactly?

(When $X$ has one element we know there's just one model in Set, so we don't need to specify anything to specify a model.)

John Baez (Jun 30 2023 at 01:03):

Could it be that to specify a model we just need to choose an element of $X$?

finegeometer (Jun 30 2023 at 01:03):

Exactly. There is one model in Set for each element of $X$.

finegeometer (Jun 30 2023 at 01:04):

Fixing $a \in X$, the model in question interprets the sort associated with $x \in X$ as the subsingleton set $\{\star | x = a\}$.

John Baez (Jun 30 2023 at 01:07):

Okay, good. I like to think semantically, i.e. describing theories by saying what their models are like. So if I'm not confused, I would say $\mathsf{Set}/X$ is "the classifying topos for the theory of an element of $X$", meaning that to specify a geometric morphism from some topos to $\mathsf{Set}/X$ we just choose an element of $X$. This extends the usual description of $\mathsf{Set}$ as the "theory of nothing", meaning that to specify a geometric morphism from some topos to $\mathsf{Set}$ we need to do nothing at all, since there's just one such geometric morphism.

finegeometer (Jun 30 2023 at 01:10):

I like "theory of elements of $X$". In fact that's what I was thinking before I asked the question. I just couldn't figure out how to phrase a theory with exactly one model per element of $X$!

John Baez (Jun 30 2023 at 01:11):

Okay, great. So now I can make a guess as to my more general question here:

John Baez said:

Given a bunch of Grothendieck topoi $\mathsf{T}_i$ ($i \in X$) that are the classifying topoi for various theories, what theory is

$\prod_{i \in X} \mathsf{T}_i$

the classifying topos for?

I'd guess a model of this theory is a choice of $i \in X$ and a model of theory corresponding to $T_i$.

John Baez (Jun 30 2023 at 01:12):

So e.g. we can use this trick to make up a classifying topos for the theory of "either a ring or a group".

finegeometer (Jun 30 2023 at 01:13):

That seems likely. Is $\prod_{i \in X} T_i$ a product or a coproduct in the 2-category of topoi? If so, I'm guessing that'll lead to a proof.

finegeometer (Jun 30 2023 at 01:20):

Let's see. If $\prod_{i\in X} T_i$ is to classify a choice of $i$ and a model of $T_i$'s theory, we need the category of geometric morphisms $E \to \prod_{i\in X} T_i$ to be the coproduct of the categories of geometric morphisms $E \to T_i$. Does that hold?

John Baez (Jun 30 2023 at 01:22):

This question is what was preventing me from answering your puzzle faster! I was trying to check the usual categorical product is actually the coproduct in the 2-category of topoi, geometric morphisms and natural transformations, but I was getting stuck.

John Baez (Jun 30 2023 at 01:23):

Getting stuck, even though I was allowing myself to be quite rough and sloppy.

finegeometer (Jun 30 2023 at 01:24):

https://ncatlab.org/nlab/show/Topos#Colimits looks like an answer to that, but I'm being slow to process what it's saying.

John Baez (Jun 30 2023 at 01:25):

I could see that the usual categorical product is not the product in the 2-category of topoi, geometric morphisms and natural transformations, since $\mathsf{Set}$ is terminal in that 2-category, so this would imply $\mathsf{Set}^X$ is also terminal!

John Baez (Jun 30 2023 at 01:26):

So, the usual categorical product has got to be the coproduct, by this argument: "what else could it be?" :upside_down: But that wasn't satisfying to me.

finegeometer (Jun 30 2023 at 01:28):

Let's argue by "let someone else do it", and take the answer from https://ncatlab.org/nlab/show/Topos#Colimits. I think that says $\prod_{i\in X} T_i$ is the coproduct. Now does this give us what we want?

John Baez (Jun 30 2023 at 01:35):

Yes.

John Baez (Jun 30 2023 at 01:37):

At least it gives me what I want: a semantic description of the geometric theory corresponding to the Grothendieck topos $\prod_{i \in X} \mathsf{T}_i$, meaning a description of what a model of that theory is, in any topos.

finegeometer (Jun 30 2023 at 01:38):

I'm missing something; can you spell out why this implies what a model in the theory of a product topos is?

John Baez (Jun 30 2023 at 01:39):

I'm getting confused yet again. There are a lot of "ops" running around here.

John Baez (Jun 30 2023 at 02:17):

Let's do a product of two Grothendieck topoi, $T \times T'$. Here I mean the ordinary product in Cat. But let's assume this is a coproduct in the 2-category Topos where the morphisms are geometric morphisms.

A model of the corresponding theory in a topos $X$ is a geometric morphism $X \to T \times T'$.

John Baez (Jun 30 2023 at 02:18):

Alas, assuming that $T \times T'$ is a coproduct in Topos doesn't help us much here! So I think my hopes were premature.

John Baez (Jun 30 2023 at 02:19):

Do I have any arrows accidentally reversed or products and coproducts mixed up?

finegeometer (Jun 30 2023 at 03:48):

Our conjecture is false. For instance, it would imply that $\prod_{i \in X} T_i$ has $X$-many geometric morphisms from the initial topos, when there should be only one.

John Baez (Jun 30 2023 at 03:53):

Which conjecture precisely? I've been guessing a lot of stuff here.

finegeometer (Jun 30 2023 at 03:57):

John Baez said:

Okay, great. So now I can make a guess as to my more general question here:

John Baez said:

Given a bunch of Grothendieck topoi $\mathsf{T}_i$ ($i \in X$) that are the classifying topoi for various theories, what theory is

$\prod_{i \in X} \mathsf{T}_i$

the classifying topos for?

I'd guess a model of this theory is a choice of $i \in X$ and a model of theory corresponding to $T_i$.

This conjecture.

Morgan Rogers (he/him) (Jun 30 2023 at 14:01):

John Baez said:

Okay, good. I like to think semantically, i.e. describing theories by saying what their models are like. So if I'm not confused, I would say $\mathsf{Set}/X$ is "the classifying topos for the theory of an element of $X$", meaning that to specify a geometric morphism from some topos to $\mathsf{Set}/X$ we just choose an element of $X$.

Unfortunately this is not the case, although it's true that the models in $\mathsf{Set}$ look like that!
As @Max New pointed out earlier, this classifies the theory of flat functors on $X$, where $X$ is viewed as a discrete category. What is a [[flat functor]]? Unfortunately, the nLab page is insufficiently detailed about this, but I can elaborate for you the definition of topos-valued flatness via the definition of site-valued flatness. :sweat_smile:

In this particular case, we require that $\coprod_{x \in X} F(x)$ covers the terminal object, which is what it means for the image to be inhabited. We require that for any span $F(x_1) \leftarrow Y \rightarrow F(x_2)$ there exists a covering family over $Y$ by objects of the form $F(x)$ such that there are spans $x_1 \leftarrow x \rightarrow x_2$ whose image under $F$ factor the original span. When $x_1 \neq x_2$ there are no such spans(!) so we require that the empty sieve covers $Y$, which is to say that $Y$ is initial. In other words, $F(x_1),F(x_2)$ are disjoint. Similarly, taking $x_1 = x_2$, we conclude that the projections from $F(x_1) \times F(x_1)$ must be equal, which (by a little diagram chase) means that $F(x_1)$ must be a subterminal object (i.e. an object whose unique morphism to the terminal object is a monomorphism). There is a third condition involving parallel arrows in $X$ but there are no interesting such pairs to worry about.

In summary, $\mathsf{Set}/X$ classifies the theory of $X$-indexed disjoint partitions of the terminal object.

There are other ways to figure this out / check it. A functor out of $\mathsf{Set}/X$ which preserves colimits is determined by the representables $\mathbf{y}(x)$ that @finegeometer identified, we only need to check which ones preserve finite limits. The representables are subterminal and disjoint, and both of these properties are preserved when finite limits are, which brings us pretty rapidly to the conclusion above.

John Baez (Jun 30 2023 at 15:48):

Thanks, @Morgan Rogers (he/him)! This was definitely beyond my powers of guessing, which explains why I felt so frustrated about this question. I still don't follow all the steps of your reasoning, but that's okay. I like how the models of this theory can be more interesting than models in $\mathsf{Set}$ when there are more subterminal objects.

John Baez (Jun 30 2023 at 15:50):

If I have a subterminal object in a topos T, do I get a new topos with that subterminal object as its terminal object?

Morgan Rogers (he/him) (Jun 30 2023 at 15:52):

You slice over it!

John Baez (Jun 30 2023 at 15:53):

Okay, I'll take that as a yes.

John Baez (Jun 30 2023 at 15:53):

Another question: if I have an $X$-indexed disjoint partition of the terminal object in a topos $\mathsf{T}$, do I get a bunch of topoi $\mathsf{T}_i$, one for each $i \in X$, such that

$\mathsf{T} \simeq \prod_{i \in X} \mathsf{T}_i$?

Morgan Rogers (he/him) (Jun 30 2023 at 15:54):

Sorry, my brain inserted "how" into your question

John Baez (Jun 30 2023 at 15:54):

Yes, I guessed maybe you did.

Morgan Rogers (he/him) (Jun 30 2023 at 15:55):

John Baez said:

Another question: if I have an $X$-indexed disjoint partition of the terminal object in a topos $\mathsf{T}$, do I get a bunch of topoi $\mathsf{T}_i$, one for each $i \in X$, such that

$\mathsf{T} \simeq \prod_{i \in X} \mathsf{T}_i$?

Yes, with the caveat that once again the product of categories is actually a coproduct in the (2-)category of toposes

Morgan Rogers (he/him) (Jun 30 2023 at 15:56):

A good exercise related to the example above, which I think appears in MacLane and Moerdijk's book, is to work out what the theory classified by presheaves on the poset $0 < 1$.

John Baez (Jun 30 2023 at 15:57):

So there you have a subterminal object with no "complement", right?

Morgan Rogers (he/him) (Jun 30 2023 at 15:57):

Right!

Oscar Cunningham (Jul 01 2023 at 08:01):

Morgan Rogers (he/him) said:

Sorry, my brain inserted "how" into your question

Propositions as types! :rolling_on_the_floor_laughing:

Reid Barton (Jul 05 2023 at 06:26):

Another description of the answer that may have been easier to guess is (if I'm not also confused)
John Baez said:

Okay, good. I like to think semantically, i.e. describing theories by saying what their models are like. So if I'm not confused, I would say $\mathsf{Set}/X$ is "the classifying topos for the theory of an element of $X$", meaning that to specify a geometric morphism from some topos [$\mathcal{E}$] to $\mathsf{Set}/X$ we just choose an element of X

... a global section of the constant sheaf $X$ on $\mathcal{E}$.

John Baez (Jul 05 2023 at 08:17):

Okay, good! I was just flailing around while waiting for the people who actually know topos theory to step in.

Jens Hemelaer (Jul 07 2023 at 18:47):

John Baez said:

Given a bunch of Grothendieck topoi $\mathsf{T}_i$ ($i \in X$) that are the classifying topoi for various theories, what theory is

$\prod_{i \in X} \mathsf{T}_i$

the classifying topos for?

Maybe this became already clear from the discussion above, but a model of this theory in a topos $\mathcal{E}$ is the same as a decomposition of $\mathcal{E}$ as a disjoint union $\mathcal{E} ~=~ \bigsqcup_{i \in X} \mathcal{E}_i$ of toposes (so categorical product), together with for each $i \in X$ a model in $\mathcal{E}_i$ for the theory of the topos $\mathcal{T}_i$.

Jens Hemelaer (Jul 07 2023 at 18:49):

So a model of $\mathcal{T}_i$ for some choice of $i$, but you can change your mind about which $i$ whenever you move to a different component.

John Baez (Jul 07 2023 at 18:50):

Thanks!