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: Syntactic Site of the Theory of an Infinite Decidable Object

Ben Logsdon (Apr 26 2024 at 14:28):

I am trying to understand classifying toposes of geometric theories, and in the process syntactic categories/sites of such theories. As an example, I'm thinking about the theory $D_\infty$ of an infinite decidable object (see this nLab page). Apparently the syntactic category of this theory is $\textnormal{FinSet}_{\textnormal{mono}}^{\textnormal{op}}$. I don't understand how this is.

According to the Elephant (D1.4), the objects of the syntactic category are formulas-in-context and the morphisms are provably functional relations. Consider the theory of an infinite decidable object and the following two objects of the syntactic site: $X := x.y.(x \# y)$ and $A := a.b.c.(a \# b \wedge a \# c)$. As far as I can tell, there are four morphisms from $X$ to $A$: 1) $(x,y) \mapsto (a,b)$, 2) $(x,y) \mapsto (a,c)$, 3) $(x,y) \mapsto (b,a)$, and 4) $(x,y) \mapsto (c,a)$. We can't have $(x,y) \mapsto (b,c)$ or $(x,y) \mapsto (c,b)$ because $b$ and $c$ are not provably apart. This means that $X$ and $A$ must be such that there are exactly $4$ injections $A \hookrightarrow X$. But the only examples of this that I can think of are $|A| = 1,3$ and $|X| = 4$, and it seems absurd that $X$ would be represented by a four-element finite set.

I must be missing something fundamental here; what is it?

Morgan Rogers (he/him) (Apr 26 2024 at 15:01):

The syntactic category for the (cartesian) theory of decidable objects is FinSet_mono; for infinite decidable objects you get a syntactic site by equipping this with the atomic topology.

Morgan Rogers (he/him) (Apr 26 2024 at 15:03):

(I may post a more helpful answer later)

Ben Logsdon (Apr 26 2024 at 15:40):

Thanks, @Morgan Rogers (he/him)

The nLab page for the Schanuel topos says that this topos is the classifying topos for $D_\infty$. The same page says that the Schanuel topos is the topos $$\textnormal{Sh}({\textnormal_{FinSet}}_{\textnormal{mono}}^{\textnormal{op}}, J)$$ where $J$ is the coverage you described. If the classifying topos of a theory is the sheaf topos of its syntactic site, wouldn't this mean that the syntactic site of $D_\infty$ is $\textnormal{FinSet}_{\textnormal{mono}}^{\textnormal{op}}$?

Morgan Rogers (he/him) (Apr 26 2024 at 15:41):

No, it doesn't go both ways: a topos is presented by many sites, and conversely the syntactic site depends on the fragment of logic one is working in.

Ben Logsdon (Apr 26 2024 at 15:43):

Is the Schanuel topos presented by both $\textnormal{FinSet}_{\textnormal{mono}}^{\textnormal{op}}$ and $\textnormal{FinSet}_{\textnormal{mono}}$ with approprate topologies, then?

Morgan Rogers (he/him) (Apr 26 2024 at 15:45):

That's not what I'm saying. I'm saying that in general you can't conclude from the statement "the theory T is classified by Sh(C,J)" that (C,J) is 'the' syntactic site for T.

Morgan Rogers (he/him) (Apr 26 2024 at 15:47):

Also yes, there was an error (missing op) in what I said earlier

Ben Logsdon (Apr 26 2024 at 15:49):

Ah, I see.

Morgan Rogers (he/him) (Apr 26 2024 at 15:52):

Alright, to concretely answer your question: considering the cartesian syntactic site $\mathcal{C}:= \mathrm{FinSet}^{\mathrm{op}}$ for the theory of decidable objects as you did, a model of the theory in Sets "is" a flat functor $\mathcal{C} \to \mathrm{Set}$, which corresponds to a geometric morphism $\mathrm{Set} \to [\mathcal{C}^{\mathrm{op}},\mathrm{Set}]$. The inverse image functor sends the representable corresponding to a formula in context $x.\phi$ to its interpretation in the model.

Morgan Rogers (he/him) (Apr 26 2024 at 15:53):

So $x,y.x \# y$ is sent to the collection of pairs of distinct elements, for instance.

Morgan Rogers (he/him) (Apr 26 2024 at 15:55):

Now, to be a point of the subtopos determined by the Grothendieck topology, it is necessary and sufficient for this inverse image to send all of the covering sieves to be sent to jointly epimorphic families. In this case this is particularly simple, since the covering sieves are all generated by singleton families of morphisms.

Morgan Rogers (he/him) (Apr 26 2024 at 15:58):

In particular, it is necessary (and sufficient, by an inductive argument) that the interpretation of the morphisms $x_1,\dotsc,x_n. \bigwedge_{i \neq j} x_i \# x_j \to x_1,\dotsc,x_{n-1}. \bigwedge_{i \neq j} x_i \# x_j$ (corresponding to the indecomposable morphisms in FinSet_mono) are sent to surjections.

Morgan Rogers (he/him) (Apr 26 2024 at 15:58):

This is how you recover that the models are exactly the infinite decidable sets.

Ben Logsdon (Apr 26 2024 at 16:09):

Thanks a bunch for the detailed answer.

Forgive me, but I think my question was a bit unclear. I'm not (currently) asking about the classifying topos itself, just the syntactic site, whose objects are formulas-in-context but which can also be viewed as finite sets through an equivalence of categories. My question is: what are the cardinalities of the objects $X$ and $A$ (as defined in my first message) when viewed as finite sets?

Really, what I want to know is is: why, in the simplest terms, is this syntactic site of $D_\infty$ equivalent to $\textnormal{FinSet}_{\textnormal{mono}}^{\textnormal{op}}$?

Morgan Rogers (he/him) (Apr 27 2024 at 14:28):

Ben Logsdon said:

I'm not (currently) asking about the classifying topos itself, just the syntactic site, whose objects are formulas-in-context but which can also be viewed as finite sets through an equivalence of categories.

I am partly responsible for the confusion here because of the language in my last explanation. FinSet_mono^op is not the (coherent) syntactic site for the theory of decidable objects, it's a full subcategory of it; it may have products but it doesn't have finite limits (consider the pushout of $1 \to 2$ along itself in FinSet: some of the universal maps out of this aren't in FinSet_mono!). We have identified some formulas representing objects of the syntactic site earlier which happen to present objects in this subcategory, but an example of an object that is missing is the formula in context $x,y.\top$, and another is $x,y,z.x\# y \vee y \# z$. The reason that we can select a smaller site is because every (coherent/finitary) formula is provably equivalent to a disjunction of conjunctions of inequalities.
It is a non-trivial fact that this theory is of presheaf type, but for any theory of presheaf type the appropriate category can be recovered (uniquely up to idempotent-completion) as the category of finitely presentable models of the theory.