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: spatial categorical logic

Leopold Schlicht (Sep 09 2021 at 12:26):

Theories in propositional logic correspond to Boolean algebras. And Boolean algebras correspond to Stone spaces.

Theories in coherent logic correspond to pretoposes. And pretoposes correspond to (some) ultracategories.

So in these two cases one not only gets a correspondence between theories and categorical structures, as usual in categorical logic, but there's an additional component: spaces. Note that the Stone space assigned to a propositional theory consists of the models of the theory in the standard Boolean algebra $2=\{0,1\}$. Similarly, the ultracategory assigned to a coherent theory consists of the models of the theory in the standard ultracategory $\mathbf{Set}$.

What about other doctrines, like geometric logic, higher-order logic, first-order logic, $\lambda$-calculus, equational logic: are there "spatial" analogues of Stone spaces and ultracategories? (Although I don't know if it's okay to call ultracategories "spatial" objects.)

Can a theory always be recovered from its "classical" models (like only those in $2$ or $\mathbf{Set}$)?

Leopold Schlicht (Sep 09 2021 at 12:34):

In the case of the doctrine of geometric logic, one might argue that the corresponding categorical structure, Grothendieck toposes, already are quite "spatial". However, in this case one can ask the question whether there's a more topological definition of Grothendieck toposes that doesn't takes the detour through considering sheaves. (There's a yoga that while Grothendieck toposes are large objects - categories of sheaves - they should correspond to, essentially, small topological objects of which they are sheaves of.) But that's quite unrelated to the above, since the class of models of a theory is almost always large.

Spencer Breiner (Sep 09 2021 at 12:36):

Some theories don't have any classical models. There is an example in this mathoverflow post.

For a more geometric presentation of toposes, you can use topological groupoids a la Butz & Moerdijk.

Morgan Rogers (he/him) (Sep 09 2021 at 12:48):

Flipping your question around, one could appeal to the broad principle of geometry-algebra duality. That is, the objects in which we interpret theories are largely algebraic in nature (most apparent in the Boolean algebra situation), while the duals of these categories are/behave like categories of spaces. This is one of the reasons for Anel and Joyal's "logos/topos duality" idea, that we should call the categories usually called toposes "logoses" and think of toposes as the dual objects (which aligns with the directions of geometric morphisms being that of the direct image functor, which many find counterintuitive).

Leopold Schlicht (Sep 11 2021 at 15:41):

Thanks both!
Spencer Breiner said:

Some theories don't have any classical models. There is an example in this mathoverflow post.

Alright, so for geometric theories it doesn't work. What's so special about coherent theories that makes it work that a theory can be recovered from its models in $\mathbf{Set}$?

For a more geometric presentation of toposes, you can use topological groupoids a la Butz & Moerdijk.

Nice result. But that's only for toposes with enough points, right? Also, it seems like they don't discuss whether the canonical morphisms between topological groupoids correspond to the geometric morphisms between the corresponding sheaf toposes.

Morgan Rogers (he/him) (Sep 11 2021 at 16:05):

Leopold Schlicht said:

Thanks both!
Spencer Breiner said:

Some theories don't have any classical models. There is an example in this mathoverflow post.

Alright, so for geometric theories it doesn't work. What's so special about coherent theories that makes it work that a theory can be recovered from its models in $\mathbf{Set}$?

You've been discussing the completeness theorem for coherent toposes in another thread; it says exactly that there are enough Set-models of any coherent theory (to entirely determine the theory). Hence Spencer's reference is apt: you can only expect to be able to recover a theory from its set-models when there are enough of these.

Leopold Schlicht (Sep 11 2021 at 16:55):

Oh, by "coherent theory" I meant "pretopos". :grinning_face_with_smiling_eyes:

Steve Awodey (Sep 11 2021 at 17:25):

This paper is probably relevant to your question:

First-Order Logical Duality
Steve Awodey, Henrik Forssell
arXiv:1008.3145

For a coherent theory, one can cover the classifying topos by a space of models (essentially the Butz-Moerdijk cover) - with a small set of points - by taking a suitable cardinal bound determined by the language. Adding a groupoid structure determined by isos of models, one then recovers the classifying topos as the equivariant sheaves on the groupoid of models. The syntax is recovered from the classifying topos (up to exact completion) by taking the coherent objects.

Morgan Rogers (he/him) (Sep 11 2021 at 18:29):

Leopold Schlicht said:

Oh, by "coherent theory" I meant "pretopos". :grinning_face_with_smiling_eyes:

It makes no difference, the functors corresponding to the models will still be jointly conservative.

Leopold Schlicht (Sep 12 2021 at 13:10):

@Steve Awodey That's very interesting, thanks!

Is there some way of avoiding, in Theorem 2.5.3, the restriction to coherent categories with enough $\kappa$-small models? Is it possible to come up with a concept like Makkai's ultracategories in this setting (instead of small topological groupoids) in which all models (of an arbitrary coherent category) are stored? That would make the analogy with Makkai duality even stronger.

@Morgan Rogers (he/him) I don't understand this. Why can a pretopos and a coherent topos be recovered from its models in Set, while a Grothendieck topos can't? Is there something like a "Deligne's theorem for pretoposes"?

Steve Awodey (Sep 13 2021 at 02:55):

Leopold Schlicht said:

Steve Awodey That's very interesting, thanks!

Is there some way of avoiding, in Theorem 2.5.3, the restriction to coherent categories with enough $\kappa$-small models? Is it possible to come up with a concept like Makkai's ultracategories in this setting (instead of small topological groupoids) in which all models (of an arbitrary coherent category) are stored? That would make the analogy with Makkai duality even stronger.

Morgan Rogers (he/him) I don't understand this. Why can a pretopos and a coherent topos be recovered from its models in Set, while a Grothendieck topos can't? Is there something like a "Deligne's theorem for pretoposes"?

sure, you could drop the cardinal bound and make large topological groupoids, just as Makkai does for ultragroupoids.

Morgan Rogers (he/him) (Sep 13 2021 at 08:23):

Leopold Schlicht said:

Morgan Rogers (he/him) I don't understand this. Why can a pretopos and a coherent topos be recovered from its models in Set, while a Grothendieck topos can't? Is there something like a "Deligne's theorem for pretoposes"?

My response was under the assumption that when you corrected to "pretopos", you meant "pretopos corresponding to (i.e. syntactic category of) a coherent theory"; otherwise what I said is false.

The reason that we need "enough points" for recoverability is that we need the corresponding functors to be jointly conservative = jointly faithful, so that no information is lost when considering the collection of all models.

Zhen Lin Low (Sep 13 2021 at 09:05):

Morgan Rogers (he/him) said:

My response was under the assumption that when you corrected to "pretopos", you meant "pretopos corresponding to (i.e. syntactic category of) a coherent theory"; otherwise what I said is false.

I don't think this restriction is necessary, unless "pretopos" means infinitary pretopos. (Finitary) pretoposes have enough points, literally by Deligne's theorem.

Morgan Rogers (he/him) (Sep 13 2021 at 09:39):

I said this because the definition of pretopos makes no restriction as to size etc, so all Grothendieck toposes are instances of pretoposes, and not all of them have enough points.

Zhen Lin Low (Sep 13 2021 at 09:43):

There's a linguistic ambiguity here which you are getting confused by. A pretopos has enough points if the class of coherent functors from it to Set is jointly conservative. A Grothendieck topos has enough points if the class of inverse-image-of-geometric-morphism functors from it to Set is jointly conservative. A Grothendieck topos may not have enough points as a Grothendieck topos but its underlying pretopos always has enough points.

Morgan Rogers (he/him) (Sep 13 2021 at 10:00):

Ah, I see; the pretopos points correspond (when the pretopos is suitably small and locally small) to the points of the topos obtained by equipping it with the coherent topology rather than the canonical topology. Thanks for the clarification!

Zhen Lin Low (Sep 13 2021 at 10:31):

Yes, there is a size issue I swept under the rug there. Small definitely suffices, I'm not sure if locally small is good enough. But if you believe in universes then there's always a big enough Set that works.

Leopold Schlicht (Sep 13 2021 at 13:04):

Thanks, your discussion cleared up some of the confusion I had!

Zhen Lin Low said:

I don't think this restriction is necessary, unless "pretopos" means infinitary pretopos. (Finitary) pretoposes have enough points, literally by Deligne's theorem.

What do you mean by "literally"? Literally, Deligne's theorem is about toposes and not pretoposes.

Zhen Lin Low (Sep 13 2021 at 13:09):

A finitary pretopos is a coherent site. Deligne's theorem says that the topos of sheaves on a coherent site has enough points.

Leopold Schlicht (Sep 13 2021 at 13:13):

And the points of that topos of sheaves correspond precisely to the points of the pretopos we started with?

Steve Awodey (Sep 13 2021 at 14:18):

Morgan Rogers (he/him) said:

Leopold Schlicht said:

Morgan Rogers (he/him) I don't understand this. Why can a pretopos and a coherent topos be recovered from its models in Set, while a Grothendieck topos can't? Is there something like a "Deligne's theorem for pretoposes"?

My response was under the assumption that when you corrected to "pretopos", you meant "pretopos corresponding to (i.e. syntactic category of) a coherent theory"; otherwise what I said is false.

The reason that we need "enough points" for recoverability is that we need the corresponding functors to be jointly conservative = jointly faithful, so that no information is lost when considering the collection of all models.

Sorry, this is not quite right.
Any small pretopos has enough coherent functors into Set by Deligne's theorem - it doesn't need to be "syntactic" or anything like that.
For large pretoposes we would need a small generating subcategory.

Morgan Rogers (he/him) (Sep 13 2021 at 14:27):

I think that's what Zhen Lin Low pointed out :+1:

Leopold Schlicht (Sep 13 2021 at 19:08):

Leopold Schlicht said:

Why can a pretopos and a coherent topos be recovered from its models in Set, while a Grothendieck topos can't?

I just found out that this is discussed in D1.5 in the Elephant.

Leopold Schlicht (Mar 02 2022 at 11:16):

Does the Butz-Moerdijk construction applied to the étale topos of the spectrum of some field $k$ yield the absolute Galois group of $k$, considered as a topological group?

Zhen Lin Low (Mar 02 2022 at 11:43):

It seems unlikely to me. The objects of the groupoid are isomorphism classes of enumerated models, but I think it is possible to have non-isomorphic enumerated models, so you don't get a one-object groupoid.

Leopold Schlicht (Mar 02 2022 at 11:44):

Thanks!

Leopold Schlicht (Mar 13 2022 at 13:14):

Is there nevertheless a relationship between these two constructions (Butz-Moerdijk groupoid vs. absolute Galois group)?

Graham Manuell (Mar 13 2022 at 18:28):

Leopold Schlicht said:

Is there nevertheless a relationship between these two constructions (Butz-Moerdijk groupoid vs. absolute Galois group)?

Well, perhaps this is a tautology, but the two topological groupoids are weakly equivalent.
Edit: I wasn't thinking when I said this was a tautology. They will have equivalent étale completions, but I don't know the particular Butz-Moerdijk construction well enough to say if they'll actually be equivalent in this case.

Leopold Schlicht (Mar 14 2022 at 09:47):

Thanks! What does weakly equivalent mean?

Graham Manuell (Mar 14 2022 at 14:04):

I meant that they are connected by a span of fully faithful essentially-surjective-on-objects internal functors.

As I mentioned in the edit, I don't actually know that this is true though. In fact, it feels like it isn't because iirc in the Butz-Moerdijk construction the source and target morphism are locally connected and maybe it's unlikely for such a groupoid to be equivalent to a profinite group?

Since localic groupoids contain strictly more information than their associated toposes, in my opinion it is probably better to construct the localic groupoid directly (and this is not too hard for the étale 'topos') and then get the topos from that if necessary, instead of trying to get a localic groupoid from the topos. Though possibly this take is controversial.

Leopold Schlicht (Mar 14 2022 at 15:11):

Thanks!

Butz and Moerdijk's construction begins by fixing a set of enough points of our input topos $\mathcal E$. Does the construction still work when we work with the large collection of all points of $\mathcal E$? We will then get a large topological groupoid - will $\mathcal E$ be equivalent to the category of equivariant sheaves on that topological groupoid?

Graham Manuell (Mar 14 2022 at 15:47):

Depending on your foundations I imagine that will work. Though I don't really see to point of trying to get a topological groupoid in the first place to be honest. Why not just work with a localic groupoid? It's more general and the construction is easier to understand (in my opinion).

Spencer Breiner (Mar 14 2022 at 17:33):

In the Butz-Moerdijk construction, the topology is built using a set of labels with surjections onto the the models of the theory. If you tried to use all models, what would you use for the label set?

Leopold Schlicht (Mar 15 2022 at 09:37):

Earlier @Steve Awodey replied to a similar question of mine:

sure, you could drop the cardinal bound and make large topological groupoids, just as Makkai does for ultragroupoids.

This suggests to me that it would work somehow. But how?

Spencer Breiner (Mar 15 2022 at 12:45):

Maybe make the construction functorial in the label set, and look at families of groupoids labelled by larger and larger sets?

Leopold Schlicht (Mar 15 2022 at 13:37):

@Graham Manuell The reason I am asking about topological groupoids is because I'm interested in the Awodey-Forssell duality for first-order logic mentioned earlier. How does the Joyal-Tierney localic groupoid of the classifying topos of a classical first-order theory look like? If this has a simple description, this could get me interested in localic groupoids.

Graham Manuell (Mar 15 2022 at 14:12):

As far as I remember the construction is actually very similar to the one used by Forssell in his PhD thesis. I don't know of a very explicit description to point you towards at the moment, but I've actually been meaning to write a short note explaining what the construction gives for the classifying topos of a geometric theory, so hopefully in a month or so I'll be able to send you a link!

Graham Manuell (Mar 15 2022 at 14:22):

In the meantime you might also be interested in this paper: https://arxiv.org/abs/1710.02246.

Leopold Schlicht (Mar 16 2022 at 14:38):

Graham Manuell said:

so hopefully in a month or so I'll be able to send you a link!

Looking forward to that!