Limits and colimits of quivers and categories

Stream: maths

[Robin Carlier]

Hey everyone! I'm thinking a bit about the possibility of adding a proof that the category of categories is both complete and co-complete. The proof I know is by caracterizing categories as monadic over quivers, and then using the fact that quivers are complete and co-complete as they are a presheaf-like categories. The monadicity theorem and the the adjunction between quivers and categories are already formalised so I think that the first part seems manageable at least in theory.
The second part seems to have a subtlety: the way quivers are defined in lean do not allow for a direct and easy presheaf-like description because of the two universes parameters: quivers with vertices of size u and with hom-types of size vshould form some full subcategory of functors from the walking parralel pair to Type max (u v), but the exact essential image don't seem to be that easy to work with at first glance (the image of the object correpresenting vertices should be a u-small type, but the image of the object co-representing edges should be some sigma type which may not have an easy recognition principle), and I'm starting to wonder wether this approach to proving that categories have limits and colimits is really the right one. Have anyone here thought a bit about this stuff?

[Reid Barton]

I think that Cat.{v u} isn't actually closed under colimits right?

[Reid Barton]

Because if it was you could construct any localization of a locally small category as again a locally small category.

[Robin Carlier]

Can you develop a bit the last argument? I somehow thought that Cat.{v u} would be closed under v-small colimits but I might be thinking to much about the case of small categories...

[Reid Barton]

For example I could start with a large collection of objects $C$ thought of as a discrete category, and then separately adjoin an initial object to form $C^\triangleleft$ or a terminal object to form $C^\triangleright$. Those are locally small categories (posets) but their pushout over $C$ has $C$ as a hom set.

[Robin Carlier]

Right, so in the end everything only work with small categories anyways, where there are no problems.

[Reid Barton]

For limits, it would be true that Cat.{v u} is closed under v-small limits provided v <= u, but we can't express this with the current setup both because we don't have universe inequalities and because the hom sets of Cat.{v u} are not v-sized but u-sized.

[Robin Carlier]

Gotcha, I'll be focusing on the small case then.

[Robin Carlier]

Thanks!

[Adam Topaz]

Reid Barton said:

For limits, it would be true that Cat.{v u} is closed under v-small limits provided v <= u, but we can't express this with the current setup both because we don't have universe inequalities and because the hom sets of Cat.{v u} are not v-sized but u-sized.

You could look at Cat.{v (max v u)}, right?

[Adam Topaz]

Oh, the hom sets will still be max v u sized in this case.

[David Wärn]

How do you prove cocompleteness from monadicity? It would probably be easier (if less fun) to construct both limits and colimits directly. For limits it should be the usual Pi-type story, and for colimits you can take a docs#category_theory.quotient of the path category of a suitable quiver on the colimit of the underlying object types.