Why is this the coequalizer in $\mathbf {Set}$?

Question

Take sets and functions $s,t:X\to Y$. Let $\sim$ be the equivalence relation generated by the set $R=\{(s(x),t(x)):x\in X\}$. The claim is that the pair $(Y/{\sim},\pi:Y\to Y/{\sim})$ where $\pi$ is the quotient map, is the coequalizer of $s,t$.

To prove this, we need to verify two things:

1) $\pi s=\pi t$

2) if $(C,f:Y\to C)$ is another pair with $fs=ft$, then there is a unique $g:Y/{\sim}\to C$ s.t. $g\pi=f$

For 1): For any $x\in X$, we have $\pi(s(x))=\pi(t(x))$ iff $s(x)\sim t(x)$, by the definition of $\pi$. But we do know that for all $x\in X$, $s(x)\sim t(x)$ (since $R$ contains all pairs $(s(x),t(x))$). Therefore, $\pi s=\pi t$.

For 2): Suppose there is $(C,f)$ as described above. We need to construct $g:Y/{\sim}\to C$. One natural choice would be to define $g([y])=f(y)$ — this will force $g\pi=f$. But I don't see how to prove that the map is well-defined.

Leinster says that the whole thing follows from Remark 5.2.8 (also quoted here), but I don't see how exactly everything follows. The remark says that maps $Y/{\sim}\to C$ correspond bijectively to maps $F:Y\to C$ such that $y\sim y'\implies F(y)=F(y')$.

Answer 1

To show that $g$ is well-defined, notice that $\{(y,z)\in Y\times Y:f(y)=f(z)\}$ is an equivalence relation on $Y$ that includes your $R$ as a subset. So it includes the equivalence relation $\sim$ generated by $R$ (by definition of "generated"). That is, if $y\sim z$ then $f(y)=f(z)$, which is exactly what you need to make $g$ well-defined.

Answer 2

You're spot on with the intuition here. To prove that $g$ is well defined, note that since $fs = ft$, then for any $y \sim y'$ in $Y$ we have $f(y) = f(y')$. This is a consequence of how we have defined the relation on $Y$ (it holds for the generators, which are pairs $s(x) \sim t(x)$, because $f(s(x)) = f(t(x))$. You should prove that therefore it holds for any equivalent pair of elements).

By the remark in the OP, this says that $f$ induces a map $g$ defined as $g([y]) = f(y)$, which is precisely to say that $g\pi = f$. Note that we get uniqueness for free: if we were to have another map $h$ such that $h\pi = f$ then we should have

$$ g\pi = f= h\pi, $$

and since $\pi$ is epi this says that $g = h$.

Answer 3

Here's how to use Remark 5.2.8 in Leinster's book.

Assume $(C,f:Y\to C)$ is another pair such that $fs=ft$. If we knew that $$\forall y,y'\in Y,\ y\sim y'\implies f(y)=f(y'), \tag{1}$$ then by Section 3.1 from Leinster, we would know that there is a unique well-defined map $\bar f:Y/\sim\to C$ given by $\bar f([y])=f(y)$ such that $\bar f\pi=f$. By Remark 5.2.8, to check $(1)$, it suffices to check $$\forall y,y'\in Y,\ (y,y')\in R\implies f(y)=f(y'), \tag{2}$$ i.e., it suffices to check $(1)$ not for $\sim$ but for the relation that generates $\sim$ (as pointed out in this comment). But we do know that $(2)$ holds. Indeed, if $(y,y')\in R$, then $(y,y')=(s(x_0),t(x_0))$ for some $x_0\in X$, and $f(s(x))=f(t(x))$ by assumption for all $x$ (in particular, for $x_0$). This completes the proof.