Closed relation generated by a set-split pair of compact Hausdorff maps (source code)

= Closed relation generated by a set-split pair of compact Hausdorff maps

Let continuous maps $f,g:X\rightrightarrows Y$ between <compact Hausdorff spaces> have an underlying <split coequalizer> $q:Y\to Z$ with set maps $s,t$ satisfying $qs=1$, $ft=1$ and $gt=sq$. Its equivalence relation is the image of the closed subset $\{(x,x')\in X^2:g(x)=g(x')\}$ under $(f,f)$. One inclusion follows from $qf=qg$; for the other use $x=t(y)$ and $x'=t(y')$ whenever $q(y)=q(y')$. This image is compact and hence closed in the Hausdorff product $Y^2$. The quotient is therefore compact Hausdorff, giving the preserved <coequalizer> required by the <Beck monadicity theorem>.