colimits in `Quiv.{v, u}`

Stream: maths

[Robert Maxton]

Is it in fact true that Quiv.{v, u} -- the category of graphs with vertices in Type u and hom-types all in Type v, i.e. "u-small and locally v-small", with v not necessarily equal to u -- has all colimits?

Let's name the property "u-small and locally v-small" as EssentiallySmall.{v, u}. (Whether or not we should actually change docs#CategoryTheory.EssentiallySmall is a separate question, I just need a short name.) Let's describe Quiv.{v, u} as a full subcategory of the functor category from the usual underlying site to Type max v u; we shall refer to that site as Quiv₀.

Then Quiv.{v, u} has all limits of size min v u (if such a universe level existed, alas), by the following argument:

1. Note that products of size w result in a Quiv.{max w v, max w u}, so the property EssentiallySmall.{v, u} is closed under min u v-sized products
2. Note that the arrow from an arbitary min u v-sized limit to the product on the same diagram is mono
3. Note that in Quiv, a prefunctor F is mono iff both F.obj and F.map are injective as functions
4. Injective functions into a small type prove the domain are small; thus EssentiallySmall.{v, u} is closed under arbitrary min v u-sized limits
5. The functor category Quiv₀ ⥤ Type max v u has all min v u-sized limits; thus the full subcategory of such functors that are EssentiallySmall.{v, u} has all such limits as well; this latter subcategory is equivalent to Quiv.{v, u}; QED.

This proof has already been implemented in Lean. I was intending to repeat this proof dually for colimits -- EssentiallySmall.{v, u} is also closed under coproducts of size u; the arrow from a coproduct to a colimit is epi; a prefunctor is epi iff both F.obj and F.map are surjective as functions; surjective functions from a small type prove the codomain is small, thus...

... nothing, because if that arrow from the coproduct to the colimit identifies enough vertices and doesn't identify the corresponding edges, then a priori your locally v-small coproduct might still produce a hom-type of size as much as max v u in the colimit.

I guess I'm asking for a second opinion/sanity check: is there some subtler reason why this can't happen? Or do I need to include a [UnivLE.{u, v}] assumption in my HasColimitsOfSize instance?

[David Wärn]

Indeed you do need UnivLE as the following example shows. Start from a quiver consisting of a lot of disjoint copies of the walking arrow. This has a large type of objects but small homsets. Then collapse all objects so you just have one object. This can be described as a pushout (of the discrete quiver on your objects, and the terminal quiver). In the end you get a lot of morphisms all in the same homset

[Robert Maxton]

Hm, okay. Thanks for the nice clear counterexample!