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: pullbacks of cofunctors

Nathaniel Virgo (Aug 25 2024 at 07:24):

Consider the 1-category where the objects are categories and the morphisms are cofunctors, aka [[retrofunctor]] s. Does this category have products or pullbacks? If so, what are they?

Bryce Clarke (Aug 25 2024 at 07:55):

Yes, the 1-category of categories and retrofunctors has all limits. This is Corollary 8.78 in Polynomial Functors: A Mathematical Theory of Interaction.

Bryce Clarke (Aug 25 2024 at 07:55):

I thought I remembered the book having an explicit description of products, but I couldn't find it, so perhaps it was only in a previous version.

Nathaniel Virgo (Aug 25 2024 at 08:20):

Thanks! The proof there is rather indirect, so I still have the question of what they are explicitly.

Todd Trimble (Aug 25 2024 at 16:49):

Is this the category of polynomial comonads on $\mathsf{Set}$, in other words the category of comonoids wrt polynomial composition?

If so, then let $G: \mathsf{Poly} \to \mathsf{Cat}^{\sharp}$ be the right adjoint to the forgetful functor $U$, which is comonadic. $G$ preserves products, so that a product $\prod_i GP_i$ of cofree comonoids $GP_i$ can be formed as $G(\prod_i P_i)$.

Meanwhile, by comonadicity, a general comonoid $C$ is canonically represented as an equalizer of maps between cofree comonoids (formed at the level of underlying polynomial functors):

$C \overset{\eta C}{\to} GUC \overset{GU\eta C}{\underset{\eta GUC}{\rightrightarrows}} GUGUC$

where $\eta$ is the unit of the $U \dashv G$ adjunction. Given a family of comonoids $C_i$, their product is the equalizer of

$\prod_i GUC_i \overset{\prod_i GU\eta C_i}{\underset{\prod_i\eta GUC_i}{\rightrightarrows}} \prod_i GUGUC_i$

(This equalizer exists because as an example of a connected limit, it is created/reflected by $U$, as Niu and Spivak remark.) I don't know how satisfying explicit this is for your purposes, but it's the formal dual of the construction recounted as Theorem 2.2 here.

Kevin Carlson (Aug 26 2024 at 02:24):

It’s implicit in Todd’s answer that you should actually expect products of categories to be hard in retrofunctor-land in the same way that coproducts of algebras are usually very complicated.

Kevin Carlson (Aug 26 2024 at 02:24):

Which is possibly disappointing.