Proposition 2.1.5.1.3 (001N): Properties of Equalisers of Sets

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

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

Associativity. We have isomorphisms of sets¹

\[ \underbrace{\text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),g\circ \text{eq}\webleft (g,h\webright )\webright )}_{{}=\text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),h\circ \text{eq}\webleft (g,h\webright )\webright )}\cong \text{Eq}\webleft (f,g,h\webright ) \cong \underbrace{\text{Eq}\webleft (f\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright )}_{{}=\text{Eq}\webleft (g\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright )}, \]

where $\text{Eq}\webleft (f,g,h\webright )$ is the limit of the diagram

in $\mathsf{Sets}$, being explicitly given by

\[ \text{Eq}\webleft (f,g,h\webright )\cong \webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=g\webleft (a\webright )=h\webleft (a\webright )\webright\} . \]
Unitality. We have an isomorphism of sets
\[ \text{Eq}\webleft (f,f\webright )\cong A. \]
Commutativity. We have an isomorphism of sets
\[ \text{Eq}\webleft (f,g\webright ) \cong \text{Eq}\webleft (g,f\webright ). \]
Interaction With Composition. Let
\[ A \underset {g}{\overset {f}{\rightrightarrows }} B \underset {k}{\overset {h}{\rightrightarrows }} C \]

be functions. We have an inclusion of sets

\[ \text{Eq}\webleft (h\circ f\circ \text{eq}\webleft (f,g\webright ),k\circ g\circ \text{eq}\webleft (f,g\webright )\webright ) \subset \text{Eq}\webleft (h\circ f,k\circ g\webright ), \]

where $\text{Eq}\webleft (h\circ f\circ \text{eq}\webleft (f,g\webright ),k\circ g\circ \text{eq}\webleft (f,g\webright )\webright )$ is the equaliser of the composition

\[ \text{Eq}\webleft (f,g\webright )\overset {\text{eq}\webleft (f,g\webright )}{\hookrightarrow }A\underset {g}{\overset {f}{\rightrightarrows }}B\underset {k}{\overset {h}{\rightrightarrows }}C. \]

¹That is, the following three ways of forming “the” equaliser of $\webleft (f,g,h\webright )$ agree:

Take the equaliser of $\webleft (f,g,h\webright )$, i.e. the limit of the diagram

in $\mathsf{Sets}$.
First take the equaliser of $f$ and $g$, forming a diagram

\[ \text{Eq}\webleft (f,g\webright )\overset {\text{eq}\webleft (f,g\webright )}{\hookrightarrow }A\underset {g}{\overset {f}{\rightrightarrows }}B \]

and then take the equaliser of the composition

\[ \text{Eq}\webleft (f,g\webright )\overset {\text{eq}\webleft (f,g\webright )}{\hookrightarrow }A\underset {h}{\overset {f}{\rightrightarrows }}B, \]

obtaining a subset

\[ \text{Eq}\webleft (f\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright )=\text{Eq}\webleft (g\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright ) \]

of $\text{Eq}\webleft (f,g\webright )$.
First take the equaliser of $g$ and $h$, forming a diagram

\[ \text{Eq}\webleft (g,h\webright )\overset {\text{eq}\webleft (g,h\webright )}{\hookrightarrow }A\underset {h}{\overset {g}{\rightrightarrows }}B \]

and then take the equaliser of the composition

\[ \text{Eq}\webleft (g,h\webright )\overset {\text{eq}\webleft (g,h\webright )}{\hookrightarrow }A\underset {g}{\overset {f}{\rightrightarrows }}B, \]

obtaining a subset

\[ \text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),g\circ \text{eq}\webleft (g,h\webright )\webright )=\text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),h\circ \text{eq}\webleft (g,h\webright )\webright ) \]

of $\text{Eq}\webleft (g,h\webright )$.

Item 1: Associativity

We first prove that $\text{Eq}\webleft (f,g,h\webright )$ is indeed given by

\[ \text{Eq}\webleft (f,g,h\webright )\cong \webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=g\webleft (a\webright )=h\webleft (a\webright )\webright\} . \]

Indeed, suppose we have a diagram of the form

in $\mathsf{Sets}$. Then there exists a unique map $\phi \colon E\to \text{Eq}\webleft (f,g,h\webright )$, uniquely determined by the condition

\[ \text{eq}\webleft (f,g\webright )\circ \phi =e \]

being necessarily given by

\[ \phi \webleft (x\webright )=e\webleft (x\webright ) \]

for each $x\in E$, where we note that $e\webleft (x\webright )\in A$ indeed lies in $\text{Eq}\webleft (f,g,h\webright )$ by the condition

\[ f\circ e=g\circ e=h\circ e, \]

which gives

\[ f\webleft (e\webleft (x\webright )\webright )=g\webleft (e\webleft (x\webright )\webright )=h\webleft (e\webleft (x\webright )\webright ) \]

for each $x\in E$, so that $e\webleft (x\webright )\in \text{Eq}\webleft (f,g,h\webright )$.

We now check the equalities

\[ \text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),g\circ \text{eq}\webleft (g,h\webright )\webright )\cong \text{Eq}\webleft (f,g,h\webright ) \cong \text{Eq}\webleft (f\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright ). \]

Indeed, we have

\begin{align*} \text{Eq}\webleft (f\circ \text{eq}\webleft (g,h\webright ),g\circ \text{eq}\webleft (g,h\webright )\webright ) & \cong \webleft\{ x\in \text{Eq}\webleft (g,h\webright )\ \middle |\ \webleft [f\circ \text{eq}\webleft (g,h\webright )\webright ]\webleft (a\webright )=\webleft [g\circ \text{eq}\webleft (g,h\webright )\webright ]\webleft (a\webright )\webright\} \\ & \cong \webleft\{ x\in \text{Eq}\webleft (g,h\webright )\ \middle |\ f\webleft (a\webright )=g\webleft (a\webright )\webright\} \\ & \cong \webleft\{ x\in A\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (a\webright )$ and $g\webleft (a\webright )=h\webleft (a\webright )$}\webright\} \\ & \cong \webleft\{ x\in A\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (a\webright )=h\webleft (a\webright )$}\webright\} \\ & \cong \text{Eq}\webleft (f,g,h\webright ).\end{align*}

Similarly, we have

\begin{align*} \text{Eq}\webleft (f\circ \text{eq}\webleft (f,g\webright ),h\circ \text{eq}\webleft (f,g\webright )\webright ) & \cong \webleft\{ x\in \text{Eq}\webleft (f,g\webright )\ \middle |\ \webleft [f\circ \text{eq}\webleft (f,g\webright )\webright ]\webleft (a\webright )=\webleft [h\circ \text{eq}\webleft (f,g\webright )\webright ]\webleft (a\webright )\webright\} \\ & \cong \webleft\{ x\in \text{Eq}\webleft (f,g\webright )\ \middle |\ f\webleft (a\webright )=h\webleft (a\webright )\webright\} \\ & \cong \webleft\{ x\in A\ \middle |\ \text{$f\webleft (a\webright )=h\webleft (a\webright )$ and $f\webleft (a\webright )=g\webleft (a\webright )$}\webright\} \\ & \cong \webleft\{ x\in A\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (a\webright )=h\webleft (a\webright )$}\webright\} \\ & \cong \text{Eq}\webleft (f,g,h\webright ).\end{align*}

Item 2: Unitality

Indeed, we have

\begin{align*} \text{Eq}\webleft (f,f\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=f\webleft (a\webright )\webright\} \\ & = A. \end{align*}

Item 3: Commutativity

Indeed, we have

\begin{align*} \text{Eq}\webleft (f,g\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ a\in A\ \middle |\ f\webleft (a\webright )=g\webleft (a\webright )\webright\} \\ & = \webleft\{ a\in A\ \middle |\ g\webleft (a\webright )=f\webleft (a\webright )\webright\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Eq}\webleft (g,f\webright ). \end{align*}

Item 4: Interaction With Composition

Indeed, we have

\begin{align*} \text{Eq}\webleft (h\circ f\circ \text{eq}\webleft (f,g\webright ),k\circ g\circ \text{eq}\webleft (f,g\webright )\webright ) & \cong \webleft\{ a\in \text{Eq}\webleft (f,g\webright )\ \middle |\ h\webleft (f\webleft (a\webright )\webright )=k\webleft (g\webleft (a\webright )\webright )\webright\} \\ & \cong \webleft\{ a\in A\ \middle |\ \text{$f\webleft (a\webright )=g\webleft (a\webright )$ and $h\webleft (f\webleft (a\webright )\webright )=k\webleft (g\webleft (a\webright )\webright )$}\webright\} .\end{align*}

and

\[ \text{Eq}\webleft (h\circ f,k\circ g\webright )\cong \webleft\{ a\in A\ \middle |\ h\webleft (f\webleft (a\webright )\webright )=k\webleft (g\webleft (a\webright )\webright )\webright\} , \]

and thus there’s an inclusion from $\text{Eq}\webleft (h\circ f\circ \text{eq}\webleft (f,g\webright ),k\circ g\circ \text{eq}\webleft (f,g\webright )\webright )$ to $\text{Eq}\webleft (h\circ f,k\circ g\webright )$.