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: formal definition of Grothendieck topos

Matteo Capucci (he/him) (Sep 14 2022 at 09:02):

If you have a Yoneda structure on a 2-category $\cal K$, then afaiu you have a KZ monad that allows you to define the 'free cocompletion' of a given object $c : \cal K$. Now free cocompletion of categories give us 'presheaf topoi', and Grothendieck topoi are defined as lex reflective subcategories thereof.
Hence I was wondering what could be a 'formal' version of this definition? The only part of the definition I don't know how to immediately abstract for any 2-cat is the 'exactness' of the reflector.

Nathanael Arkor (Sep 14 2022 at 10:14):

In the case of Grothendieck topoi, the presheaf construction gives a $(\mathbf{Cat} \hookrightarrow \mathbf{CAT})$-relative KZ doctrine taking small categories to their free cocompletions under small colimits (which takes values in locally-small categories); and a coKZ doctrine on $\mathbf{CAT}$ taking locally-small categories to their free completions under finite limits. The presheaf construction lifts to the algebras of the coKZ-doctrine, which gives a $(\mathbf{Lex} \hookrightarrow \mathbf{LEX})$-relative KZ-doctrine (in other words, there's a distributive law between a relative KZ-doctrine and a coKZ doctrine). The "$J$-small" algebras for this lifted relative KZ-doctrine are Grothendieck topoi: the exactness condition on the left adjoint arises from the distributivity condition. The intuition for these ideas comes from Fiore–Gambino–Hyland–Winskel's Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures together with Garner–Lack's Lex colimits.

Nathanael Arkor (Sep 14 2022 at 10:15):

To formalise this situation, you therefore need a (pseudo)distributive law between a (relative) KZ-doctrine and a coKZ-doctrine.

Morgan Rogers (he/him) (Sep 14 2022 at 10:52):

Why do you need the coKZ-doctrine part? It's true that you need something extra to show that a free cocompletion is lex, but I don't think that's a strictly crucial feature of the construction.

Nathanael Arkor (Sep 14 2022 at 11:33):

Taking the definition of Grothendieck topos to be a lex-reflective subcategory of a presheaf category (which is the definition that most readily formalises to a 2-categorical context), you need two components: small colimits, and finite limits. The relative KZ-doctrine provides the small colimits, the coKZ-doctrine proves the finite limits, and the pseudodistributive law provides the interaction between the two.

Nathanael Arkor (Sep 14 2022 at 11:34):

I imagine one could take a different definition of Grothendieck topos, and formalise it differently, but this is the one that seems most in the spirit of 2-categorical algebra (essentially the viewpoint presented by Anel–Joyal in Topo-logie).

Morgan Rogers (he/him) (Sep 14 2022 at 11:48):

Silly me for skipping over the lex requirement on the reflection! Fair enough. This does make it hard for me to tell how unusual these conditions are, though. How much of topos theory do you think you could rebuild on top of that abstraction @Nathanael Arkor?

Nathanael Arkor (Sep 14 2022 at 12:11):

I haven't given it a great deal of thought, but my inclination is that one could get quite far using this abstraction. There are other structures that have similar theorems to that of Grothendieck topoi (e.g. Grothendieck categories, and para-topoi) that arise from different (KZ, coKZ) pairs. For some theorems, it may be necessary also to add a presentability assumption (in the vein of Di Liberti–Loregian's Accessibility and presentability in 2-categories), since this does not come for free in a formal setting, unlike the categorical setting, because one cannot play the same tricks with size.

Mike Shulman (Sep 14 2022 at 17:13):

There are also other, more concrete, ways to define lexness abstractly. For instance, you can say that an object $c$ of a 2-category $K$ is lex if all hom-categories $K(x,c)$ have finite limits and all precomposition functors $(-\circ g) : K(y,c) \to K(x,c)$ preserve them. Similarly, if $c$ and $d$ are lex, then a morphism $f:c\to d$ is lex if all postcomposition functors $(f\circ -) : K(x,c) \to K(x,d)$ preserve finite limits. This way you can define a "Grothendieck topos object" in any Yoneda structure.

Nathanael Arkor (Sep 14 2022 at 17:22):

You don't even need a Yoneda structure to define a topos this way, if you're happy defining cocompleteness similarly. I suppose you're imagining that the presheaf aspect is being given by the Yoneda structure, and the lexness representably. But this definition seems a little artificial to me, because it disregards the exactness properties of Grothendieck topoi, since there is no guarantee the presheaf objects of the Yoneda structure are cocomplete. Furthermore, this doesn't recover the correct notion of finite completeness for enriched categories: for that, you need to define the limits using the Yoneda structure too (and then the approach is very similar to the one I outlined).

Mike Shulman (Sep 14 2022 at 17:39):

I think it's consistent to be okay with defining lexness this way but want some more abstract way to talk about cocompleteness, since lexness is an elementary property whereas cocompleteness is not.

Mike Shulman (Sep 14 2022 at 17:40):

And I'm not an expert in Yoneda structures specifically, but it seems to me that in any sensible notion of "formal category theory" presheaf objects should be cocomplete. For instance, this is the case for virtual equipments when you use a suitable notion of smallness (specifically, such that composites along small objects exist) -- the proof is essentially given in 10.25 of Enriched indexed categories.

Mike Shulman (Sep 14 2022 at 17:41):

It's true that you should in general use the notion of "finite limits" from your formal category theory, so that they have an enriched universal property. But I think there is still an essential difference with the KZ/coKZ approach in that the notion of finite limit can be defined, rather than postulated, and one doesn't need to assume or prove that the free completion under such finite limits exists.

Mike Shulman (Sep 14 2022 at 17:41):

I wouldn't be surprised if using an actual definition of "finite limit" in this way, rather than an abstract coKZ monad, yields a notion of "topos object" that behaves more like a traditional topos.

Nathanael Arkor (Sep 14 2022 at 17:48):

it seems to me that in any sensible notion of "formal category theory" presheaf objects should be cocomplete

I am inclined to agree, but I think it's not possible to prove that the presheaf objects of a Yoneda structure are cocomplete without an additional assumption (Weber needs to assume it in Theorem 3.20 of Yoneda structures from 2-toposes, for instance). I think Yoneda structures have several shortcomings over more equipment-theoretic approaches to formal category theory, though.

Nathanael Arkor (Sep 14 2022 at 17:50):

I do agree that the most appropriate setting for "formal topoi" is some kind of equipment, but I think the (co)KZ approach is simpler to explain.

Mike Shulman (Sep 14 2022 at 17:51):

Maybe if you already know what "(co)KZ" means it is. But if you're working in an equipment (or Yoneda structure) you should already know what the correct notion of internal limit and colimit are, so saying "this morphism preserves finite limits" shouldn't really require any extra explanation.

Matteo Capucci (he/him) (Sep 15 2022 at 16:51):

Thank you all for the great replies!