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: Comonadicity of Presheaf Categories

Max New (May 15 2023 at 15:08):

Let $C$ be a category, call the presheaf category $\textrm{Psh} C$ and the presheaf category on the underlying set (or groupoid) of objects of $C$ be called $\textrm{Pow} C$. There is a forgetful functor $U : \textrm{Psh} C \to \textrm{Pow} C$ that has a right adjoint $\forall : \textrm{Pow} C \to \textrm{Psh} C$ which looks like $(\forall R) c = \int_{c'} C(c',c) \to R c'$. It looks to me that this is actually comonadic: a presheaf is a family of sets $R : C_0 \to \textrm{Set}$ equipped with a functoriality structure which looks just like a coalgebra $\varepsilon : R \to U(\forall R)$. Do I have this right? Are there any interesting consequences of this? I vageuly remember a talk by Marcelo Fiore that mentioned a construction like this?

Max New (May 15 2023 at 15:28):

Since comonadic functors create colimits a simple consequence would be that colimits in the presheaf cat are computed pointwise. And if it's also the case that presheaf categories are monadic with the corresponding left adjoint this would also give a reason why limits are given pointwise.

Mike Shulman (May 15 2023 at 16:11):

Yep, this is correct.

Mike Shulman (May 15 2023 at 16:13):

One consequence that I find interesting and useful is that when you consider Cat-enrichment, the category of 2-presheaves has both lax/pseudo morphism classifiers (because it's finitary monadic) and co-classifiers (because it's co-finitary co-monadic). Thus, for Cat-valued presheaves $X,Y$ there are both $QX$ and $RY$ such that a pseudonatural map $X \leadsto Y$ can be represented either by a strict map $QX\to Y$ or a strict map $X\to RY$. This categorifies to "bar and cobar constructions" in homotopy theory.

Dylan McDermott (May 15 2023 at 16:27):

Max New said:

I vageuly remember a talk by Marcelo Fiore that mentioned a construction like this?

My guess is that you mean Marcelo's HoTTEST talk from last year. Slides and video are linked from here, it is on slide 24. There is also a paper.

Nathanael Arkor (May 15 2023 at 16:50):

cc @Dima Szamozvancev

Dima Szamozvancev (May 16 2023 at 08:26):

Indeed, this is what I'm writing my thesis on under Marcelo. The initial inspiration came from Allais et al. (https://arxiv.org/pdf/2001.11001.pdf) who use the coalgebra structure $\square \triangleq U\forall$ to capture renaming. One in fact has an adjoint triple $\exists \dashv U \dashv \forall$ given by left and right Kan extensions along the injection from the underlying objects to $C$, and $U$ is monadic, giving an equivalence of categories between presheaves on $C$, and the categories of $\square$-coalgebras and $\diamond$-algebras (for $\diamond \triangleq U\exists$) on the category of indexed families (~ presheaves on the discrete subcategory). The practical advantage of this is that the presheaf model of abstract syntax (Fiore, Turi, Plotkin, 1999) can be simplified somewhat by separating "presheaves" from their presheaf action and only requiring it when it is needed (in their work, for the pointed strength that pushes substitutions under binders). It makes the theory more amenable to formalisation e.g. in Agda, because you're mostly working with indexed sets, rather than full-on presheaves. Our POPL 2022 paper gives a high-level overview of the theory and how it leads to an Agda framework for language formalisation, and my thesis (nearing (?) completion) will discuss the underlying theory at a higher level of abstraction.

Morgan Rogers (he/him) (May 16 2023 at 09:14):

Another perspective: a point of a topos $\mathcal{E}$ is a geometric morphism $\mathrm{Set} \to \mathcal{E}$ (that is, an adjoint pair of functors with right adjoint in the direction of the arrow, $f_*:\mathrm{Set} \to \mathcal{E}$, such that the left adjoint $f^*$ preserves finite limit. A set $X$ of points can be combined into a geometric morphism $\mathrm{Set}^X \to \mathcal{E}$. This morphism is a geometric surjection (ie the left adjoint is comonadic) if and only if the points in $X$ are jointly faithful, or (equivalently in this case, thanks to the nice properties of toposes) jointly conservative.

A presheaf topos has some special 'representable' points, given by evaluation at a given object of the underlying category. In particular, combining these points produces the geometric morphism from $\mathrm{Set}^{\mathrm{ob}(\mathcal{C})}$ that you noticed, and it is a surjection because the joint conservativity condition is certainly satisfied in this case.
The representable points are essential, meaning that $f^*$ has a further left adjoint, and this is similarly inherited by the compiled point, as you observed.

Matteo Capucci (he/him) (May 17 2023 at 11:21):

I guess this fact can be also read as the fact (co)presheaves on $C$ are equivalent to actions of $C$ on families of sets indexed by its objects. Categories of acts are usually both monadic and comonadic (not sure about actions of categories though), which in this case would tell you the action on morphisms of a (co)presheaf as either an algebraic or coalgebraic structure.

Max New (May 30 2023 at 21:55):

I've thought of another example, which is that the category of coalgebras of a lex comonad on an elementary topos is an elementary topos, and IIUC the comonad above is lex and so this shows how to prove a presheaf category is an elementary topos given that you've proven the easier fact that presheaves on a discrete category form an elementary topos. This is I think what Todd is calling the "lex comonad theorem" here (https://ncatlab.org/toddtrimble/published/Three+topos+theorems+in+one)

Max New (Jun 19 2023 at 15:34):

Is there a way to use this to prove the Yoneda lemma? From this POV, we can take any presheaf $P$ and construct the cofree coalgebra on the underlying family $(\square P)_c = \prod_{c' \in C_0} C(c',c) \to P(c')$, and then the Yoneda lemma gives an explicit description of any $P$ as a sub-presheaf of $\square P$ as an end/the natural elements. I guess this is the image of the coalgebra map $P \to \square P$.

And the co-Yoneda lemma similarly looks like showing every presheaf is a quotient of a free algebra

Max New (Jun 28 2023 at 14:44):

Yes, in fact the Yoneda lemma and Co-Yoneda lemma follow from a general theorem about algebras/co-algebras: (https://ncatlab.org/nlab/show/Eilenberg-Moore+category#AsColimitCompletionOfKleisliCategory).

For the Yoneda case, we have that presheaves are $\square$-coalgebras, and that every coalgebra $(P,\alpha)$ is the equalizer in $P \to \square P \to \square \square P$ where the first arrow is the coalgebra map $\alpha$ and the two arrows being equalized are $\square \alpha$ and the comultiplication $\nu$. The end in the Yoneda lemma is by definition this same equalizer $\square P$, and so since they are equalizers of the same diagram they are canonically isomorphic. Co-Yoneda follows by the dual theorem for algebras as coequalizers.

Max New (Jun 28 2023 at 18:19):

The general theorem about (co)-algebras is the subject of Chapter 5.4 in Emily Riehl's textbook