Grothendieck is fully faithful

$\Newextarrow{\xRightarrow}{10,10}{0x21D2}$

2018-04-25

Given (a category $\cata$) and (functors $\functX,\functY : \cata \to \Set$),
we may form the comma categories $1\downarrow \functX$ and $1\downarrow \functY$,
where $1$ is (the functor $1: \cati \to \Set$) whose values are (the unit set $1\in\Set$) and (its identity function).
The construction $1\downarrow \functX$ is actually a special case of the more general “Grothendieck construction”, which treats functors into $\Cat$ (Wikipedia, nlab, $\text{C&D}$ section 6).
This construction is actually a functor (with many names): $$\mkern{-250mu} \begin{array}{} \bar\theta_\cata = {\cal G} = {\cal G}_\cata^\cati = Gr = {\displaystyle\int} = 1\downarrow {?} & : & [\cata, \Set] & \longrightarrow & \rlap{(\text{discrete opfibrations over $\cata$}) \subseteq (\CAT\downarrow\cata)} \\ && \functX & \longmapsto && 1\downarrow\functX \\ &&&&&& \searrow \rlap{d_\functX} \\ && \llap\tau \Big\Downarrow & \longmapsto && \mkern{10mu} \Big\downarrow \mkern{-30mu} 1\downarrow\tau && \cata \\ &&&&&& \nearrow \rlap{d_\functY} \\ && \functY & \longmapsto && 1\downarrow\functY \\ \end{array} \taglabel{C&D(6.9)}$$ In the following we show that this functor is fully faithful.
In fact, not just two but three homsets are shown to be in bijection,
demonstrating, not only (the full faithfulness of $Gr$), but also that ($\functX$ is a left extension over $d_\functX$ of $!1$).

Theorem. ($\text{C&D(6.30)}$, with $[\mkern{-2mu}[?, \CAT]\mkern{-2mu}]$ replaced by $[?, \Set]$.)
We have bijections between three homsets as shown in the first row of the table below.
The second row shows (elements of each homset) which correspond (under the bijections),
while the third row shows components of (the transformations) and (the functor).
The bijection labeled (comma) is a special case (for $1\downarrow\functX$) of (the universal property of $1\downarrow \functY$).
The bijection labeled (lan) demonstrates that $\functX$ is (a left extension over $d_\functX$ of $!1$).
The composite bijection demonstrates (the full faithfulness of $\bar\theta_\cata = {\cal G} = {\cal G}_\cata^\cati = Gr = \int = 1\downarrow {?}$).

homset	$\hom \functX {[\cata, \Set]} \functY$	$\buildrel \textstyle \text{(lan)} \over \cong$	$\hom {!1} {[(1\downarrow\functX) , \Set]} {d_\functX\functY}$	$\buildrel \textstyle \text{(comma)} \over\cong$	$\hom {1\downarrow \functX} {\big( \CAT\downarrow\cata \big)} {1\downarrow \functY}$
arrow	$\functX \xRightarrow[\textstyle \tau]{} \functY$	$\leftrightarrow$	$!1 \xRightarrow[\textstyle \eltx \ncomp1 (d_\functX \ncomp0 \tau) = \sigma = \functM \ncomp0 \elty]{} d_\functX \functY$	$\leftrightarrow$	$1\downarrow\functX \xrightarrow[\textstyle 1\downarrow\tau = \langle d_\functX, \sigma \rangle = \functM]{} 1\downarrow\functY$
component	$\functX_\obja \xrightarrow[\textstyle \tau_\obja = ( \lambda \eltx \in \functX_\obja ) \sigma_{\langle\obja,\eltx\rangle}]{} \functY_\obja$		$1 \xrightarrow[\textstyle \eltx \tau_\obja = \sigma_{\langle \obja, \eltx \rangle} = \elty_{\functM_{\langle \obja, \eltx \rangle}}]{} \functY_\obja$		$\mkern{30mu}\langle \obja, \eltx \rangle \mapsto \langle \obja, \eltx \tau_\obja \rangle = \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \functM_{\langle \obja, \eltx \rangle}$

The symbol “$x$” has several meanings in the table:
in set theory as a bound variable in $\functX_\obja$, in the category $\Set$ as an arrow $1\to\functX_\obja$, and in the 2-category $\CAT$ as the universal 2-cell for $1\downarrow\functX$.

The relations between $\tau$, $\sigma$, and $\functM$ are mediated by the two equalities in the 2-category $\CAT$ shown below.
The equalities in effect show two ways of factoring $\sigma$.
(Due to software limitations, some do-it-yourself additions are needed:
In the triangular prism, the three vertical arrows and three vertical 2-cells should be extended to their appropriate sources and targets.)

$\bbox[20px,border:4px groove black]{ \begin{array}{} \source{ 1\downarrow\functX } && \source{ \xrightarrow[]{\textstyle \mkern40mu \llap{! \mkern20mu} {} \mkern40mu} } && \cati \\ & \llap{\lower3pt\hbox{$\boxed\functM\mkern{-6mu}$}} \searrow & \raise6pt\hbox{$\Vert$} & \target{ \nearrow \rlap{\lower3pt\hbox{${!}$}} } \\ && \target{ 1\downarrow\functY } \\ \source{ \llap{d_\functX} \Big\downarrow } && \source{ \mkern{-50mu}\llap{\eltx} \Big\Downarrow } && \Big\downarrow \rlap{1} \\ & \Big\Vert && \target{ \Big\Downarrow \rlap{\elty} } \\ && \target{ \Big\downarrow \rlap{d_\functY} } \\ \source{ \cata } && \source{ \xrightarrow[]{\textstyle \mkern40mu \llap{\functX\mkern20mu} {} \mkern40mu} } && \Set \\ & \llap{\lower3pt\hbox{$1_\cata \mkern{-10mu}$}} \searrow & \Downarrow \rlap{\boxed\tau} & \target{ \nearrow \rlap{\lower3pt\hbox{$\functY$}} } \\ && \target{ \cata } \\ \end{array} }$

$\begin{array}{} \xlongequal[]{\textstyle \boxed\functM \mkern2mu \ncomp0 \target\elty}\\ \xlongequal[\textstyle \source\eltx \ncomp1 (\source{d_\functX} \ncomp0 \, \boxed\tau)]{}\\ \end{array}$

$\bbox[20px,border:4px groove black]{ \begin{array}{} \source{1\downarrow\functX} & \source{\buildrel \textstyle ! \over \longrightarrow} & \cati \\ \source{\llap{d_\functX} \Big\downarrow} & \Big\Downarrow \rlap{\boxed\sigma} & \Big\downarrow\rlap 1 \\ \cata & \target{\xrightarrow[\textstyle \functY]{}} & \Set\\ \end{array} }$

Proof:
Suppose $\alpha \in \hom \obja \cata \objap$, $\eltx \in \functX_\obja$, and $\eltxp = \eltx \functX_\alpha \in \functX_\objap$.
Consider the following display, exhibiting potential diagrams in three different categories.
The upper left arrow is (an arrow in $1\downarrow\functX$).
The lower right arrow is (a possible arrow in $1\downarrow\functY$).
The diamond in the center is (a diagram in $\Set$).
The commutativity of its upper left triangle corresponds to ($\alpha$ being an arrow in $1\downarrow\functX$).
Its upper right and lower left triangles commute by the definition of $\sigma$.
The commutativity of its lower right triangle is in question;
its commuting is shown below to be equivalent to:

• $\alpha$ being an arrow in $1\downarrow\functY$;
• the naturality of $\sigma$ at $\alpha$, $\eltx$;
• the naturality of $\tau$ at $\alpha$, $\eltx$.

$$\begin{array}{} &&&& \langle \obja, \eltx \rangle \\ && \\ &&&& \functX_\obja \\ & \llap\alpha \swarrow && \llap{\raise3pt\hbox{$\functX_\alpha \mkern{-8mu}$}} \swarrow & \Bigg\uparrow \mkern{-11mu}\eltx & \llap{\lower5pt\hbox{$\scriptstyle \text{defn}$}\!} \searrow \rlap{\raise4pt\hbox{$\mkern{-4mu} \boxed{\tau_\obja} = ( \lambda \eltx \in \functX_\obja ) \sigma_{\langle\obja,\eltx\rangle}$}} \\ \langle \objap, \eltxp \rangle && \functX_\objap & \xleftarrow[]{\hbox{$\mkern{10mu} \eltxp \mkern{10mu}$}} & 1 & \xrightarrow[]{\textstyle \boxed{\sigma_{\langle \obja, \eltx \rangle}}} & \functY_\obja && \langle \obja, \eltx \tau_\obja \rangle = \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \boxed{\functM_{\langle \obja, \eltx \rangle}} \\ &&& \llap{\tau_\objap} \searrow \rlap{\!\!\!\raise8pt\hbox{$\scriptstyle \text{defn}$}} & \Bigg\downarrow \rlap{\mkern{-17mu} \sigma_{\langle \objap, \eltxp \rangle}} & \llap {\raise5pt\hbox{$\red{?}$}} \swarrow \rlap{\functY_\alpha} && \swarrow \rlap{\alpha {\red ?}} \\ &&&& \functY_\objap \\ && \\ &&&& \llap{ \langle \objap, \eltxp \tau_\objap \rangle = \big\langle \objap, \sigma_{\langle \objap, \eltxp \rangle} \big\rangle } = \rlap{ \functM_{\langle \objap, \eltxp \rangle}} \\ \end{array} \taglabel{C&D(6.5)}$$

---

We have

$$\begin{array}{} \alpha & \in & \hom {\langle \obja, \eltx \rangle} {(1\downarrow\functX)} {\langle \objap, \eltxp \rangle} \\ & \Updownarrow \\ \eltxp & = & \eltx \functX_\alpha \\ & \Downarrow \rlap{- \tau_\objap} \\ \eltxp \tau_\objap & = & \eltx \functX_\alpha \tau_\objap \\ \Vert & {} \rlap{ \mkern{5mu} \Downarrow \mkern{-15mu} \lower5pt\hbox{$\swarrow \mkern{-15mu} \nearrow$} } & \Vert & {} \Leftrightarrow \tau \text{ natural at } \alpha, \eltx \\ \eltxp \tau_\objap & = & \eltx \tau_\obja \functY_\alpha \\ \llap{\text{defn $\sigma$}} \Vert & \Updownarrow & \Vert \rlap{\text{defn $\sigma$}} \\ \sigma_{\langle \objap, \eltxp \rangle} & \red{ = \rlap {?} } & \sigma_{\langle \obja, \eltx \rangle}\functY_\alpha & {} \Leftrightarrow \sigma \text{ natural at } \alpha, \eltx \\ & \Updownarrow \\ \alpha & \in & {} \rlap{ \hom {( \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \functM_{\langle \obja, \eltx \rangle} )} {(1\downarrow\functY)} {( \langle \objap, \sigma_{\langle \objap, \eltxp \rangle} \rangle = \functM_{\langle \objap, \eltxp \rangle} )} } \\ \end{array}$$

which proves

$$\Big[ \alpha \in \hom {\langle \obja, \eltx \rangle} {(1\downarrow\functX)} {\langle \objap, \eltxp \rangle} \Big] \Rightarrow \Big[ \big[ \alpha \in \hom {( \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \functM_{\langle \obja, \eltx \rangle} )} {(1\downarrow\functY)} {( \langle \objap, \sigma_{\langle \objap, \eltxp \rangle} \rangle = \functM_{\langle \objap, \eltxp \rangle} )} \big] \Leftrightarrow \big[ \tau \text{ natural at } \alpha, \eltx \big] \Big]$$

thus, given $\alpha\in\hom\obja\cata\objap$, $\eltx\in\functX_\obja$, and defining $\eltxp=\eltx\functX_\alpha$ so that $\alpha \in \hom {\langle \obja, \eltx \rangle} {(1\downarrow\functX)} {\langle \objap, \eltxp \rangle}$,
the following are logically equivalent:

• $\tau$ is natural at $\alpha$, $\eltx$;
• $\sigma$ is natural at $\alpha$, $\eltx$;
• $\alpha \in \hom {( \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \functM_{\langle \obja, \eltx \rangle} )} {(1\downarrow\functY)} {( \langle \objap, \sigma_{\langle \objap, \eltxp \rangle} \rangle = \functM_{\langle \objap, \eltxp \rangle}) }$.

The theorem then follows easily (mainly by interchanging universal quantification over ($\alpha\in\hom\obja\cata\objap$) and ($\eltx\in\functX_\obja$)).

---

References “$\text{C&D(6.n)}$” are to section 6 of the paper
Kelly, G. M. (1974). "On clubs and doctrines". Category Seminar (Proceedings Sydney Category Theory Seminar 1972/1973). SLNM. 420. pp. 181–256. doi:10.1007/BFb0063104,
which extends this document by replacing $\Set$ with $\Cat$ and introducing laxity all over the place.
(The defining equation $\langle \obja, \eltx \tau_\obja \rangle = \functM_{\langle \obja, \eltx \rangle}$ is $\text{C&D(6.11)}$; $\sigma$ is implicit but not explicit in $\text{C&D}$.)

---

Work in progress:
The theorem as stated occupies an intermediate position between many generalizations and many specializations.
Here are a few of the special cases of the theorem which are of importance.

Example 1. ($\cata = \cati$)
Take $\cata$ to be the unit category $\cati$.
In this case $\tau$ amounts to a single function, say $f : \functX \to \functY$ in $\Set$,
while $\sigma$ amounts to its specification on elements, $\eltx \mapsto \sigma_\eltx = (\eltx)f$.

Example 2. ($\cata$ discrete, $\functX, \functY$ constant)
Take $\cata$ to be a discrete category, so we may identify it with its set of objects, $\cata_0 = {}$, say, $A$.
Further, let both $\functX, \functY : A \to \Set$ be constant functors (functions in this case) at, respectively, sets $X, Y \in \Set$.
In the following table we put the special case, for this case, below the general case.

homset	$\hom \functX {[\cata, \Set]} \functY$	$\buildrel \textstyle \text{(lan)} \over \cong$	$\hom {!1} {[1\downarrow\functX , \Set]} {d_\functX\functY}$	$\buildrel \textstyle \text{(comma)} \over\cong$	$\hom {1\downarrow \functX} {\big( \CAT\downarrow\cata \big)} {1\downarrow \functY}$
homset	$\big[ \objA, [\objX,\objY] \big]$	$\cong$	$[\objA\times \objX, \objY] \cong \big[\objA\times \objX , [1,\objY] \big]$	$\buildrel \textstyle \text{(comma)} \over\cong$	$\hom {\langle \objA\times \objX, \pi_0 \rangle} {\big( \Set\downarrow \objA \big)} {\langle \objA\times \objY, \pi_0 \rangle}$
arrow	$\functX \xRightarrow[\textstyle \tau]{} \functY$	$\leftrightarrow$	$!1 \xRightarrow[\textstyle \eltx \ncomp1 (d_\functX \ncomp0 \tau) = \sigma = \functM \ncomp0 \elty]{} d_\functX \functY$	$\leftrightarrow$	$1\downarrow\functX \xrightarrow[\textstyle 1\downarrow\tau = \langle d_\functX, \sigma \rangle = \functM]{} 1\downarrow\functY$
arrow	$\objA \xrightarrow[\textstyle \tau]{} [\objX, \objY]$	$\leftrightarrow$	$\objA\times\objX \xrightarrow[\textstyle \sigma]{} \objY \mkern{10mu} \leftrightarrow \mkern{10mu} \objA\times\objX \xrightarrow[\textstyle \sigma]{} [1,\objY]$	$\leftrightarrow$	$\objA\times\objX \xrightarrow[\textstyle \langle \pi_0, \sigma \rangle = \functM]{} \objA\times\objY$
component	$\functX_\obja \xrightarrow[\textstyle \tau_\obja = ( \lambda \eltx \in \functX_\obja ) \sigma_{\langle\obja,\eltx\rangle}]{} \functY_\obja$		$1 \xrightarrow[\textstyle \eltx \tau_\obja = \sigma_{\langle \obja, \eltx \rangle}]{} \functY_\obja$		$\mkern{30mu}\langle \obja, \eltx \rangle \mapsto \langle \obja, \eltx \tau_\obja \rangle = \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \functM_{\langle \obja, \eltx \rangle}$
component	$\obja \mapsto (\objX \xrightarrow[\textstyle \tau_\obja]{} \objY)$		$\langle \obja, \eltx \rangle \mapsto (1 \xrightarrow[\textstyle \sigma_{\langle \obja, \eltx \rangle}]{} \objY)$		$\mkern{30mu}\langle \obja, \eltx \rangle \mapsto \langle \obja, \eltx \tau_\obja \rangle = \langle \obja, \sigma_{\langle \obja, \eltx \rangle} \rangle = \functM_{\langle \obja, \eltx \rangle}$