$\Newextarrow{\xrightrightarrows}{5,5}{0x21C9} \Newextarrow{\xLeftrightarrow}{2,2}{0x21D4}$
Theorem.
Let $\setX$ be (a set with two structures on it):
- (a graph $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$) having $\setX$ as its set of vertices, and
- (a function $\setX \rightcat{{}\xrightarrow{\functionf} \setY}$) from $\setX$ to another set $\setY$.
Then, referring to (the entities in the diagram below),
there exists a $u$
lifting $d_0,d_1$
through $k_0,k_1$
$u = \langle d_0,d_1 \rangle / \rightadj{\langle k_0,k_1 \rangle}$ | $\Longleftrightarrow$ |
$\leftcat{d_0}\rightcat\functionf = \leftcat{d_1}\rightcat\functionf$
the fork condition
$\leftcat{\langle d_0,d_1 \rangle} \mathrel{\class{fork}\perp} \rightcat\functionf \;$
$\leftcat{\langle d_0,d_1 \rangle} \mathrel\forktwoone \rightcat\functionf \;$ | $\Longleftrightarrow$ |
there exists a $v$
extending $\functionf$
over $\leftadj q_{\leftcat E}$
$v = \leftadj q_{\leftcat E} \backslash \functionf$ | . |
\[\bbox[10px,border:4px groove gray]{\begin{array}{c}
& \leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d_0}_{d_1}} & \setX & \leftadj{\xtwoheadrightarrow[\smash{\textstyle q_{\leftcat E}}]{\textstyle (\leftcat{d_0},\leftcat{d_1})\coequ}} &
\leftadj{(\leftcat{d_0},\leftcat{d_1})\Coequ } \mathrel{\leftadj=}
\leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E & \leftadj{\text{[right exact fork]}}\\
& \leftcat{\llap{\exists?u = \langle d_0,d_1 \rangle / {\langle k_0,k_1 \rangle}} \unicode[8,8]{x21E3}} && \Vert && \rightcat{\unicode[8,8]{x21E3} \rlap{\exists?v = \leftadj q_{\leftcat E} \backslash \functionf }}\\
\rightadj{\text{[left exact fork]}} & \{\eltx,\eltxp \mid \eltx\rightcat\functionf \mathrel{\rightcat{\xlongequal{\setY}}} \eltxp\rightcat\functionf \} \mathrel{\rightadj=} \rightcat\functionf \mathop{\rightadj\Kp} \mathrel{\rightadj=} \rightadj(\rightcat\functionf \rightadj)\rightadj\kernelreln & \rightadj{\mathop\rightrightarrows\limits^{k_0}_{k_1}} & \setX & \rightcat{\xrightarrow[\smash{\textstyle \functionf}]{}} & \rightcat \setY\\
\end{array}}\]
Further, since (
$k_0,k_1$ are jointly monic),
(the lift $u$) is unique if (it exists),
and, since ($\leftadj q_{\leftcat E}$ is epic),
(the extension $v$) is unique if (it exists).
Proof:
If ($\leftcat{d_0}\rightcat f = \leftcat{d_1}\rightcat f$)
then (the existence of a unique $u$ lifting $d_0,d_1$ through $k_0,k_1$)
is simply (the universal property of
the kernel relation (which is also known as the “kernel pair”) of $\rightcat f$).
Conversely, if (such a lift $u$ exists), then we have
$$\leftcat{d_0}\rightcat f \mathrel{\leftcat{\xlongequal{\text{lift}}}} \leftcat u\rightadj{k_0}\rightcat f \mathrel{\rightadj{\xlongequal{\rightadj{\langle k_0,k_1 \rangle} \mathrel\forktwoone \rightcat f}}} \leftcat u\rightadj{k_1}\rightcat f \mathrel{\leftcat{\xlongequal{\text{lift}}}} \leftcat{d_1}\rightcat f\quad.$$
The argument for the quotient (also known as the coequalizer) of the parallel pair
is entirely analogous, using the universal property of the coequalizer. QED.
This topic is also discussed at nlab’s discussion of quotient object,
see especially Proposition 1 there.
The discussion in this document is of the more general case,
where $\leftcat E$ is (merely a graph), not necessarily (an equivalence relation or a congruence).
(The diagram above) can be expanded to show [the factorization of $\leftcat u$ and $\rightcat v$
through (the unit and counit of the adjunction)]:
\[\bbox[10px,border:4px groove red]{\begin{array}{c}
\leftcat E & \leftcat= & \leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d_0^E}_{d_1^E}} & \setX & \leftadj{\xtwoheadrightarrow{q_{\leftcat E}}} & \leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} & \leftadj= & \leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0}\\
&&\leftadj{\llap{\eta_{\rightcat E}}\downarrow} & \leftadj{\text{[unit for $\leftcat E$]}} & \Vert &&&& \\
&& \rightadj(\leftadj{q_{\leftcat E}}\rightadj)\rightadj\kernelreln & \rightadj{\mathop\rightrightarrows\limits^{k_0^{\leftadj q_{\rightcat E}}}_{k_1^{\leftadj q_{\rightcat E}}}} & \setX && \rightcat{\Big\downarrow} \rlap{\leftadj(\leftcat u\leftadj,\setX\leftadj{)\pi_0}}\\
\leftcat{\llap u\Bigg\downarrow} &&&& \Vert &&&& \rightcat{\Bigg\downarrow\rlap v}\\
&& \llap{\rightadj(\rightcat v\rightadj)\rightadj\kernelreln}\leftcat{\Big\downarrow} && \setX & \leftadj{\xtwoheadrightarrow[\textstyle \text{coimage for } \rightcat f]{\textstyle q_{\rightadj(\rightcat f\rightadj)\rightadj\kernelreln}}} & \leftadj{\bigl(}\rightadj(\rightcat f\rightadj)\rightadj\kernelreln\leftadj,\setX\leftadj{\bigr)\pi_0}\\
&&&& \Vert & \rightadj{\text{[counit for $\rightcat f$]}} & \rightadj{\downarrow\rlap{\epsilon_{\rightcat f}}}\\
\rightadj(\rightcat f\rightadj)\rightadj\kernelreln & \rightadj= & \rightadj(\rightcat f\rightadj)\rightadj\kernelreln & \rightadj{\mathop\rightrightarrows\limits^{k_0^{\rightcat f}}_{k_1^{\rightcat f}}} & \setX & {}\rlap{\rightcat{\mkern-3.5em \xrightarrow[\textstyle \functionf]{\mkern15em}}} & \rightcat \setY & = & \rightcat \setY\\
\end{array}}\]
| $\leftcat E \leftadj\eta$ | is defined by the right universal property of | $\leftcat E \ladjQ \radjK$ | applied to | $\leftcat E$ | $\forktwoone$ | $\leftcat E \ladjQ$ . |
| $\rightcat v \radjK$ | is defined by the right universal property of | $\rightcat f \radjK$ | applied to | $\leftcat E \ladjQ \radjK$ | $\forktwoone$ | $\rightcat{\big(f = \black(\leftcat E \ladjQ\black) \circ v \big)}$ . |
| $\leftcat u$ | is defined by the right universal property of | $\rightcat f \radjK$ | applied to | $\leftcat E$ | $\forktwoone$ | $\rightcat{\big(f = \black(\leftcat E \ladjQ\black) \circ v \big)}$ . |
| $\rightcat f \rightadj\epsilon$ | is defined by the left universal property of | $\rightcat f \radjK \ladjQ$ | applied to | $\rightcat f\radjK$ | $\forktwoone$ | $\rightcat f$ . |
| $\leftcat u \ladjQ$ | is defined by the left universal property of | $\leftcat E \ladjQ$ | applied to | $\leftcat{\big(E = u \circ \black(\rightcat f \radjK\black)\big)}$ | $\forktwoone$ | $\rightcat f \radjK \ladjQ$ . |
| $\rightcat v$ | is defined by the left universal property of | $\leftcat E \ladjQ$ | applied to | $\leftcat{\big(E = u \circ \black(\rightcat f \radjK\black)\big)}$ | $\forktwoone$ | $\rightcat f$ . |
The adjunction where
(the graph on $\setX$) is
(the projection $\pi:\setX\times G\to \setX$) and (action $\nu:\setX\times G\to \setX$)
of (a group $G$) acting on $\setX$.
\[\begin{array}{c}
\leftcat{\llap{E = {}} \setX \times G} & \leftcat{\mathop\rightrightarrows\limits^\pi_\nu} & \setX & \leftadj{\xtwoheadrightarrow q} & \setX\leftadj/G \\
\leftcat{\llap{(\forall x\in \setX)(\forall g\in G)\bigl(x\rightcat f=(xg)\rightcat f\bigr)}\big\downarrow} && \big\Vert && \rightcat{\big\downarrow}\\
\rightadj(\rightcat f\rightadj) \rightadj\kernelreln & \rightadj\rightrightarrows & \setX & \rightcat{\mathop\longrightarrow\limits^f} & \rightcat \setY\\
\end{array}\]
The above showing the factorization through the counit of the adjunction.
\[\begin{array}{c}
\leftcat{\llap{E = {}} \setX \times G} & \leftcat{\mathop\rightrightarrows\limits^\pi_\nu} & \setX & \leftadj{\xtwoheadrightarrow q} & \setX\leftadj/G & \leftadj= & \setX\leftadj/G \\
\leftcat{\llap{(\forall x\in \setX)(\forall g\in G)\bigl(x\rightcat f=(xg)\rightcat f\bigr)}\big\downarrow} && \big\Vert && \rightcat{\big\downarrow\rlap{\scriptstyle(\forall x\in \setX)\bigl(xG \subseteq xff^{-1}\bigr)}} && \rightcat{\big\downarrow}\\
\rightadj(\rightcat f\rightadj) \rightadj\kernelreln & \rightadj\rightrightarrows & \setX & \leftadj{\xtwoheadrightarrow{q}} & \leftadj(\rightcat f\leftadj) \leftadj\kernelpart & \rightadj{\mathop\rightarrowtail\limits^{\epsilon_{\rightcat f}}} & \rightcat \setY\\
\big\Vert && \big\Vert &&&& \rightcat{\big\Vert}\\
\rightadj(\rightcat f\rightadj) \rightadj\kernelreln & \rightadj\rightrightarrows & \setX & {} \rlap{\rightcat{\mkern-1em \xrightarrow[\functionf]{\mkern16em}}} &&& \rightcat \setY\\
\end{array}\]
An example of the quotient-kernel adjunction:
| The left arrow $u$ in $\graphsoverx$ |
The fork |
The right arrow $v$ in $\setsunderx$ |
| \[\begin{array}{c}
\leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d_0}_{d_1}} & \setX\\
\leftcat{\llap{u}\big\downarrow} && \big\Vert\\
\rightadj(\rightcat f\rightadj)\rightadj\kernelreln & \rightadj{\mathop\rightrightarrows\limits^{k_0}_{k_1}} & \setX
\end{array}\] |
\[\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX \rightcat{{}\xrightarrow{f} \setY}\] |
\[\begin{array}{c}
\setX & \leftadj{\mathop\twoheadrightarrow\limits^{q_{\leftcat E}}} & \leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E\\
\big\Vert && \rightcat{\big\downarrow\rlap{v}}\\
\setX & \rightcat{\mathop\longrightarrow\limits^f} & \rightcat \setY\\
\end{array}\] |
| \[\begin{array}{c}
\leftcat u & 0 & 1 & 2 & 3 & 4\\
0 & \rightadj{\text{KR}} & \leftcat e \atop \rightadj{\text{KR}} & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \\
1 & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \leftcat {e'} \atop \rightadj{\text{KR}} & \rightadj{\text{KR}} & \\
2 & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \\
3 & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \rightadj{\text{KR}} & \\
4 & & & & & \rightadj{\text{KR}}
\end{array}\] |
\[\begin{array}{c}
[5] & : & 0 & \leftcat{\xrightarrow{e \in E}} & 1 & \leftcat{\xrightarrow{e' \in E}} & 2 && 3 && 4\\
\rightcat{\llap f \downarrow} & \rightcat: & \rightcat\downarrow && \rightcat\downarrow && \rightcat\downarrow && \rightcat\downarrow && \rightcat\downarrow\\
\rightcat{\{a,b,c\}} & \rightcat: & \rightcat a & \rightcat = & \rightcat a & \rightcat = & \rightcat a & \rightcat = & \rightcat a & \phantom= & \rightcat b & \phantom= & \rightcat c
\end{array}\] |
\[\begin{array}{c}
[5] & : & 0 & 1 & 2 & 3 & 4\\
\leftadj{\llap{q_{\leftcat E}}\downarrow} & \leftadj: & \leftadj\searrow & \leftadj\downarrow & \leftadj\swarrow & \leftadj\downarrow & \leftadj\downarrow\\
\leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E & \leftadj: & & \leftadj{\{0,1,2\}} && \leftadj{\{3\}} & \leftadj{\{4\}}\\
\rightcat{\llap v \downarrow \rlap{\leftadj q_{\leftcat E} \backslash f}} & \rightcat: && \rightcat\searrow && \rightcat\swarrow & \rightcat\downarrow\\
\rightcat{\{a,b,c\}} & \rightcat: &&& \rightcat a && \rightcat b & \rightcat c
\end{array}\] |
An expansion of the example showing the factorization through
the unit $\eta_{\leftcat E}$ of the adjunction:
| \[\begin{array}{c}
\leftcat E & \leftcat= & \leftcat E & \leftcat= & \leftcat E\\
&&&& \leftadj{\downarrow\rlap{\eta_{\leftcat E}}}\\
&& \leftcat{\llap{u}\Bigg\downarrow} && \leftcat{E^\ast} = \rightadj(\leftadj{q_{\leftcat E}}\rightadj)\rightadj\kernelreln\\
\leftcat{\llap{d_0^E}\downdownarrows\rlap{d_1^E}} &&&& \rightcat\downarrow\rlap{\rightadj(\rightcat v\rightadj)\rightadj\kernelreln}\\
&& \rightadj(\rightcat f\rightadj)\rightadj\kernelreln & \rightadj= & \rightadj(\rightcat f\rightadj)\rightadj\kernelreln\\
&&& \rightadj{\llap{k_0^{\rightcat f}}\downdownarrows\rlap{k_1^{\rightcat f}}}\\
\setX && = & \setX\\
\rightcat{\llap f \downarrow}\\
\rightcat \setY\\
\end{array}\] |
\[\begin{array}{c}
& 0 & 1 & 2 & 3 && 4\\
0 & \leftcat{1_0\in E^\ast}\rightcat\subseteq \radjK & \leftcat{\boxed e\in E\leftadj{\mathop\subseteq\limits^{\eta_{\leftcat E}}} E^\ast}\rightcat\subseteq \radjK & \leftcat{ee'\in E^\ast}\rightcat\subseteq \radjK & \radjK & \\
1 & \leftcat{e^{-1}\in E^\ast}\rightcat\subseteq \radjK & \leftcat{1_1\in E^\ast}\rightcat\subseteq \radjK & \leftcat{\boxed{e'}\in E\leftadj{\mathop\subseteq\limits^{\eta_{\leftcat E}}} E^\ast}\rightcat\subseteq \radjK & \radjK & \\
2 & \leftcat{(ee')^{-1}\in E^\ast}\rightcat\subseteq \radjK & \leftcat{e'^{-1}\in E^\ast}\rightcat\subseteq \radjK & \leftcat{1_2\in E^\ast}\rightcat\subseteq \radjK & \radjK & \\
3 & \radjK & \radjK & \radjK & \radjK &\\
4 &&&&&& \radjK
\end{array}\] |
An expansion of the example showing the factorization through
the counit $\epsilon_{\rightcat f}$ of the adjunction:
\[\begin{array}{c}
[5] && = & [5] & = & [5] & : & 0 & 1 & 2 & 3 & 4\\
&&& \leftadj{\big\downarrow \rlap{\leftcat E \ladjQ}} &&& \leftadj: & \leftadj\searrow & \leftadj\downarrow & \leftadj\swarrow & \leftadj\downarrow & \leftadj\downarrow\\
&& \setX\leftadj/\leftcat E & = & \leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} & \leftadj{\Bigg\downarrow}\rlap{\rightcat f \radjK \ladjQ} & \leftadj: & & \leftadj{\{0,1,2\}} && \leftadj{\{3\}} & \leftadj{\{4\}}\\
\rightcat{\llap f\Bigg\downarrow} &&&& \llap{\setX\leftadj/\leftcat u \,} \leftcat{\big\downarrow} \rlap{\leftcat u \ladjQ} && \rightcat: && \rightcat\searrow && \rightcat\swarrow & \rightcat\downarrow\\
&& \rightcat{\llap v\bigg\downarrow} && \leftadj{\bigl(}\rightadj(\rightcat f\rightadj)\rightadj\kernelreln\leftadj,\setX\leftadj{\bigr)\pi_0} & & \leftadj: &&& \leftadj{\{0,1,2,3\}} && \leftadj{\{4\}}\\
&&&&& \rightadj{\big\downarrow\rlap{\rightcat f \epsilon}} & \rightadj: &&& \rightadj\downarrow && \rightadj\downarrow \\
\rightcat{\{a,b,c\}} & = & \rightcat{\{a,b,c\}} && = & \rightcat{\{a,b,c\}} & \rightcat: &&& \rightcat a && \rightcat b && \rightcat c\\
\end{array}\]
On the right of the above diagram, to the right of the $:$'s,
is the "internal diagram",
a forest showing the elements of the various sets and what they map to.
To the left of the $:$'s is the "external diagram",
a diagram of sets and functions in the category $\Set$.
We can step up to a third level of description by showing this situation
in the 2-category $\CAT$:
\[\begin{array}{}
\cati && \leftcat{\buildrel \textstyle E \over \longrightarrow} && \graphsoverx && \\
& \rightcat{\llap{\lower4pt\hbox{$f\!\!\!$}} \searrow} & \leftcat{\Big\Downarrow \rlap u} & \rightadj{\nearrow\rlap{\lower5pt\hbox{$\!\!\!\!\!K$}}} & \rightadj{\Big\Downarrow\rlap\epsilon} & \leftadj{\searrow\rlap{\raise4pt\hbox{$\!\!\!\!Q$}}} &\\
&& \setsunderx && \rightcat\longrightarrow && \setsunderx\\
\end{array}\]
Cf. what this 2-categorical diagram amounts to in $\Set$.
\[\begin{array}{}
\setX & \leftadj{\xtwoheadrightarrow{\textstyle \leftcat E Q}} & \leftadj(\rightcat E\leftadj,\,\setX\leftadj)\leftadj{\pi_0}\\
\rightcat{\llap f\Bigg\downarrow} & \leftadj\searrow\rlap{\raise5pt\hbox{$\!\!\!\rightcat f \radjK \ladjQ$}} & \leftcat{\Bigg\downarrow\rlap{u\ladjQ}}\\
\rightcat \setY & \rightadj{\xleftarrow[\textstyle \rightcat f \epsilon]{}} & \leftadj(\rightcat f\radjK\leftadj,\,\setX\leftadj)\leftadj{\pi_0}\\
\end{array} \quad = \qquad
\begin{array}{}
\setX & \leftadj{\xtwoheadrightarrow{\textstyle \leftcat E Q}} & \leftadj(\rightcat E\leftadj,\,\setX\leftadj)\leftadj{\pi_0}\\
\rightcat{\llap f\Bigg\downarrow} & \rightcat{\swarrow\rlap{\!\! v}} & \leftcat{\Bigg\downarrow\rlap{u\ladjQ}}\\
\rightcat \setY & \rightadj{\xleftarrow[\textstyle \rightcat f \epsilon]{}} & \leftadj(\rightcat f\radjK\leftadj,\,\setX\leftadj)\leftadj{\pi_0}\\
\end{array}
\]
Here we present the diagram of large categories, functors, and natural transfomations
which the quotient-kernel adjunction defines
in $\CAT$, the very large category of large categories.
For brevity,
the names of the
left (quotient) and
right (kernel-relation) adjoint functors
are abbreviated to $\ladjQ$ and $\radjK$.
First just the data :
\[\begin{array}{c}
\graphsoverx & \leftadj{\xrightarrow{Q}} & \setsunderx\\
\llap{\leftcat 1_\graphsoverx}\leftcat\Vert & \leftadj{\eta\Rightarrow} \qquad \leftcat{\epsilon\Rightarrow} & \rightcat\Vert\rlap{\rightcat 1_\setsunderx}\\
\leftcat{\graphsoverx} & \rightadj{\xleftarrow[K]{}} & \rightcat{\setsunderx}\\
\end{array}\]
Now the data expanded to show the composites that appear in the triangle identities:
\[\begin{array}{}
&& \graphsoverx && \xrightarrow{\mkern3em} && \graphsoverx \\
& \rightadj{\llap\radjK \nearrow} & \rightadj{\Big\Downarrow\rlap\epsilon} & \leftadj{\searrow\rlap\ladjQ} & \leftadj{\Big\Downarrow \rlap\eta} & \rightadj{\nearrow\rlap\radjK} & \rightadj{\Big\Downarrow \rlap\epsilon} & \leftadj{\searrow\rlap\ladjQ} \\
\setsunderx && \xrightarrow[\mkern3em]{} && \setsunderx && \xrightarrow[\mkern3em]{} && \setsunderx \\
\end{array}\]
In the above $\graphsoverx$ is the category of (
graphs over $\setX$) (i.e., graphs having $\setX$ as their sets of vertices),
and $\setsunderx$ is the
under category of (
sets under $\setX$).
The functorality of $\radjK$ and $\ladjQ$
\[\begin{array}{}
&\leftcat{\buildrel E \over \rightrightarrows} & \setX & \leftadj{\xtwoheadrightarrow{\leftcat E Q}} &\\
\leftcat{\llap u\Big\downarrow} && \Big\Vert && \llap{\exists!} \leftadj{\Big\downarrow\rlap{\leftcat u Q}}\\
&\leftcat{\mathop\rightrightarrows\limits_F} & \setX & \leftadj{\xtwoheadrightarrow[\leftcat F Q]{}} &\\
\end{array}
\Space{6em}{0ex}{0ex}
\begin{array}{}
&\rightadj{\buildrel \rightcat f K \over \rightrightarrows} & \setX & \rightcat{\xrightarrow f} &\\
\llap{\exists!} \rightadj{\Big\downarrow\rlap{\rightcat v K}} && \Big\Vert && \rightcat{\Big\downarrow\rlap v}\\
&\rightadj{\mathop\rightrightarrows\limits_{\rightcat g K}} & \setX & \rightcat{\xrightarrow[g]{}} &\\
\end{array}\]
For a quick look at the way the universal properties of $\radjK$ and $\ladjQ$ on objects
enable them to act on arrows as well, see the diagrams at right.
| $\leftcat u \ladjQ$ | is defined by the left universal property of | $\leftcat E \ladjQ$ | applied to | $\leftcat{(E = u \circ F)}$ | $\forktwoone$ | $\leftcat F \ladjQ$ . |
| $\rightcat v \radjK$ | is defined by the right universal property of | $\rightcat g \radjK$ | applied to | $\rightcat f \radjK$ | $\forktwoone$ | $\rightcat{ (g = f \circ v ) }$ . |
(Some related facts are in Section 3 of the paper by Ross Street, “The Core of Adjoint Functors”.)
$\radjK \ladjQ \radjK \mathrel{\rightadj\cong} \radjK$ and $\ladjQ \radjK \ladjQ \mathrel{\leftadj\cong} \ladjQ$
For the isomorphism featuring $\radjK$, we offer three independent proofs,
each featuring a different aspect of the situation.
First, a proof using the unit and counit of the adjunction.
Consider the commutative diagram
(where (the corners of the diagram) are determined by (the horizontal arrows that abut them))
\[\begin{array}{}
& \rightadj{\xrightrightarrows{\textstyle \rightcat f \radjK \ladjQ \radjK}} & \setX & \leftadj{\xtwoheadrightarrow{\textstyle \rightcat f \radjK \ladjQ}}\\
\llap{\rightcat f \radjK \leftadj\eta} \leftadj{\Bigg\uparrow} \lower1.7ex\hbox{$\rightadj\parallel$} \rightadj{\Bigg\downarrow} \rlap{\rightcat f \rightadj\epsilon \radjK} && \Bigg\Vert && \rightadj{\Bigg\downarrow} \rlap{\rightcat f \rightadj\epsilon}\\
& \rightadj{\xrightrightarrows[\textstyle \rightcat f\radjK]{}} & \setX & \rightcat{\xrightarrow[\textstyle f]{}} & \\
\end{array}\]
| $\rightcat f \rightadj\epsilon$ | is defined by the left universal property of | $\rightcat f \radjK \ladjQ$ | applied to | $\rightcat f\radjK$ | $\forktwoone$ | $\rightcat f$ . |
| $\rightcat f \rightadj\epsilon \radjK$ | is defined by the right universal property of | $\rightcat f\radjK$ | applied to | $\rightcat f \radjK \ladjQ \radjK$ | $\forktwoone$ | $\bigl( \rightcat f = (\rightcat f \radjK \ladjQ) \circ (\rightcat f \rightadj\epsilon) \bigr)$ . |
| $\rightcat f \radjK \leftadj\eta$ | is defined by the right universal property of | $\rightcat f \radjK \ladjQ \radjK$ | applied to | $\rightcat f \radjK$ | $\forktwoone$ | $\rightcat f \radjK \ladjQ$ . |
That $(\rightcat f \radjK \leftadj\eta)\circ(\rightcat f \rightadj\epsilon \radjK) \mathrel{\rightadj=} \text{identity}$ and $(\rightcat f \rightadj\epsilon \radjK)\circ(\rightcat f \radjK \leftadj\eta) \mathrel{\rightadj=} \text{identity}$
follows from the facts that
$\rightcat f \radjK \leftadj\eta$ and $\rightcat f \rightadj\epsilon \radjK$ are morphisms in $\graphsoverx$
and each of the parallel pairs $\rightcat f \radjK \ladjQ \radjK$ and $\rightcat f \radjK$ is jointly monic in $\Set$.
So $\rightcat f \radjK \leftadj\eta$ and $\rightcat f \rightadj\epsilon \radjK$ are inverse to each other,
providing an isomorphism in $\graphsoverx$ between $\rightcat f\radjK$ and $\rightcat f \radjK \ladjQ \radjK$.
\[\begin{array}{}
\leftcat E & \leftcat{\mathop\rightrightarrows\limits^{d_0}_{d_1}} & \setX & \leftadj{\xtwoheadrightarrow{\textstyle \rightcat f \radjK \ladjQ}}\\
&& \Bigg\Vert && \rightadj{\Bigg\downarrow} \rlap{\rightcat f \rightadj\epsilon} & \\
& \lower4pt\hbox{$\rightadj{\begin{smallmatrix} \xrightarrow{} \\ \xrightarrow[\textstyle \rightcat f\radjK]{} \end{smallmatrix}}$} & \setX & \rightcat{\xrightarrow[\textstyle f]{}} & \\
\end{array}\]
Second, a proof that shows $\rightcat f\radjK$ satisfies
the right universal property that defines $\rightcat f \radjK \ladjQ \radjK$.
When $\leftcat{E \mathrel{\mathop\rightrightarrows\limits^{d_0}_{d_1}} {}} \setX$ is an arbitary fork for $\rightcat f \radjK \ladjQ$, i.e., $\leftcat{\langle d_0,d_1 \rangle} \mathrel\forktwoone \rightcat f \radjK \ladjQ$,
consider the diagram at right:
$\leftcat{\langle d_0,d_1 \rangle} \mathrel\forktwoone \rightcat f \radjK \ladjQ$ implies
$\leftcat{\langle d_0,d_1 \rangle} \mathrel\forktwoone \bigl( (\rightcat f \radjK \ladjQ) \circ (\rightcat f \rightadj\epsilon) = \rightcat f \bigr)$.
Thus the (
the right universal property of $\rightcat f\radjK$) implies
there exists a unique (lift of $\leftcat{\langle d_0,d_1 \rangle}$ through $\rightcat f\radjK$),
showing that $\rightcat f\radjK$ satisfies (
the right universal property which defines $\rightcat f \radjK \ladjQ \radjK$).
The above two proofs used categorial methods.
They readily generalize to categories with kernel pairs and coequalizers,
including notably the regular categories.
Now we provide a proof using a strictly set-theoretical method, using elements.
The proof amounts to simply unwinding the set-theoretical definitions.
The following statements are logically equivalent:
| $\langle x,x'\rangle \in \rightcat f \radjK \ladjQ \radjK$ | (in $\setX \times \setX$) |
| $x(\rightcat f \radjK \ladjQ) = x'(\rightcat f \radjK \ladjQ)$ | (in the target set (codomain) of $\rightcat f \radjK \ladjQ$) |
| $\langle x,x'\rangle \in \rightcat f \radjK$ | (in $\setX \times \setX$;
this step uses that $\rightcat f \radjK$ is already an equivalence relation) |
| $x\rightcat f = x'\rightcat f$ | (in the target set (codomain) of $\rightcat f$) |
The logical equivalence of the first and third statements shows that
$\rightcat f \radjK \ladjQ \radjK = \rightcat f \radjK$ as subsets of $\setX\times \setX$;
the fourth statement is provided simply as a reminder of the definition of $\rightcat f \radjK$.
Finally, the proof that $\ladjQ \radjK \ladjQ \mathrel{\leftadj\cong} \ladjQ$ is left as an exercise.
Emulate any one of the above three proofs for the other isomorphism.
The following is just some discussion, not really important.
The setting for this very important adjunction is both simple and ubiquitous.
We have a set $\setX$ with two structures on it:
- a graph $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$ having $\setX$ as its set of vertices, and
- a function $\setX \rightcat{{}\xrightarrow{f} \setY}$ from $\setX$ to another set $\setY$.
A (the?) natural question then is, might there be a relation between those two structures?
I suppose there could be many possible relations,
but a commonly considered relation, and the one considered in this document,
occurs when we combine those two structures into a single diagram
\[\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX \rightcat{{}\xrightarrow{f} \setY}\]
and the two composites $\leftcat{d_0}\rightcat f$ and $\leftcat{d_1}\rightcat f$ are then equal: $\leftcat{d_0}\rightcat f = \leftcat{d_1}\rightcat f$.
In that case we say that the diagram forms a fork.
(To aid our understanding of this situation, it may be useful to describe what that means in words:
If $x,x'\in \setX$ are connected by an edge $e\in E$, then $x\rightcat f = x'\rightcat f$.
In other words, $\rightcat f$ is constant on vertices connected by edges.
And this holds not just for elements of $\setX$ connected by a single edge.
If there is a string (often called a path) of edges in $E$ connecting $x$ to $x'$,
then again, $x\rightcat f = x'\rightcat f$.
So $\rightcat f$ is constant on connected components of the graph $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}} \setX$.)
The fork condition is a relation between the graph $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$ and the function $\setX \rightcat{{}\xrightarrow{f} \setY}$.
We can fix either one of those elements and consider the class of elements on the other side that bear the fork relation to the fixed element.
In each case, it turns out that there is an element on the other side which is “closest” in a suitable sense to the fixed element.
To establish what “closest” means it is useful to put a category structure on all the possibilities for each of the two structures considered.
First we consider the graphs over $\setX$.
An arrow between two such graphs is an arrow such as $\leftcat u$ in the diagram below which commutes with the structure arrows of the graphs, i.e., $ud^{E'}_0 = d^E_0$ and $ud^{E'}_1 = d^E_1$.
\[\begin{array}{c}
\leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d^E_0}_{d^E_1}} & \setX\\
\leftcat{\llap{u}\Big\downarrow} && \Big\Vert\\
\leftcat E' & \leftcat {\mathop\rightrightarrows\limits^{d^{E'}_0}_{d^{E'}_1}} & \setX\\
\end{array}\]
In terms of elements, that means that
if $x \xrightarrow{e} x'$ is an edge in $E$,
with initial and final vertices as indicated,
then $xu \rightarrow{eu} x'u$ is an edge in $E'$.
With that definition of arrow, the graphs over $\setX$ form a category.
It has an initial object, the empty graph, and a terminal object, the graph $\setX \mathop\rightrightarrows\limits^{1_\setX}_{1_\setX} \setX$.
Let us fix a function $\setX \rightcat{{}\xrightarrow{f} \setY}$
and consider the full subcategory of the graphs over $\setX$ determined by
those which are in a fork relation with $\setX \rightcat{{}\xrightarrow{f} \setY}$.
Among them is
$$\rightadj(\rightcat f\rightadj)\rightadj\kernelreln \mathrel{\rightadj{\mathop\rightrightarrows\limits^{d_0}_{d_1}}} \setX\;,$$
and in fact it is the terminal object for that subcategory.
Thus for every graph $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$ forking $\rightcat f$
we have a unique arrow of graphs $\leftcat u$ as in the left part of the diagram below.
\[\begin{array}{c}
& \leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d_0}_{d_1}} & \setX & \leftadj{\xtwoheadrightarrow{q_{\leftcat E}}} & \leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E & \leftadj{\text{[right exact fork]}}\\
& \leftcat{\llap{u}\Big\downarrow} && \Big\Vert && \rightcat{\Big\downarrow\rlap{v}}\\
\rightadj{\text{[left exact fork]}} & \rightadj(\rightcat f\rightadj)\rightadj\kernelreln & \rightadj{\mathop\rightrightarrows\limits^{k_0}_{k_1}} & \setX & \rightcat{\xrightarrow f} & \rightcat \setY\\
\end{array}\]
Similarly we have the standard definition of arrows under $\setX$ forming a co-slice category $\setX\downarrow\Set$.
If we consider a fixed graph over $\setX$, $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$,
we may consider the subcategory of $\setX\downarrow\Set$
of (functions out of $\setX$ which form a fork with $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$).
That subcategory has an initial object,
$$\setX \leftadj{{} \xtwoheadrightarrow{q_{\leftcat E}} {}} \leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E\;,$$
so that for every other (function out of $\setX$ which forms a fork with $\leftcat{E \mathop\rightrightarrows\limits^{d_0}_{d_1}{}} \setX$)
there is a unique (arrow $\rightcat v$ in $\setX\downarrow\Set$)
which makes (the right part of the diagram above commute).
An extension
The key idea is that we replace (the vertical equality $\setX=\setX$) (in the diagram describing the original adjunction) with (a function, say $\setX \xrightarrow{\textstyle\functionf} \setY$).
Renaming, to avoid confusion, (the arrow $\setX \rightcat{{}\xrightarrow{\textstyle \functionf} \setY}$ in the original adjunction) to ($\setY \rightcat{{}\xrightarrow{\textstyle \functiong} \setZ}$), (the extended adjunction diagram) then becomes:
\[\bbox[10px,border:4px groove gray]{\begin{array}{c}
& \leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d_0}_{d_1}} & \setX & \leftadj{\xtwoheadrightarrow[\smash{\textstyle q_{\leftcat E}}]{\textstyle \langle \leftcat{d_0},\leftcat{d_1} \rangle \coequ}} &
\leftadj{ \langle \leftcat{d_0},\leftcat{d_1} \rangle \Coequ } \mathrel{\leftadj=}
\leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E & \leftadj{\text{[right exact fork]}} \\
& \leftcat{\llap{\exists?u = \big(\langle d_0,d_1 \rangle \functionf\big) \big/ \rightadj{\big(}\rightcat\functiong\mathop{\rightadj\kp}\rightadj{\big)} } \unicode[8,8]{x21E3}} && \Bigg\downarrow \rlap\functionf && \rightcat{\unicode[8,8]{x21E3} \rlap{\exists?v = \leftadj q_{\leftcat E} \backslash (\functionf\functiong) }}\\
\rightadj{\text{[left exact fork]}} & \{\elty,\eltyp \mid \elty\rightcat\functiong \mathrel{\rightcat{\xlongequal{\setZ}}} \eltyp\rightcat\functiong \} \mathrel{\rightadj=} \rightcat\functiong\mathop{\rightadj\Kp} \mathrel{\rightadj=} \rightadj(\rightcat\functiong \rightadj)\rightadj\kernelreln & \xrightrightarrows[\textstyle \rightcat\functiong\mathop{\rightadj\kp}]{}
& \setY & \rightcat{\xrightarrow[\smash{\textstyle \functiong}]{}} & \rightcat \setZ \\
\end{array}}\]
To prove this, we consider (the diagram shown below), apply (the original adjunction) to (this new diagram), then (relate $(\functionf\rightcat\functiong)\mathop{\rightadj\Kp}$ to $\rightcat\functiong\mathop{\rightadj\Kp}$).
\[\mkern-3em \bbox[10px,border:4px groove gray]{\begin{array}{c}
& \leftcat E & \leftcat {\mathop\rightrightarrows\limits^{d_0}_{d_1}} & \setX & \leftadj{\xtwoheadrightarrow[\smash{\textstyle q_{\leftcat E}}]{\textstyle \langle \leftcat{d_0},\leftcat{d_1} \rangle \coequ}} &
\leftadj{ \langle \leftcat{d_0},\leftcat{d_1} \rangle \Coequ } \mathrel{\leftadj=}
\leftadj(\leftcat E\leftadj,\setX\leftadj{)\pi_0} \mathrel{\leftadj=} \setX\leftadj/\leftcat E & \leftadj{\text{[right exact fork]}} \\
& \leftcat{\llap{\exists?u = \langle d_0,d_1 \rangle \big/ \rightadj{\big((}\functionf\rightcat\functiong\rightadj)\mathop{\rightadj\kp}\rightadj{\big)} } \unicode[8,8]{x21E3}} && \Bigg\Vert && \rightcat{\unicode[8,8]{x21E3} \rlap{\exists?v = \leftadj q_{\leftcat E} \backslash (\functionf\functiong) }}\\
\rightadj{\text{[left exact fork]}} & \{\eltx,\eltxp \mid \eltx\functionf\rightcat\functiong \mathrel{\rightcat{\xlongequal{\setZ}}} \eltxp\functionf\rightcat\functiong \} \mathrel{\rightadj=} (\functionf\rightcat\functiong)\mathop{\rightadj\Kp} \mathrel{\rightadj=} \rightadj(\functionf\rightcat\functiong \rightadj)\rightadj\kernelreln & \xrightrightarrows[\textstyle \rightadj(\functionf\rightcat\functiong\rightadj) \mathop{\rightadj\kp}]{} & \setX & \xrightarrow[\smash{\textstyle \mkern1em \functionf \mkern1em}]{} \setY \mathrel{\rightcat{\xrightarrow[\smash{\textstyle \mkern1em \functiong \mkern1em}]{}}} & \rightcat \setZ \\
\end{array}}\]
The logical interrelations are:
\[\begin{array}{}
\leftcat{\langle d_0,d_1 \rangle} & \in & \rightadj(\functionf\rightcat\functiong\rightadj)\mathop{\rightadj\Kp} \\
& \Updownarrow \\
& {} \rlap{\mkern-6em \text{$\leftcat{\langle d_0,d_1 \rangle}$ lifts through $\rightadj(\functionf\rightcat\functiong\rightadj)\mathop{\rightadj\kp}$}} \\
& \Updownarrow \\
\leftcat{d_0}(\functionf\rightcat\functiong) & = & \leftcat{d_1}(\functionf\rightcat\functiong) & \mkern2em \xLeftrightarrow{\textstyle \text{definition of $\leftadj\coequ$}} \mkern2em & \functionf\rightcat\functiong \text{ extends over } \leftadj{\langle \leftcat{d_0},\leftcat{d_1} \rangle \coequ} \\
\Vert & \Updownarrow & \Vert \\
(\leftcat{d_0}\functionf)\rightcat\functiong & = & (\leftcat{d_1}\functionf)\rightcat\functiong \\
& \Updownarrow \\
& {} \rlap{\mkern-12em
\leftcat{\langle d_0,d_1 \rangle}\functionf = \langle \leftcat{d_0}\functionf,\leftcat{d_1}\functionf \rangle
\text{ lifts through $\rightcat\functiong\mathop{\rightadj\kp}$}} \\
& \Updownarrow \\
\llap{\leftcat{\langle d_0,d_1 \rangle}\functionf = {}} \langle \leftcat{d_0}\functionf,\leftcat{d_1}\functionf \rangle & \in & \rightcat\functiong\mathop{\rightadj\Kp} \\
\end{array}\]
