The Clowder Project

Let $f\colon X\to Y$ be a function and let $R$ be a relation on $X$.

1. As a Coequaliser. We have an isomorphism of sets
   \[ X/\mathord {\sim }^{\mathrm{eq}}_{R}\cong \text{CoEq}\webleft (R\hookrightarrow X\times X\stackrel{\stackrel{\text{pr}_{1}}{\rightarrow }}{\stackrel{\rightarrow }{\scriptsize \text{pr}_{2}}}X\webright ), \]

   where $\mathord {\sim }^{\mathrm{eq}}_{R}$ is the equivalence relation generated by $\mathord {\sim }_{R}$.

2. As a Pushout. We have an isomorphism of sets¹
   
   where $\mathord {\sim }^{\mathrm{eq}}_{R}$ is the equivalence relation generated by $\mathord {\sim }_{R}$.
3. The First Isomorphism Theorem for Sets. We have an isomorphism of sets²³
   \[ X/\mathord {\sim }_{\mathrm{Ker}\webleft (f\webright )} \cong \mathrm{Im}\webleft (f\webright ). \]
4. Descending Functions to Quotient Sets, I. Let $R$ be an equivalence relation on $X$. The following conditions are equivalent:
   1. There exists a map
      \[ \overline{f}\colon X/\mathord {\sim }_{R}\to Y \]

      making the diagram

      

      commute.

   2. We have $R\subset \mathrm{Ker}\webleft (f\webright )$.
   3. For each $x,y\in X$, if $x\sim _{R}y$, then $f\webleft (x\webright )=f\webleft (y\webright )$.
5. Descending Functions to Quotient Sets, II. Let $R$ be an equivalence relation on $X$. If the conditions of Item 4 hold, then $\overline{f}$ is the unique map making the diagram
   

   commute.

6. Descending Functions to Quotient Sets, III. Let $R$ be an equivalence relation on $X$. We have a bijection
   \[ \textup{Hom}_{\mathsf{Sets}}\webleft (X/\mathord {\sim }_{R},Y\webright )\cong \textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X,Y\webright ), \]

   natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, given by the assignment $f\mapsto \overline{f}$ of Item 4 and Item 5, where $\textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X,Y\webright )$ is the set defined by

   \[ \textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X,Y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ f\in \textup{Hom}_{\mathsf{Sets}}\webleft (X,Y\webright )\ \middle |\ \begin{aligned} & \text{for each $x,y\in X$,}\\ & \text{if $x\sim _{R}y$, then}\\ & \text{$f\webleft (x\webright )=f\webleft (y\webright )$}\end{aligned} \webright\} . \]
7. Descending Functions to Quotient Sets, IV. Let $R$ be an equivalence relation on $X$. If the conditions of Item 4 hold, then the following conditions are equivalent:
   1. The map $\overline{f}$ is an injection.
   2. We have $R=\mathrm{Ker}\webleft (f\webright )$.
   3. For each $x,y\in X$, we have $x\sim _{R}y$ iff $f\webleft (x\webright )=f\webleft (y\webright )$.
8. Descending Functions to Quotient Sets, V. Let $R$ be an equivalence relation on $X$. If the conditions of Item 4 hold, then the following conditions are equivalent:
   1. The map $f\colon X\to Y$ is surjective.
   2. The map $\overline{f}\colon X/\mathord {\sim }_{R}\to Y$ is surjective.
9. Descending Functions to Quotient Sets, VI. Let $R$ be a relation on $X$ and let $\mathord {\sim }^{\mathrm{eq}}_{R}$ be the equivalence relation associated to $R$. The following conditions are equivalent:
   1. The map $f$ satisfies the equivalent conditions of Item 4:
      • There exists a map
        \[ \overline{f}\colon X/\mathord {\sim }^{\mathrm{eq}}_{R}\to Y \]

        making the diagram

        

        commute.

      • For each $x,y\in X$, if $x\sim ^{\mathrm{eq}}_{R}y$, then $f\webleft (x\webright )=f\webleft (y\webright )$.

   2. For each $x,y\in X$, if $x\sim _{R}y$, then $f\webleft (x\webright )=f\webleft (y\webright )$.

---

¹Dually, we also have an isomorphism of sets

²Further Terminology: The set $X/\mathord {\sim }_{\mathrm{Ker}\webleft (f\webright )}$ is often called the coimage of $f$, and denoted by $\mathrm{CoIm}\webleft (f\webright )$.

³In a sense this is a result relating the monad in $\textbf{Rel}$ induced by $f$ with the comonad in $\textbf{Rel}$ induced by $f$, as the kernel and image

\begin{gather*} \mathrm{Ker}\webleft (f\webright )\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X,\\ \mathrm{Im}\webleft (f\webright )\subset Y \end{gather*}

of $f$ are the underlying functors of (respectively) the induced monad and comonad of the adjunction

of Chapter 7: Constructions With Relations, Item 2 of Proposition 7.3.1.1.2.