Coequalizer

definition example theorem proof

The coequalizer of a parallel pair $p,q:A\rightrightarrows B$ is the Colimit of the diagram $\bullet \rightrightarrows \bullet$: an object $C$ with a coequalizing morphism $e:B\to C$ such that $e\circ p=e\circ q$, universal: any $f:B\to X$ with $f\circ p=f\circ q$ factors uniquely as $f=\tilde{f}\circ e$.

Kittenlab’s definition: the coequalizer is a representing object for $F(X)=\{f:B\to X\mid f\circ p=f\circ q\}$; the proposition that a representative comes with a coequalizing morphism $e$ (corresponding to ${\mathrm{id}}_C\in y_C(C)$) and conversely, is “much less data to lug around than a whole natural isomorphism”. “If coproducts allow you to add objects, coequalizers allow you to squish them.”

Sources: Kittenlab Lecture 9 (quotient group $G/H$), 11 (“Adding and squishing”: angles); DaoFP §9.5 (“Coequalizers”), Exercise 9.5.2; 7 Sketches §6.2.4 (finite colimits in $\mathbf{Set}$), §1.2.1 (Quotient Set); CTfS Definition 2.6.3.1, Exercises 2.6.3.2–2.6.3.3, 3.1.2.4, 3.3.1.10

Examples

• Angles (Kittenlab): a program taking an angle should agree on $\theta$ and $\theta +2\pi$; the functor $F(X)=\{f:\mathbb{R}\to X\mid f\circ 1_{\mathbb{R}}=f\circ (+2\pi )\}$ (functions of period $2\pi$) is represented by $[0,2\pi )$, by $[-\pi ,\pi )$ (convenient for pendulums), and by the circle $S^1=\{z\in \mathbb{C}:|z|=1\}$ with $e(\theta )=e^{i\theta }$. In $\mathbf{Set}$ all three are isomorphic; in $\mathbf{Top}$ only $S^1$ works, since $\mathbb{R}\to [0,2\pi )$ “jumps” — the coequalizer depends on the category.
• In $\mathbf{Set}$: $C=B/\sim$ where $\sim$ is the Equivalence Relation generated by $p(a)\sim q(a)$; ”$C$ is a copy of $B$ in which elements produced from the same $a$ have been identified” — bucketizing (DaoFP): coequalizing $\mathsf{fst},\mathsf{snd}$ on pairs of integers of equal parity gives Bool with q n = even n, and any parity-only q' factors as h q' . q (DaoFP Exercise 9.5.2).
• The clock (CTfS Exercises 2.6.3.2, 3.1.2.4): coequalizing $\mathrm{id},(x\mapsto x+1):\mathbb{R}\rightrightarrows \mathbb{R}$ gives the circle $[0,1)$; with $x\mapsto x+12$ it gives the clock face $T=[0,12)$, and the universal property is exactly what makes “advance the clock by $x$ hours” a well-defined map $T\to T$ — an action of the monoid $(\mathbb{R},0,+)$ on the clock (Monoid Action).
• Graphs (CTfS Exercise 3.3.1.10): a graph is a parallel pair $\mathrm{src},\mathrm{tgt}:A\rightrightarrows V$; its coequalizer is the set of connected components (its Equalizer is the set of loops).
• Quotient groups (Kittenlab Lecture 9): in $\mathbf{Ab}$, the coequalizer of the inclusion $H\hookrightarrow G$ and the zero map is $G/H$ — “declaring by fiat every element of $H$ to be $0$“.
• Matrices (Kittenlab Lecture 11): in $\mathbf{Mat}$, the coequalizer of $M,0:n\rightrightarrows m$ is $m-\mathrm{rank}(M)$, with coequalizing matrix $E$ whose rows are an orthonormal basis of the orthogonal complement of the range of $M$: $EM=0$, and any $E^{\prime }$ with $E^{\prime }M=0$ factors through $E$.
• A Pushout is a coequalizer of the two injections into a coproduct; every Colimit is a coequalizer of coproducts.

JuliaLeanHaskell

Docs: FinSets · Limits & colimits — Kittenlab Lecture 9, Lecture 11

using Catlab
p = FinFunction([1, 3], 4); q = FinFunction([2, 3], 4)     # identify 1~2 (and 3~3)
C = coequalizer(p, q)
apex(C), collect(proj(C))        # FinSet(3), [1, 1, 2, 3]
 
# Kittenlab Lecture 11: the coequalizer of M and 0 in Mat via an orthonormal complement
using LinearAlgebra
function coequalizer_mat(M)
  m, k = size(M, 1), rank(M)
  Q = Matrix(qr(hcat(M, Matrix{Float64}(I, m, m))).Q)   # extend an orthonormal basis of range(M)
  Q[:, k+1:m]'                                          # rows v_{k+1}..v_m
end
M = [1.0 0; 0 0; 1 0]; E = coequalizer_mat(M); norm(E * M) < 1e-12   # true

#check CategoryTheory.Limits.coequalizer     -- coequalizer f g with coequalizer.π and coequalizer.desc
#check CategoryTheory.Limits.coequalizer.condition
#check CategoryTheory.Limits.Types.coequalizerIso   -- a quotient by the generated relation

-- DaoFP §9.5: coequalizing fst, snd on same-parity pairs gives Bool
q :: Int -> Bool
q n = n `mod` 2 == 0
 
h :: (Int -> a) -> Bool -> a          -- the unique factorization of a parity-only q'
h q' True  = q' 0
h q' False = q' 1
-- for q' insensitive to the pair components: h q' . q == q'