Split equalizer (source code)

= Split equalizer
{title2=$E\xrightarrow eX\rightrightarrows Y$}

A split equalizer consists of $e:E\to X$ and $f,g:X\rightrightarrows Y$ with $fe=ge$, together with maps $r:X\to E$, $s:Y\to X$ satisfying $re=1_E$, $sf=er$, and $sg=1_X$. If $fh=gh$, these identities give $h=erh$, so $rh$ is its unique factorization through $e$. Thus it is an <equalizer>, and every <functor> preserves it: all the defining identities survive application of the functor. Interchanging $f,g$ gives the other orientation of the same convention.