Remark 4.2.5.1.3 (002P) — The Clowder Project

4.2.5 Coequalisers

Let $A$ and $B$ be sets and let $f,g\colon A\rightrightarrows B$ be functions.

Definition 4.2.5.1.1 ▶ Coequalisers of Sets

The coequaliser of $f$ and $g$ is the coequaliser of $f$ and $g$ in $\mathsf{Sets}$ as in , .

Construction 4.2.5.1.2 ▶ Construction of Coequalisers of Sets

Concretely, the coequaliser of $f$ and $g$ is the pair $\webleft (\operatorname {\mathrm{CoEq}}\webleft (f,g\webright ),\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\webright )$ consisting of:

1.
The Colimit. The set $\operatorname {\mathrm{CoEq}}\webleft (f,g\webright )$ defined by

\[ \operatorname {\mathrm{CoEq}}\webleft (f,g\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}B/\mathord {\sim }, \]

where $\mathord {\sim }$ is the equivalence relation on $B$ generated by $f\webleft (a\webright )\sim g\webleft (a\webright )$.
2.
The Cocone. The map

\[ \operatorname {\mathrm{coeq}}\webleft (f,g\webright )\colon B\twoheadrightarrow \operatorname {\mathrm{CoEq}}\webleft (f,g\webright ) \]

given by the quotient map $\pi \colon B\twoheadrightarrow B/\mathord {\sim }$ with respect to the equivalence relation generated by $f\webleft (a\webright )\sim g\webleft (a\webright )$.

Proof of Construction 4.2.5.1.2.

We claim that $\operatorname {\mathrm{CoEq}}\webleft (f,g\webright )$ is the categorical coequaliser of $f$ and $g$ in $\mathsf{Sets}$. First we need to check that the relevant coequaliser diagram commutes, i.e. that we have

\[ \operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ f=\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ g. \]

Indeed, we have

\begin{align*} \webleft [\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ f\webright ]\webleft (a\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\webright ]\webleft (f\webleft (a\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f\webleft (a\webright )\webright ]\\ & = \webleft [g\webleft (a\webright )\webright ]\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\webright ]\webleft (g\webleft (a\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ g\webright ]\webleft (a\webright )\end{align*}

for each $a\in A$. Next, we prove that $\operatorname {\mathrm{CoEq}}\webleft (f,g\webright )$ satisfies the universal property of the coequaliser. Suppose we have a diagram of the form

in $\mathsf{Sets}$. Then, since $c\webleft (f\webleft (a\webright )\webright )=c\webleft (g\webleft (a\webright )\webright )$ for each $a\in A$, it follows from Chapter 10: Conditions on Relations, Item 4 and Item 5 of Proposition 10.6.2.1.3 that there exists a unique map $\operatorname {\mathrm{CoEq}}\webleft (f,g\webright )\overset {\exists !}{\to }C$ making the diagram

commute.

Remark 4.2.5.1.3 ▶ Unwinding Definition 4.2.5.1.1

In detail, by Chapter 10: Conditions on Relations, Construction 10.5.2.1.2, the relation $\mathord {\sim }$ of Definition 4.2.5.1.1 is given by declaring $a\sim b$ iff one of the following conditions is satisfied:

1.
We have $a=b$;
2.
There exist $x_{1},\ldots ,x_{n}\in B$ such that $a\sim 'x_{1}\sim '\cdots \sim 'x_{n}\sim 'b$, where we declare $x\sim 'y$ if one of the following conditions is satisfied:
1. (a)
  There exists $z\in A$ such that $x=f\webleft (z\webright )$ and $y=g\webleft (z\webright )$.
2. (b)
  There exists $z\in A$ such that $x=g\webleft (z\webright )$ and $y=f\webleft (z\webright )$.
In other words, there exist $x_{1},\ldots ,x_{n}\in B$ satisfying the following conditions:
1. (a)
  There exists $z_{0}\in A$ satisfying one of the following conditions:
  1. (i)
    We have $a=f\webleft (z_{0}\webright )$ and $x_{1}=g\webleft (z_{0}\webright )$.
  2. (ii)
    We have $a=g\webleft (z_{0}\webright )$ and $x_{1}=f\webleft (z_{0}\webright )$.
2. (b)
  For each $1\leq i\leq n-1$, there exists $z_{i}\in A$ satisfying one of the following conditions:
  1. (i)
    We have $x_{i}=f\webleft (z_{i}\webright )$ and $x_{i+1}=g\webleft (z_{i}\webright )$.
  2. (ii)
    We have $x_{i}=g\webleft (z_{i}\webright )$ and $x_{i+1}=f\webleft (z_{i}\webright )$.
3. (c)
  There exists $z_{n}\in A$ satisfying one of the following conditions:
  1. (i)
    We have $x_{n}=f\webleft (z_{n}\webright )$ and $b=g\webleft (z_{n}\webright )$.
  2. (ii)
    We have $x_{n}=g\webleft (z_{n}\webright )$ and $b=f\webleft (z_{n}\webright )$.

Example 4.2.5.1.4 ▶ Examples of Coequalisers of Sets

Here are some examples of coequalisers of sets.

1.
Quotients by Equivalence Relations. Let $R$ be an equivalence relation on a set $X$. We have a bijection of sets

\[ X/\mathord {\sim }_{R}\cong \operatorname {\mathrm{CoEq}}\webleft (R\hookrightarrow X\times X\underset {\operatorname {\mathrm{\mathrm{pr}}}_{2}}{\overset {\operatorname {\mathrm{\mathrm{pr}}}_{1}}{\rightrightarrows }}X\webright ). \]

Proof of Example 4.2.5.1.4.

Item 1: Quotients by Equivalence Relations

See [Proof Wiki Contributors, Quotient Mapping Is Coequalizer — Proof Wiki].

Proposition 4.2.5.1.5 ▶ Properties of Coequalisers of Sets

Let $A$, $B$, and $C$ be sets.

1.
Associativity. We have isomorphisms of sets¹

\[ \underbrace{\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ f,\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ h\webright )}_{{}=\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ g,\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ h\webright )}\cong \operatorname {\mathrm{CoEq}}\webleft (f,g,h\webright ) \cong \underbrace{\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ f,\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ g\webright )}_{{}=\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ f,\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ h\webright )}, \]
where $\operatorname {\mathrm{CoEq}}\webleft (f,g,h\webright )$ is the colimit of the diagram
in $\mathsf{Sets}$.
2.
Unitality. We have an isomorphism of sets

\[ \operatorname {\mathrm{CoEq}}\webleft (f,f\webright )\cong B. \]
3.
Commutativity. We have an isomorphism of sets

\[ \operatorname {\mathrm{CoEq}}\webleft (f,g\webright ) \cong \operatorname {\mathrm{CoEq}}\webleft (g,f\webright ). \]
4.
Interaction With Composition. Let

\[ A \underset {g}{\overset {f}{\rightrightarrows }} B \underset {k}{\overset {h}{\rightrightarrows }} C \]

be functions. We have a surjection

\[ \operatorname {\mathrm{CoEq}}\webleft (h\circ f,k\circ g\webright )\twoheadrightarrow \operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (h,k\webright )\circ h\circ f,\operatorname {\mathrm{coeq}}\webleft (h,k\webright )\circ k\circ g\webright ) \]

exhibiting $\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (h,k\webright )\circ h\circ f,\operatorname {\mathrm{coeq}}\webleft (h,k\webright )\circ k\circ g\webright )$ as a quotient of $\operatorname {\mathrm{CoEq}}\webleft (h\circ f,k\circ g\webright )$ by the relation generated by declaring $h\webleft (y\webright )\sim k\webleft (y\webright )$ for each $y\in B$.

¹That is, the following three ways of forming “the” coequaliser of $\webleft (f,g,h\webright )$ agree:
1. (a)
  Take the coequaliser of $\webleft (f,g,h\webright )$, i.e. the colimit of the diagram
  in $\mathsf{Sets}$.
2. (b)
  First take the coequaliser of $f$ and $g$, forming a diagram
  
  \[ A\underset {g}{\overset {f}{\rightrightarrows }}B\overset {\operatorname {\mathrm{coeq}}\webleft (f,g\webright )}{\twoheadrightarrow }\operatorname {\mathrm{CoEq}}\webleft (f,g\webright ) \]
  
  and then take the coequaliser of the composition
  
  \[ A\underset {h}{\overset {f}{\rightrightarrows }}B\overset {\operatorname {\mathrm{coeq}}\webleft (f,g\webright )}{\twoheadrightarrow }\operatorname {\mathrm{CoEq}}\webleft (f,g\webright ), \]
  
  obtaining a quotient
  
  \[ \operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ f,\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ h\webright )=\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ g,\operatorname {\mathrm{coeq}}\webleft (f,g\webright )\circ h\webright ) \]
  of $\operatorname {\mathrm{CoEq}}\webleft (f,g\webright )$
3. (c)
  First take the coequaliser of $g$ and $h$, forming a diagram
  
  \[ A\underset {h}{\overset {g}{\rightrightarrows }}B\overset {\operatorname {\mathrm{coeq}}\webleft (g,h\webright )}{\twoheadrightarrow }\operatorname {\mathrm{CoEq}}\webleft (g,h\webright ) \]
  
  and then take the coequaliser of the composition
  
  \[ A\underset {g}{\overset {f}{\rightrightarrows }}B\overset {\operatorname {\mathrm{coeq}}\webleft (g,h\webright )}{\twoheadrightarrow }\operatorname {\mathrm{CoEq}}\webleft (g,h\webright ), \]
  
  obtaining a quotient
  
  \[ \operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ f,\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ g\webright )=\operatorname {\mathrm{CoEq}}\webleft (\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ f,\operatorname {\mathrm{coeq}}\webleft (g,h\webright )\circ h\webright ) \]
  of $\operatorname {\mathrm{CoEq}}\webleft (g,h\webright )$.