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.
What are some benefits of (co)end calculus? To put it differently, what is some motivation to learn it (as a category theorist)?
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
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)
It also continues to work in the -enriched setting, which comes in handy
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 :)
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
Screenshot 2025-12-18 at 15.09.43.png
(Here's the computation on pg 90)
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.
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:
Fosco’s book is indeed goated
It's also full of silly typos! Someday I will compile an errata..
Maybe I can tell you how I fell in love with the topic! Tomorrow morning.
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!)
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" 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.
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 to : maybe this map here is easier to find... after all now I have to come up with an idea to associate an arrow , or a "term" of the internal hom, to an arrow , 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.
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 , depending covariantly on x, and a certain , 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!
Let me add a third example. My favourite category is the category of combinatorial species. Let be the species of subsets, sending a finite set to the set of cardinality of all its subsets. Let 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 and the Cauchy product .
"Cauchy product" is just a fancy name for "Day convolution", a certain monoidal structure that exists on categories of the form : combinatorial species are of this form, if C is the category having objects finite sets, and arrows all the bijections.
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.
So. You can prove that 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 and the coend
First, find a cowedge ; such a cowedge is just a cocone
since does not depend on (and it's constant in a singleton set). (More precisely, the domain of is the set of pairs where is a decomposition of into and is a bijection.)
The component is induced by the image function, sending a bijection to the image of under , i.e. . This is a cocone as the diagram [Figure 1] commutes for every pair of bijections . It is also an initial cocone, as given another cocone for the same diagram, into another set , one can use the cocone condition on to prove that the function sending a subset to is (well-defined and) the unique fitting in the diagram [Figure 2] (the key observation is that every permutation decomposes as where : since the cocone condition can be phrased as the equality for every a permutation acting on and via the sum of two permutations acting on the summands of the the decomposition , one has that \emph{every} is of the form if and . But then, .
...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.
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.
(thinking is very empowering, but requires energy and creativity. We don't always have a full supply of those)
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.
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.
@fosco Thank you so much for your detailed explanations! :folded_hands: