Loading [MathJax]/jax/element/mml/optable/MathOperators.js

Monday, April 14, 2014

The quotient-kernel adjunction


Theorem.
Let X be (a set with two structures on it):
  • (a graph Ed0d1X) having X as its set of vertices, and
  • (a function XfY) from X to another set Y.
Then, referring to (the entities in the diagram below),
there exists a u
lifting d0,d1
through k0,k1
u=d0,d1/k0,k1
d0f=d1f
the fork condition
d0,d1f
d0,d1
\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}

No comments:

Post a Comment

MathJax 2.7.9