module Cat.Diagram.Coend where


Let be a functor, which, by the general yoga of bifunctors we think of as combining a contravariant action and a covariant action of on 1. As a concrete example, we could take the 1-object associated to a ring β€” then the functors and would be left- and right- respectively. In fact, let us focus on this case and consider two modules and incarnated as a pair of functors and

In this situation, we may study the tensor product (of modules!) as being an β€œuniversal object where the actions of and agree”. In particular, it’s known that we can compute the tensor product of modules as being (the object in) a coequaliser diagram like

where the undecorated stands for the tensor product of abelian groups, and the two maps are given by the of and More explicitly, letting stand for a tensor, the equation holds in and the tensor product is the universal object where this is forced to hold.

Going back to the absurd generality of a bifunctor we may still wish to consider these sorts of β€œuniversal quotients where a pair of actions are forced to agree”, even if our codomain category does not have a well-behaved calculus of tensor products. As a motivating example, the computation of left Kan extensions as certain colimits has this form!

We call such an object a coend of the functor and denote it by (or for short). Being a type of colimit, coends are initial objects in a particular category, but we will unpack the definition here and talk about cowedges instead.


record Cowedge (F : Functor (C ^op Γ—αΆœ C) D) : Type (coend-level F) where

A cowedge under a functor is given by an object (which we refer to as the nadir, because we’re pretentious), together with a family of maps

    nadir : D.Ob
    ψ     : βˆ€ c β†’ D.Hom (F.β‚€ (c , c)) nadir

This family of maps must satisfy a condition called extranaturality, expressing that the diagram below commutes. As the name implies, this is like the naturality condition for a natural transformation, but extra! In particular, it copes with the functor being covariant in one argument and contravariant in the other.

      : βˆ€ {c c'} (f : C.Hom c c')
      β†’ ψ c' D.∘ F.second f ≑ ψ c D.∘ F.first f

A coend, then, is a universal cowedge. In particular, we say that is a coend for such that, given any other wedge under we can factor through by a unique map Furthermore, the map must commute with the maps meaning explicitly that

record Coend (F : Functor (C ^op Γ—αΆœ C) D) : Type (coend-level F) where
    cowedge : Cowedge F

Unfolding the requirement of uniqueness for we require that, given any other map s.t. for all objects then This is exactly analogous to the uniqueness properties of colimiting maps for every other colimit.

    factor   : βˆ€ (W : Cowedge F) β†’ D.Hom cowedge.nadir (W .nadir)
    commutes : βˆ€ {W : Cowedge F} {a} β†’ factor W D.∘ cowedge.ψ a ≑ W .ψ a
      : βˆ€ {W : Cowedge F} {g : D.Hom cowedge.nadir (W .nadir)}
      β†’ (βˆ€ {a} β†’ g D.∘ cowedge.ψ a ≑ W .ψ a)
      β†’ g ≑ factor W

  1. β€œAction” here is meant evoke the idea of e.g.Β group actions, and does not refer to a specific conceptβ†©οΈŽ