Free cocompletions made friendly?


Kevin Carlson


July 23, 2024

Lots of us are familiar with computations in Poly, some of which are made really nice by the fact that Poly is the category of families in Set^op, more formally, the free cocompletion of Set^op under coproducts. Free cocompletions under all colimits are also really important; they’re presheaf categories! However, presheaf categories are kind of annoying to actually calculate colimits in (coequalizers of sets are scary), in contrast to how trivial it is to calculate coproducts of polynomials. Free cocompletions are supposed to be closing a category up under “formal” colimits in some sense, so shouldn’t taking the colimits also be “formal”? Actually, it can be! There is a category structure on the class of all small diagrams in C that models the free cocompletion of C in an extremely elementary way with lots of nice properties. This has been known to a few people, such as Andrée Ehresmann, for decades, and in the case of free cocompletions under filtered colimits to a lot more people, such as Grothendieck, but has only been known to me for a couple of weeks. I’d like to make it known to you too. I’m hoping this will be helpful both for generalizations of Poly beyond mere sets of positions and for better expressing data migrations, which is all about writing down functors from a category into a free cocompletion.