Kernels, quotients, and function composition

$\begin{array}{cccccl} \setX & \xrightarrow[\phantom{n}]{\textstyle\functionf} & \setY & \xrightarrow{\textstyle \functiong} & \setZ && \text{(the general case)} \\ \text{Population} & \xrightarrow[\phantom{n}]{\textstyle\text{species}} & \text{Species} & \xrightarrow{\textstyle\text{genus}} & \text{Genera} && \text{(an example from biology)} \\ \text{Population} & \xrightarrow{\textstyle\text{county}} & \text{Counties} & \xrightarrow{\textstyle\text{state}} & \text{States} && \text{(an example from politics)} \\ \end{array}$ Each composable pair of functions in $\Set$,
such as those at the right,
generates a number of frequently useful diagrams in $\Set$.
Several of these are shown below.

$\Newextarrow{\xrightrightarrows}{5,5}{0x21C9}$

$\begin{array}{} && \boxed{ \begin{array}{} \functionf\Kp \\ \eltx,\eltxp \mid \eltx\functionf \xlongequal{\setY} \eltxp\functionf \\ \end{array} } & \xrightarrow{} & \setY \\ && \cap\mid & \smash{\raise1ex\hbox{$\lrcorner$}}\mkern2em & \downarrow \rlap{\Delta_\setY} \\ && \setX\times\setX & \xrightarrow{\smash{\textstyle \functionf\times\functionf}} & \setY\times\setY & \xrightarrow{\smash{\textstyle \functiong\times\functiong}} & \setZ\times\setZ \\ && {\cup}{|} & \smash{\lower1ex\hbox{$\urcorner$}}\mkern2em & {\cup}{\vert} & \smash{\lower1ex\hbox{$\urcorner$}}\mkern2em & \uparrow \rlap{\Delta_\setZ} \\ && \boxed{ \begin{array}{} (\functionf\functiong)\Kp \\ \eltx,\eltxp \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltxp\functionf\functiong \\ \end{array} } & \xrightarrow{} & \boxed{ \begin{array}{} \functiong\Kp \\ \elty,\eltyp \mid \elty\functiong \xlongequal{\setZ} \eltyp\functiong \\ \end{array} } & \xrightarrow{} & \setZ \\ & \llap{\raise2ex\hbox{$\text{inclusion}$}} \nearrow & \downdownarrows \rlap{(\functionf\functiong)\kp} && \downdownarrows \rlap{\functiong\kp} && \Vert \\ \smash{ \boxed{ \begin{array}{} \functionf\Kp \\ \eltx,\eltxp \mid \eltx\functionf \xlongequal{\setY} \eltxp\functionf \\ \end{array} } } & \xrightrightarrows[\textstyle \functionf\kp]{\smash{}} & \setX & \xrightarrow[\textstyle \functionf]{\smash{}} & \setY & \xrightarrow[\textstyle \functiong]{\smash{}} & \setZ \\ \end{array}$ First,there are the three kernel pairs $$\functionf\kp, (\functionf\functiong)\kp, \functiong\kp\; ,$$ as defined in the boxes in
the diagram of sets and functions at right.
In those boxes,
the set braces $\{,\}$ are omitted from
(the specification of the elements of the sets being defined);
on the other hand, (each equality sign) declares
(the set whose equality predicate is being used).
$\functionf\Kp$ appears twice, the first appearance as a pullback.

Second, a larger diagram of pullbacks in $\Set$, showing more about the kernel pairs, is below.
(The large square, showing a factorization of $(\functionf\functiong)\kp\functionf\functiong)$) is [the pasting composite of (four inscribed component pullback squares)];
that [(the composite square) is a pullback for (the lower and right composite $\functionf\functiong$ edges)] amounts to a two-dimensional version of (the basic pullback lemma). \[\begin{array}{} \boxed{\begin{array}{} \eltx,\eltxp \mid \eltx\functionf \xlongequal{\setY} \eltxp\functionf \\ \setX \times_\setY \setX \\ \boxed{ \functionf\Kp } \\ \end{array} } & \subseteq & \setX\times\setX & \xrightarrow{\textstyle \functionf\times\setX} & \setY\times\setX & \xrightarrow{\textstyle \pi_1} & \setX \\ \cap\mid & \searrow \rlap{\raise1ex\hbox{$\text{inclusion}$}} & \cup\mid && \cup\mid && \Vert \\ \setX\times\setX & \supseteq & \boxed{\begin{array}{} (\setX \times_\setZ \setY) \times_{(\setY\times_\setZ\setY)}(\setY \times_\setZ \setX)\\ \eltx, \eltyp, \elty, \eltxp \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltyp\functiong \land \langle \eltx\functionf,\eltyp \rangle \xlongequal{\setY\times_\setZ\setY} \langle \elty, \eltxp\functionf \rangle \land \elty\functiong \xlongequal{\setZ} \eltxp\functionf\functiong \\ \eltx,\eltxp \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltxp\functionf\functiong \\ \setX \times_\setZ \setX \\ \boxed{ (\functionf\functiong)\Kp } \\ \end{array} } & \xrightarrow{\textstyle \functionf\times_\setZ\setX} & \boxed{\begin{array}{} (\setY\times_\setZ\setY) \times_\setY \setX \\ \elty, \eltyp, \eltxp \mid \elty\functiong \xlongequal{\setZ} \eltyp\functiong \land \eltyp \xlongequal{\setY} \eltxp\functionf \\ \elty,\eltxp \mid \elty\functiong \xlongequal{\setZ} \eltxp\functionf\functiong \\ \setY \times_\setZ \setX \\ \\ \end{array} } & \xrightarrow{\textstyle \pi_1} & \setX & \ni & \eltxp \\ \llap{\setX\times\functionf} \Bigg\downarrow && \llap{\setX\times_\setZ\functionf} \Bigg\downarrow & \llap {{\raise2ex\hbox{$\lrcorner$}}\mkern1em} \searrow \rlap{\functionf\times_\setZ\functionf} & \Bigg\downarrow \rlap{\setY\times_\setZ\functionf} & \mkern-2em{\raise2ex\hbox{$\lrcorner$}} & \Bigg\downarrow \rlap\functionf \\ \setX\times\setY & \supseteq & \boxed{\begin{array}{} \setX \times_\setY (\setY\times_\setZ\setY) \\ \eltx,\elty,\eltyp \mid \eltx\functionf \xlongequal{\setY} \elty \land \elty\functiong \xlongequal{\setZ} \eltyp\functiong \\ \eltx,\eltyp \mid \eltx\functionf\functiong \xlongequal{\setZ} \eltyp\functiong \\ \setX \times_\setZ \setY \\ \\ \end{array} } & \xrightarrow{\textstyle \functionf\times_\setZ\setY} & \boxed{\begin{array}{} \\ \\ \elty,\eltyp \mid \elty\functiong \xlongequal{\setZ} \eltyp\functiong \\ \setY \times_\setZ \setY \\ \boxed{ \functiong\Kp } \\ \end{array} } & \xrightarrow{\textstyle \pi_1} & \setY & \ni & \eltyp \\ \llap{\pi_0} \Bigg\downarrow && \llap{\pi_0} \Bigg\downarrow & \mkern-10em{\raise2ex\hbox{$\lrcorner$}} & \llap{\pi_0} \Bigg\downarrow & \llap { {\raise2ex\hbox{$\lrcorner$}} \mkern3em } \searrow & \Bigg\downarrow \rlap\functiong \\ \setX & = & \setX & \xrightarrow[\textstyle \mkern.8em \functionf \mkern.8em]{} & \setY & \xrightarrow[\textstyle \mkern.8em \functiong \mkern.8em]{} & \setZ \\ &&\eltx &&\elty \\ \end{array} \]

---

Third, if, in (the above diagram), we identify (the lower $\functionf,\functiong$ edge) with (the right $\functionf,\functiong$ edge),
and omit (the two intermediate pullbacks $\setX\times_\setZ\setY$ and $\setY\times_\setZ\setX$),
we obtain (the left-hand side, i.e., the kernel pair side), of (the diagram below)
(in which, to demonstrate a possible application, $\setX \xrightarrow{\textstyle\functionf} \setY \xrightarrow{\textstyle \functiong} \setZ$ is equated to $\text{Population} \xrightarrow{\text{species}} \text{Species} \xrightarrow{\text{genus}} \text{Genera}$).
(The right-hand side, of coimages), is generated from (the left-hand side, of kernel-pairs) by (the quotient-kernel adjunction). \[\begin{array}{cccccccc} \setX\times\setX & \supseteq & \{ \eltx,\eltxp \mid \eltx\functionf = \eltxp\functionf \} & = & \functionf\Kp & \xrightrightarrows{\textstyle \functionf\kp} & (\setX = \text{Population}) & \xtwoheadrightarrow{\textstyle \functionf\coim} & \big(\functionf\Coim = \text{Population grouped by species}\big) \\ \Big\Vert && \llap{\text{inclusion}} \Big\downarrow \rlap{\text{of subsets}} && \Big\downarrow && \Big\Vert && \Big\downarrow \rlap{\text{merge operation}} \\ \setX\times\setX & \supseteq & \{ \eltx,\eltxp \mid \eltx\functionf\functiong = \eltxp\functionf\functiong \} & = & (\functionf\functiong)\Kp & \xrightrightarrows{ \smash { \textstyle (\functionf\functiong)\kp } } & (\setX = \text{Population}) & \xtwoheadrightarrow{ \smash { \textstyle (\functionf\functiong)\coim } } & \big((\functionf\functiong)\Coim = \text{Population grouped by genus}\big) \\ \llap{\functionf\times\functionf} \Big\downarrow && \Big\downarrow \rlap{\mkern-7.3em \text{restriction of $\functionf\times\functionf$}} && \Big\downarrow && \Big\downarrow \rlap{\mkern-2em (\functionf = \text{species}) } && \Big\downarrow \\ \setY\times\setY & \supseteq & \{ \elty,\eltyp \mid \elty\functiong = \eltyp\functiong \} & = & \functiong\Kp & \xrightrightarrows{ \smash { \textstyle \functiong\kp } } & (\setY = \text{Species}) & \xtwoheadrightarrow{ \smash { \textstyle \functiong\coim } } & \big(\functiong\Coim = \text{Species grouped by genus}\big) \\ && &&&& \Big\downarrow \rlap{\mkern-2em (\functiong = \text{genus}) } & \swarrow \rlap{\functiong\epsilon} \\ && &&&& (\setZ = \text{Genera}) \\ \end{array}\] Note how (the exact fork for $\functionf\functiong$) interpolates between (the exact forks for $\functionf$ and $\functiong$).
Two of the counit arrows, $\functionf\epsilon : \functionf\Coim \to \setY$ and $(\functionf\functiong)\epsilon : (\functionf\functiong)\Coim \to \setZ$, are not shown in the above diagram, due to limitations of the typesetting software.
By performing a horizontal shear on the lower two-thirds of the diagram,
and shifting $(\functionf\functiong)\Coim$ right along with what is below it, those arrows can be displayed: \[\begin{array}{cccccccc} \setX\times\setX & \supseteq & \{ \eltx,\eltxp \mid \eltx\functionf = \eltxp\functionf \} & = & \functionf\Kp & \xrightrightarrows{\textstyle \functionf\kp} & \setX & \xtwoheadrightarrow{\textstyle \functionf\coim} & \functionf\Coim \\ \Big\Vert && \llap{\text{inclusion}} \Big\downarrow \rlap{\text{of subsets}} && \Big\downarrow && \Big\Vert && & \searrow \rlap{\text{merge operation}} \\ \setX\times\setX & \supseteq & \{ \eltx,\eltxp \mid \eltx\functionf\functiong = \eltxp\functionf\functiong \} & = & (\functionf\functiong)\Kp & \xrightrightarrows{ \smash { \textstyle (\functionf\functiong)\kp } } & \setX & {} \rlap{ \mkern-2em \xtwoheadrightarrow{ \smash { \textstyle (\functionf\functiong)\coim \mkern7.6em } } } & \smash{\Bigg\downarrow \rlap{\mkern-.8em\raise2ex\hbox{$\functionf\epsilon$}}} && (\functionf\functiong)\Coim & = & (\functionf\functiong)\Coim \\ & \llap{\functionf\times\functionf} \searrow && \searrow \rlap{\mkern-7.6em \text{restriction of $\functionf\times\functionf$}} && \searrow && \searrow \rlap{\mkern-36mu \functionf = \text{species} } &&& \big\downarrow \\ && \setY\times\setY & \supseteq & \{ \elty,\eltyp \mid \elty\functiong = \eltyp\functiong \} & = & \functiong\Kp & \xrightrightarrows[ \smash { \textstyle \functiong\kp } ]{} & \setY & \xtwoheadrightarrow{ \smash { \textstyle \functiong\coim } } & \functiong\Coim && \Big\downarrow \rlap{(\functionf\functiong)\epsilon} \\ && &&&&&&& \searrow \rlap{\mkern-36mu \functiong = \text{genus} } & \downarrow \rlap{\functiong\epsilon} \\ && &&&&&&&& \setZ & = & \setZ \\ \end{array}\] The arrow from $(\functionf\functiong)\Coim$ to $\functiong\Coim$ may seem a little mysterious.
The idea is that, using the terminology of (the genus and species example),
if (two specimens have the same genus), then (their species will also have the same genus).