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: community: our work

Topic: Presheaves and cocompletions in formal category theory


view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:23):

@Dylan McDermott and I have a new preprint on arXiv: Presheaves and cocompletions in formal category theory.

It is a classic and fundamental theorem that the presheaf construction, i.e. the construction taking a small category C\mathbf C to the functor category [Cop,Set][\mathbf{C^\text{op}}, \mathbf{Set}], admits a universal property: it is the completion of C\mathbf C under small colimits (i.e. the free cocompletion of C\mathbf C). Furthermore, even when C\mathbf C is not large, we can obtain its free cocompletion by restricting to the subcategory of [Cop,Set][\mathbf{C^\text{op}}, \mathbf{Set}] spanned by the so-called small presheaves, i.e. the small colimits of representable presheaves. More generally, we can obtain free cocompletions of C\mathbf C under arbitrary classes of colimits (e.g. coproducts, finite colimits, filtered colimits, etc.) by restricting to suitable subcategories of the presheaf category on C\mathbf C.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:24):

The motivation for our paper is to understand the extent to which this phenomenon is purely formal, rather than relying on properties specific to ordinary categories. It is known that this phenomenon also holds in some other contexts, e.g. categories enriched in a nice monoidal category, which might lead us to believe that whenever we have some notion of "presheaf construction" and some notion of "colimit", the presheaf construction may always be used to construct "free cocompletions".

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:24):

But how can we study "presheaf constructions" in general? Rather than work concretely with categories or similar structures, we can work in a context for formal category theory, which is a two-dimensional approach to "category theories". Specifically, we are working in the context of a [[virtual equipment]]. The objects of a virtual equipment behave "like categories", and so we can reason about category-like structures by reasoning about the objects of a virtual equipment.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:24):

In our paper, we define the notion of P\mathbb P-presheaf object in a virtual equipment, which axiomatises "subcategories of presheaf categories", as well as the notion of Φ\Phi-cocompletion, which axiomatises "free cocompletions under a class Φ\Phi of colimits", and show that, under mild assumptions, we may always construct Φ\Phi-cocompletions in the presence of presheaf objects.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:25):

This demonstrates the the classical relationship between presheaf constructions and free cocompletions is not specific to categories, but is entirely formal.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:28):

A secondary motivation for our paper is to address a longstanding gap in the enriched category theory literature, by providing constructions of free completions and cocompletions for categories enriched in a bicategory. (In fact, our construction appears to be new even in the generality of enrichment in a non-symmetric monoidal category.)

Categories enriched in bicategories have not been as well studied as categories enriched in symmetric monoidal categories, but there are plenty of interesting examples (two classic examples being sheaves on a site, and fibrations). We give a small survey of cocompletions of categories enriched in bicategories in the final section of the paper.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:29):

Along the way, we extend much of the theory of presheaves and colimits from enriched category theory (e.g. from Kelly's Basic Concepts of Enriched Category Theory) to formal category theory.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:29):

Here's the abstract:

We study the relationship between presheaf constructions and free cocompletions in the context of formal category theory, elucidating the coincidence between the two concepts in familiar settings. We show that, in a virtual equipment satisfying mild assumptions, free cocompletions under classes of weights are exhibited by presheaf constructions. We furthermore extend the theory of weighted colimits from enriched category theory to this setting, developing the concepts of atomicity and rank, and providing recognition theorems for presheaf objects, free cocompletions, and cocomplete objects. As an application of our methods, we construct free cocompletions, under arbitrary classes of colimit-small weights, of (possibly large) categories enriched in (not necessarily symmetric) monoidal categories and bicategories; this resolves a longstanding omission in the literature on enriched category theory.

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 07:29):

Happy to answer any questions anyone has!

view this post on Zulip Nathanael Arkor (Apr 27 2026 at 08:06):

Dylan gave a recorded talk about this work at the Second Virtual Workshop on Double Categories.

view this post on Zulip John Onstead (Apr 27 2026 at 18:51):

This work was very interesting to me as someone who is looking into formal category theory. I keep a notebook of my category theory questions and in fact one of them was something along the lines of "if a virtual equipment has all presheaf objects, does it have all internal free cocompletions"? It's nice to finally have an answer to that!

view this post on Zulip John Onstead (Apr 27 2026 at 18:52):

I did have a related question. Let's say your virtual equipment doesn't have all the presheaf objects or internal free cocompletions. Maybe you're working with VV-enriched categories where VV does not satisfy the conditions given by the theorems in the paper's sections 9.3 and 9.4, or maybe VV is a non-closed monoidal category (viewed as a one object bicategory). My question is: how does one construct a "free presheaf object completion" that adds in the missing presheaf objects to the equipment? That is, if VirtEq\mathrm{VirtEq} is the category of virtual equipments, PVirtEq\mathrm{PVirtEq} is the category of virtual equipments with all presheaf objects, and U:PVirtEqVirtEqU: \mathrm{PVirtEq} \to \mathrm{VirtEq} is the obvious forgetful functor, the free presheaf object completion is precisely the adjoint to UU. What might be the explicit way to construct this free completion, and how does it work in the case of equipments of form VCatV\mathrm{Cat}?

view this post on Zulip Nathanael Arkor (Apr 28 2026 at 04:55):

It's not something I've considered before, but I don't think it should be too difficult to construct: for each object AA, you will add a new object P[A]\mathcal P[A], for which the tight-cells XP[A]X \to \mathcal P[A] are precisely the loose-cells X↛AX \not\to A, which has a single loose-cell P[A]↛A\mathcal P[A] \not\to A, and no other nontrivial tight/loose-cells to/from P[A]\mathcal P[A]. Because of the paucity of loose-cells into/from the freely added presheaf object, there is little work to adapt this so that it still provides a virtual equipment. As far as I see, the process of adding a presheaf object to an object preserves any existing presheaf objects on other objects, so you can just iterate this process (amounting to adding, for each object, an infinite number of presheaf objects Pn[A]\mathcal P^n[A]). Probably there are some subtleties to iron out, but I expect it is simpler than constructing many other kinds of free constructions.

view this post on Zulip Nathanael Arkor (Apr 28 2026 at 04:56):

(I'm not sure what there is to say in the case of doing this for enriched categories specifically. I don't expect there is some elegant concrete characterisation.)

view this post on Zulip John Onstead (Apr 28 2026 at 06:32):

Interesting- thanks for the insights!

Nathanael Arkor said:

Because of the paucity of loose-cells into/from the freely added presheaf object, there is little work to show that this still provides a virtual equipment

Maybe for every loose arrow X↛AX \not\to A and thus tight arrow XP[A]X \to P[A], one can add in a companion and conjoint loose arrow X↛P[A]X \not\to P[A], to ensure the minimum of virtual equipment structure still exists.