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[1]
    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[2][3]
    \[ 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 )$.

Item 1: As a Coequaliser
Omitted.
Item 2: As a Pushout
Omitted.
Item 3: The First Isomorphism Theorem for Sets
Clear.
Item 4: Descending Functions to Quotient Sets, I
See [Proof Wiki, Condition For Mapping From Quotient Set To Be Well Defined].
Item 5: Descending Functions to Quotient Sets, II
See [Proof Wiki, Mapping From Quotient Set When Defined Is Unique].
Item 6: Descending Functions to Quotient Sets, III
This follows from Item 5 and Item 6.
Item 7: Descending Functions to Quotient Sets, IV
See [Proof Wiki, Condition For Mapping From Quotient Set To Be An Injection].
Item 8: Descending Functions to Quotient Sets, V
See [Proof Wiki, Condition For Mapping From Quotient Set To Be A Surjection].
Item 9: Descending Functions to Quotient Sets, VI
The implication Item (a)$\implies $Item (b) is clear. Conversely, suppose that, for each $x,y\in X$, if $x\sim _{R}y$, then $f\webleft (x\webright )=f\webleft (y\webright )$. Spelling out the definition of the equivalence closure of $R$, we see that the condition $x\sim ^{\mathrm{eq}}_{R}y$ unwinds to the following:
  • There exist $\webleft (x_{1},\ldots ,x_{n}\webright )\in R^{\times n}$ satisfying at least one of the following conditions:

    1. The following conditions are satisfied:
      1. We have $x\sim _{R}x_{1}$ or $x_{1}\sim _{R}x$;
      2. We have $x_{i}\sim _{R}x_{i+1}$ or $x_{i+1}\sim _{R}x_{i}$ for each $1\leq i\leq n-1$;
      3. We have $y\sim _{R}x_{n}$ or $x_{n}\sim _{R}y$;
    2. We have $x=y$.

Now, if $x=y$, then $f\webleft (x\webright )=f\webleft (y\webright )$ trivially; otherwise, we have

\begin{align*} f\webleft (x\webright ) & = f\webleft (x_{1}\webright ),\\ f\webleft (x_{1}\webright ) & = f\webleft (x_{2}\webright ),\\ & \vdots \\ f\webleft (x_{n-1}\webright ) & = f\webleft (x_{n}\webright ),\\ f\webleft (x_{n}\webright ) & = f\webleft (y\webright ), \end{align*}

and $f\webleft (x\webright )=f\webleft (y\webright )$, as we wanted to show.


Footnotes

[1] Dually, we also have an isomorphism of sets
[2] 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 )$.
[3] 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 6: Constructions With Relations, Item 2 of Proposition 6.3.1.1.2.

Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: