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: learning: questions

Topic: (Co)end calculus


view this post on Zulip Jana Nickel (Dec 18 2025 at 19:10):

What are some benefits of (co)end calculus? To put it differently, what is some motivation to learn it (as a category theorist)?

view this post on Zulip Tyler Bryson (Dec 18 2025 at 19:26):

Gosh, it depends on where you're going. In my case, I always find it useful to go through the simplest non-trivial version of a concept in detail.
The first time, I actually bothered proving say (co)end Fubini, I did it with small categories as an exercise to help me understand how to construct Kan Extensions...but I ended up getting an understanding of the coYoneda lemma out of the bargain.
So, for me, I got a better understanding of representability, some hints about how enriched category theorists do their work, and bit of intuition for adjoint functor theorems YMMV

view this post on Zulip Chris Grossack (she/they) (Dec 18 2025 at 20:03):

It's a useful computational tool! It's like a souped-up version of the Yoneda style arguments from module theory where you bounce various adjunctions around (tensor-hom, left/right duals, etc.). (In fact, while I haven't thought very hard about it, I'm sure you can recover those kinds of arguments as a special case)

view this post on Zulip Chris Grossack (she/they) (Dec 18 2025 at 20:05):

It also continues to work in the V\mathcal{V}-enriched setting, which comes in handy

view this post on Zulip Tyler Bryson (Dec 18 2025 at 20:07):

Screenshot 2025-12-18 at 3.07.00 PM.png

Plus, if you have a near crippling need to diagram, parts of it are pretty :)

view this post on Zulip Chris Grossack (she/they) (Dec 18 2025 at 20:08):

In case it's helpful, I just looked through my zotero and found the paper Finite-Product-Preserving Functors, Kan Extensions, and Strongly-Finitary 2-Monads by Kelly and Lack, which is the paper that convinced me to finally learn some of this stuff. In my notes (from 2023) I wrote

This paper freely uses coends…. Which I don’t really understand, haha. It seems like a concise way of building (left) kan extensions, which I kind of understand… But maybe it’s time for me to finally read that book on coend calculus.
...
OH. Wow. Yeah I just saw the computation on written page 90. Yeah… Maybe now’s the time, haha.

Maybe this paper will also convince you, haha

view this post on Zulip Chris Grossack (she/they) (Dec 18 2025 at 20:10):

Screenshot 2025-12-18 at 15.09.43.png

(Here's the computation on pg 90)

view this post on Zulip Ruby Khondaker (she/her) (Dec 18 2025 at 20:28):

Jana Nickel said:

What are some benefits of (co)end calculus? To put it differently, what is some motivation to learn it (as a category theorist)?

It’s very very economical - the way I like to think of it is as categorifying “forall” and “exists”. It lets me write lots and lots of examples of universal constructions with a single notation, and gives me a lot of control in how I express it! I find it similar in spirit to Einstein’s index notation for tensor calculus - it’s very helpful to actually _see_ what indices are getting contracted in a way that isn’t as clear for a more coordinate-free approach.

view this post on Zulip Jana Nickel (Dec 18 2025 at 20:58):

Many thanks!

I also found this book from Fosco Loregian: https://arxiv.org/abs/1501.02503 ,
which seems to include many (theoretic) applications! :slight_smile:

view this post on Zulip Ruby Khondaker (she/her) (Dec 18 2025 at 21:30):

Fosco’s book is indeed goated

view this post on Zulip fosco (Dec 18 2025 at 23:40):

It's also full of silly typos! Someday I will compile an errata..

view this post on Zulip fosco (Dec 18 2025 at 23:41):

Maybe I can tell you how I fell in love with the topic! Tomorrow morning.

view this post on Zulip fosco (Dec 18 2025 at 23:43):

In the meantime, let me tell you I love that Kelly/Lack paper. And many others that didn't make it to the table of contents because I understood them too late. Plus, now I understand a bit better the role of dinaturality and parametricity, thanks to my student @Andrea Laretto (computer scientists should look at his/our work!)

view this post on Zulip fosco (Dec 25 2025 at 15:24):

Suppose you have to compute a (pointwise, but let me drop the qualifier from now on) Kan extension. All concept are Kan extensions, so eventually you will have the problem of determining which precise Kan extension your thing is.

You know it's something with a certain universal property, for every 2-cell such and such there is a unique such and such... and for some reason you also know that they exist, because the codomain category is cocomplete. You are so good that you even know that the colimit you have to compute has domain a certain comma category.

Instead of opening the "analytic" definition of said colimit, coend calculus gives you a general way to argue, when you know that you are trying to evaluate the "integral" xhom(Gx,a)×Fx\int^x \hom(Gx,a)\times Fx in order to see what the left extension of F along G looks like. A proof of this kind usually takes several steps, but its backbone tends to be always the same.

  1. Find a family of arrows hom(Gx,a)×FxS\hom(Gx,a)\times Fx \to S, one for each xx, to a codomain S (depending on aa), that you are guessing is the result
  2. show that the family of point 1 is a "cowedge";
  3. show that it is initial among cowedges.

This proof strategy is similar to what you do when you try to compute a colimit: clearly, the most difficult part is come up with an educated guess for S. There is no general recipe, and that's why colimits are hard, much like integrals. But phrasing things in the terminology of coends one acquires a couple more tools to make the guess. For example, say the ambient category allows to pass from hom(Gx,a)×FxS\hom(Gx,a)\times Fx \to S to hom(Gx,a)[Fx,S]\hom(Gx,a)\to [Fx,S]: maybe this map here is easier to find... after all now I have to come up with an idea to associate an arrow FxSFx \to S, or a "term" of the internal hom, to an arrow GxaGx \to a, and the latter feels more concrete. So, a first advantage of coend calculus that colimits don't enjoy is that often you have more tricks in your bag to "compute" and to have an explicit answer to "what's the unique object having this property?"

This is good: some category theory feels a bit dry. The answer to a problem is "the unique blah such that blah". No shit, my friend, I know: I want to compute it, touch it "in pornographic level of detail", as a dear friend loved to say when he was asking for mathematical explanation. Coends are a gateway to such level of explicitness.

view this post on Zulip fosco (Dec 25 2025 at 15:30):

Another advantage of becoming proficient in the rules of coend calculus (of any calculus, basically by the definition of what is a "calculus": rules you apply offloading some thinking power, in favour or algorythmic manipulation of symbols) is that it gives results --and then the problem is to interpret them. More than once I was able to formulate a conjecture, or prove it, because I was able to "feel" that a certain thing obtained coupling an FxFx, depending covariantly on x, and a certain GxGx, depending contravariantly, was equal to a third thing of interest. How do you prove it? With the "rules" of the calculus: expressing natural transformations between functors as an end, Kan extensions as co/ends, the Fubini rule, Yoneda lemma to "decompose" a "distribution" in terms of its "plane waves" (allow the the Fourier transform analogy :stuck_out_tongue:)...

This is what motivated me to open this question, and Andrea to produce so much work justifying a part of this feeling I had six years ago. I invite you to speak with him, if you want to know more!

view this post on Zulip fosco (Dec 25 2025 at 15:34):

Let me add a third example. My favourite category is the category of combinatorial species. Let \wp be the species of subsets, sending a finite set to the set of cardinality 2n2^n of all its subsets. Let EE be the terminal object of the category (the "species of sets" sending each set to a singleton, regarded as the "answer to the question <<is my input a finite set?>>"). Then there is an isomorphism between \wp and the Cauchy product EEE\otimes E.

"Cauchy product" is just a fancy name for "Day convolution", a certain monoidal structure that exists on categories of the form [C,Set][C,Set]: combinatorial species are of this form, if C is the category having objects finite sets, and arrows all the bijections.

view this post on Zulip fosco (Dec 25 2025 at 15:36):

there are beautiful proofs of this identification, rooted in the fact that species can be depicted as certain decorated graphs, and the operation of Cauchy product is "surgery" on these graphs. Who doesn't know what I'm talking about should skim the book

Bergeron, François, Gilbert Labelle, and Pierre Leroux. Combinatorial species and tree-like structures. No. 67. Cambridge University Press, 1998.

and they will see from the first pages what I'm talking about; alternatively, Joyal's original papers, or Brent Yorgey's thesis, are brilliant resources to learn combinatorial species, which are some categorical object lying at the core of modern enumerative combinatorics.

view this post on Zulip fosco (Dec 25 2025 at 15:43):

So. You can prove that EE\wp\cong E\otimes E using combinatorics, but if you are a category theorist you might want a "more idiomatic" proof: at the cost of being pedantic and verbose, here it is

==

One has to prove that there is a canonical isomorphism between [A]\wp[A] and the coend

IJE[I]×E[J]×Bij(I+J,A)\int^{IJ} E[I]\times E[J] \times \mathbf{Bij}(I+J,A)

First, find a cowedge E[I]×E[J]×Bij(I+J,A)Bij(I+J,A)[A]E[I]\times E[J] \times \mathbf{Bij}(I+J,A) \cong \mathbf{Bij}(I+J,A) \to \wp[A]; such a cowedge is just a cocone

ωIJ:Bij(I+J,A)[A]\omega_{IJ} : \mathbf{Bij}(I+J,A)\to \wp[A]

since E[I]×E[J]E[I]\times E[J] does not depend on I,JI,J (and it's constant in a singleton set). (More precisely, the domain of ωIJ\omega_{IJ} is the set of pairs ((I,J);σ)((I,J);\sigma) where (I,J)(I,J) is a decomposition of AA into I+JI+J and σ:I+J=AA\sigma : I+J=A\to A is a bijection.)

The component ωIJ:Bij(I+J,A)[A]\omega_{IJ} : \mathbf{Bij}(I+J,A) \to \wp[A] is induced by the image function, sending a bijection σ:I+JA\sigma : I+J\to A to the image of II under σ\sigma, i.e. (I,J)σIA(I,J)\mapsto\sigma I \subseteq A. This is a cocone as the diagram [Figure 1] commutes for every pair of bijections α:II,β:JJ\alpha : I'\to I,\beta :J'\to J. It is also an initial cocone, as given another cocone γIJ:Bij(I+J,A)Z\gamma_{IJ} : \mathbf{Bij}(I+J,A)\to Z for the same diagram, into another set ZZ, one can use the cocone condition on (γIJ,(I,J))(\gamma_{IJ}, (I,J)) to prove that the function [A]Z\wp[A] \to Z sending a subset IAI\subseteq A to γI,Ic(1A)\gamma_{I,I^c}(1_A) is (well-defined and) the unique uu fitting in the diagram [Figure 2] (the key observation is that every permutation σ:I+JA\sigma : I+J\to A decomposes as α+β\alpha+\beta where α:IσI,β:JσJ\alpha : I \to \sigma I, \beta : J\to \sigma J: since the cocone condition can be phrased as the equality γIJ(τ(α+β))=γIJ(τ)\gamma_{I'J'}(\tau \circ (\alpha + \beta)) = \gamma_{IJ}(\tau) for every σ=α+β:I+JI+J\sigma = \alpha + \beta : I + J \to I' + J' a permutation acting on III \cong I' and JJJ \cong J' via the sum of two permutations acting on the summands of the the decomposition A=I+JA = I + J, one has that \emph{every} σ\sigma is of the form σ1+σ2\sigma_1+\sigma_2 if I:=σ(I)I' := \sigma(I) and J=σ(J)J' = \sigma(J). But then, γ(σ)=γ(idσ)=γ(id)\gamma(\sigma) = \gamma(\text{id} \circ \sigma) = \gamma(\text{id}).

image.png
image.png

view this post on Zulip fosco (Dec 25 2025 at 15:45):

...before you complain: admittedly, this proof technique is useless and masochistic. One can handwave the isomorphism in question gaining in intuition. But it's also a proof of concept that if you are particularly stubborn you can throw intuition out of the window, armed with only category theory, and prove in the familiar terms of coends, a fact about combinatorial objects that have no specific incarnation.

One of the lessons that my masters repeated the strongest is that a mathematician is a lazy creature: if you have a proof that forces you to think, and one where you just blindly compute, you should prefer the latter... provided you are confident you can compute correctly.

view this post on Zulip fosco (Dec 25 2025 at 15:47):

So the punchline: coend calculus is cool because it is among a series of martial arts with which one can make correct statements regarding things they don't intimately know. And asserting correct things about stuff we ignore is, in my humble opinion, the heart of Mathematics.

view this post on Zulip fosco (Dec 25 2025 at 15:49):

(thinking is very empowering, but requires energy and creativity. We don't always have a full supply of those)

view this post on Zulip Patrick Nicodemus (Dec 25 2025 at 17:09):

fosco said:

(thinking is very empowering, but requires energy and creativity. We don't always have a full supply of those)

This was phrased well by Alfred North Whitehead:

Operations of thought are like cavalry charges in a battle — they are strictly limited in number, they require fresh horses, and must only be made at decisive moments.

view this post on Zulip Patrick Nicodemus (Dec 25 2025 at 17:13):

if you have a proof that forces you to think, and one where you just blindly compute, you should prefer the latter... provided you are confident you can compute correctly.

Well, it depends what the goal is. Mathematical practice has multiple distinct ends and aims. I would preface this by saying: if the sole goal is to establish a theorem, then yes, let us compute.

view this post on Zulip Jana Nickel (Dec 25 2025 at 18:08):

@fosco Thank you so much for your detailed explanations! :folded_hands: