open import Cat.Instances.Product open import Cat.Prelude import Cat.Functor.Bifunctor as Bifunctor import Cat.Reasoning as Cat module Cat.Diagram.Coend where

# Coendsπ

Let
$F : \mathcal{C}{^{{\mathrm{op}}}}\times \mathcal{C} \to \mathcal{D}$
be a functor, which, by the general yoga of bifunctors we think of as
combining a contravariant action
$F(-,x) : \mathcal{C}{^{{\mathrm{op}}}}\to \mathcal{D}$
and a covariant action
$F(x,-) : \mathcal{C} \to \mathcal{D}$
of
$\mathcal{C}$
on
$\mathcal{D}$^{1}. As a concrete example, we could
take
$\mathcal{C} = {\mathbf{B}}R$,
the 1-object ${{\mathbf{Ab}}}$-category
associated to a ring
$R$
β then the functors
$F(-,x)$
and
$F(x,-)$
would be left- and right-
$R$-modules,
respectively. In fact, let us focus on this case and consider two
modules
$A$
and
$B$,
incarnated as a pair of functors
$A : {\mathbf{B}}R{^{{\mathrm{op}}}}\to {{\mathbf{Ab}}}$
and
$B : {\mathbf{B}}R \to {{\mathbf{Ab}}}$.

In this situation, we may study the **tensor product**
(of modules!)
$A \otimes_R B$
as being an βuniversal object where the actions of
$A$
and
$B$
agreeβ. In particular, itβs known that we can compute the tensor product
of modules as being (the object in) a coequaliser diagram like

$A \otimes R \otimes B {\rightrightarrows}A \otimes B {\twoheadrightarrow}A \otimes_R B\text{,}$

where the undecorated $A \otimes B$ stands for the tensor product of abelian groups, and the two maps are given by the $R$-actions of $A$ and $B$. More explicitly, letting $a \otimes b$ stand for a tensor, the equation $a\otimes rb = ar\otimes b$ holds in $A \otimes_R B$, and the tensor product is the universal object where this is forced to hold.

Going back to the absurd generality of a bifunctor $F : \mathcal{C}{^{{\mathrm{op}}}}\times \mathcal{C} \to \mathcal{D}$, 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 $\mathcal{D}$ 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
$F$,
and denote it by
$\int^c F(c,c)$
(or
$\int F$
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.

## Formalisationπ

record Cowedge (F : Functor (C ^op ΓαΆ C) D) : Type (coend-level F) where no-eta-equality

A **cowedge** under a functor
$F$
is given by an object
$w : \mathcal{D}$
(which we refer to as the nadir,
because weβre pretentious), together with a family of maps
$\psi_c : F(c,c) \to w$.

field 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.

extranatural : β {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
**$(w,\psi)$
is a coend for
$F$**
such that, given any other wedge
$(w',\psi)$
under
$F$,
we can factor
$w$
through
$w'$
by a unique map
$e : w \to w'$.
Furthermore, the map
$e$
must commute with the maps
$\psi$,
meaning explicitly that
$e\psi_a = \psi'_a$.

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

field cowedge : Cowedge F

Unfolding the requirement of uniqueness for $e$, we require that, given any other map $f : w \to w'$ s.t. $f\psi_a = \psi'_a$ for all objects $a$, then $e = f$. This is exactly analogous to the uniqueness properties of colimiting maps for every other colimit.

field factor : β (W : Cowedge F) β D.Hom cowedge.nadir (W .nadir) commutes : β {W : Cowedge F} {a} β factor W D.β cowedge.Ο a β‘ W .Ο a unique : β {W : Cowedge F} {g : D.Hom cowedge.nadir (W .nadir)} β (β {a} β g D.β cowedge.Ο a β‘ W .Ο a) β g β‘ factor W

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