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:CopΓ—Cβ†’DF : \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):Copβ†’DF(-,x) : \mathcal{C}{^{{\mathrm{op}}}}\to \mathcal{D} and a covariant action F(x,βˆ’):Cβ†’DF(x,-) : \mathcal{C} \to \mathcal{D} of C\mathcal{C} on D\mathcal{D}1. As a concrete example, we could take C=BR\mathcal{C} = {\mathbf{B}}R, the 1-object Ab{{\mathbf{Ab}}}-category associated to a ring RR β€” then the functors F(βˆ’,x)F(-,x) and F(x,βˆ’)F(x,-) would be left- and right- RR-modules, respectively. In fact, let us focus on this case and consider two modules AA and BB, incarnated as a pair of functors A:BRopβ†’AbA : {\mathbf{B}}R{^{{\mathrm{op}}}}\to {{\mathbf{Ab}}} and B:BRβ†’AbB : {\mathbf{B}}R \to {{\mathbf{Ab}}}.

In this situation, we may study the tensor product (of modules!) AβŠ—RBA \otimes_R B as being an β€œuniversal object where the actions of AA and BB 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βŠ—RβŠ—B⇉AβŠ—Bβ† AβŠ—RB, A \otimes R \otimes B {\rightrightarrows}A \otimes B {\twoheadrightarrow}A \otimes_R B\text{,}

where the undecorated AβŠ—BA \otimes B stands for the tensor product of abelian groups, and the two maps are given by the RR-actions of AA and BB. More explicitly, letting aβŠ—ba \otimes b stand for a tensor, the equation aβŠ—rb=arβŠ—ba\otimes rb = ar\otimes b holds in AβŠ—RBA \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:CopΓ—Cβ†’DF : \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 D\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 FF, and denote it by ∫cF(c,c)\int^c F(c,c) (or ∫F\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 FF is given by an object w:Dw : \mathcal{D} (which we refer to as the nadir, because we’re pretentious), together with a family of maps ψc:F(c,c)β†’w\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,ψ)(w,\psi) is a coend for FF such that, given any other wedge (wβ€²,ψ)(w',\psi) under FF, we can factor ww through wβ€²w' by a unique map e:wβ†’wβ€²e : w \to w'. Furthermore, the map ee must commute with the maps ψ\psi, meaning explicitly that eψa=ψaβ€²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 ee, we require that, given any other map f:wβ†’wβ€²f : w \to w' s.t. fψa=ψaβ€²f\psi_a = \psi'_a for all objects aa, then e=fe = 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

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