Note: for a category $C$, we write $[X, Y]_C$ for the hom-class of maps from $X$ to $Y$.

An adjunction is a pair of functors $F : C \rightarrow D$ and $G : D \rightarrow C$ with a certain relationship. There are many texts expositing adjunctions, but I have not seen one covering what I think of as their fundamental theorem. This is regrettable, since I think many people would appreciate the simplifying effect this result has on the theory of adjunctions in $\text{Cat}$. My goal today is to cover this theorem using coend calculus.

Adjunctions in a nutshell. First, an example. Let $\text{Set}$ be the category of sets and let $R \text{-mod}$ be the category of $R$-modules for a ring $R$. There are functors $F : \text{Set} \rightarrow R \text{-mod}$ sending a set $X$ to $\oplus_{x \in X} R$ and a functor $G : R \text{-mod} \rightarrow \text{Set}$ sending an $R$-module $M$ to its underlying set. There is a natural way of going back and forth between maps of $R$-modules $F(X) \rightarrow M$ and maps of sets $X \rightarrow M$. For a map of $R$-modules, $f: F(X) \rightarrow M$, we get a map of sets by first applying $G$ (this really does nothing) and then precomposing with a map $\eta_X$ of sets $X \rightarrow G(F(X))$ sending $x$ to the element $(a_y)_{y \in X}$ in the underlying set of $F(X)$ where $a_x = 1$ and $a_y =0$ for $y \neq x$. The resulting map is $X \stackrel{\eta_X}{\rightarrow} G(F(X)) \stackrel{G(f)}{\rightarrow} G(M)$. For a map of sets $f: X \rightarrow G(M)$, we get a map $F(X) \stackrel{f}{\rightarrow} F(G(M)) \stackrel{\epsilon_M}{\rightarrow} M$ where $\epsilon_M: F(G(M)) \rightarrow M$ sends $(a_x)_{x \in X}$ to $\sum_{x \in X} a_X$, where the sum is taken in $M$. What we have here is a natural correspondence between hom sets $[F(X), M]_{R \text{-mod}}$ and $[X, G(M)]_{\text{Set}}$. To go one way we apply $G$ and then precompose with $\eta_X$ (kind of like correcting for an error, since $F$ and $G$ are not inverses), and to go the other way we apply $F$ and then postcompose with $\epsilon_M$. This hints at the definition of an adjoint:

Definition: Let $F : C \rightarrow D$ and $G : D \rightarrow C$ be functors. We say that $F$ is adjoint to $G$, or that $F$ and $G$ are adjoint, if there is a natural isomorphism $\Phi : [ F-, -]_D \rightarrow [-, G-]_C$ between the functors $[ F-, -]_D, [-, G-]_C : C^{op} \times D \rightarrow \text{Set}$.

The example also hints at what I call the fundamental theorem of adjunctions in the $2$-category $\text{Cat}$:

Theorem: Let $C$ and $D$ be categories and $F$ and $G$ be functors. Then
(i) $[[F-, -], [-, G-]]_{[C^{op} \times D, \text{Set}]}$ and $[1_C, GF]_{[C^{op}, C^{op}]}$ are naturally isomorphic.
(ii) $[[-, G-], [F-, -]]_{[C^{op} \times D, \text{Set}]}$ and $[FG, 1_D]_{[D, D]}$ are naturally isomorphic.

Proof: These are dual; we prove the first. For the isomorphism itself, we have a series of natural isomorphisms:

This finishes the proof.

Using coend calculus like that is nice, but we are also interested in an explicit description of the isomorphisms $\alpha : \text{Nat}_{[C^{op} \times D, \text{Set}]} ([F-, -], [-, G-]) \rightarrow \text{Nat}_{[C^{op}, C^{op}]}(1_C, GF)$ and $\beta : \text{Nat}_{[C^{op}, C^{op}]}(1_C, GF) \rightarrow \text{Nat}_{[C^{op} \times D, \text{Set}]} ([F-, -], [-, G-])$! To achieve this description, notice that the following diagram commutes for each $X \in \text{Obj}(C)$ and each $Y \in \text{Obj}(D)$:

Take a natural transformation $\eta : 1 \rightarrow GF$. For each $X$, define a natural transformation $H_{X} : [FX, -] \rightarrow [X, G(-)]$ such that $(H_{X})_Y : [FX, Y] \rightarrow [X, GY]$ sends $f$ to $G(f) \circ \eta_X$, to $(H_{X})_Y$. Define a natural transformation $H : [[F(-), -]_D, [-, G(-)]_{C}]_{[C^{op} \times D, \text{Set}]}$ where $H_{X, Y} = (H_X)_Y$. The composition

gives the following diagram of mappings:

As this holds for each $X \in \text{Obj}(C)$ and each $Y \in \text{Obj}(D)$, we have $\alpha(\eta) = H$.

Next take a natural transformation $H : [[F(-), -]_D, [-, G(-)]_{C}]_{[C^{op} \times D, \text{Set}]}$. For each $X$, define a natural transformation $H_{X} : [FX, -] \rightarrow [X, G(-)]$ such that $(H_{X})_Y = H_{X, Y}$. Define a natural transformation $\eta : 1_C \rightarrow GF$ such that $\eta_X = (H_X)_{FX}(1_{FX})$. The composition

gives the following diagram of mappings:

As this holds for each $X \in \text{Obj}(C)$ and each $Y \in \text{Obj}(D)$, $\beta(H) = \eta$.

Hence $\alpha$ sends a natural transformation $\eta : 1_C \rightarrow GF$ to the natural transformation $H : [F-, -] \rightarrow [-, G-]$ where $H_{X, Y}(f)= Gf \circ \eta_X$ for $X \in \text{Obj}(C)$, $Y \in \text{Obj}(D)$, and $f : FX \rightarrow Y$, and $\beta$ sends a natural transformation $H : [F(-), -]_D \rightarrow [-, G(-)]_{C}$ to the natural transformation $\eta : 1_C \rightarrow GF$ such that $\eta_X = H_{X, FX} (1_{FX})$.

This theorem puts us in a place where we can prove other results about adjoints much more easily:

Theorem: The following are equivalent:

(i) The functors $[F-, -]_D : C^{op} \times D \rightarrow \text{Set}$ and $[-, G-]_C : C^{op} \times D \rightarrow \text{Set}$ are naturally isomorphic.
(ii)(a) (Universal Morphisms Definition) There is a natural transformation $\eta : 1_{C} \rightarrow G F$ such that, for each $X \in \text{Obj}(C)$, each $Y \in \text{Obj}(D)$, and each morphism $f : X \rightarrow GY$ in $C$, there is a unique morphism $g : FX \rightarrow Y$ in $\text{Mor}(D)$ such that $Gg \circ \eta_X =f$.
(ii)(b) (Universal Morphisms Definition) There is a natural transformation $\epsilon : FG \rightarrow 1_{D}$ such that, for each $Y \in \text{Obj}(D)$, each $X \in \text{Obj}(C)$, and each $g : FX \rightarrow Y$ in $D$, there is a unique morphism $f : X \rightarrow GY$ in $C$ such that $\epsilon_Y \circ Ff = g$.
(iii) (The Unit Counit Definition) There are natural transformations $\epsilon : FG \rightarrow 1_{D}$ and $\eta : 1_{C} \rightarrow G F$ such that the following compositions are the identity morphism, for each $X \in \text{Obj}(C)$ and $Y \in \text{Obj}(D)$.

Proof: $(i) \implies (ii)(a)$. Suppose that the functors $[F-, -]_D : C^{op} \times D \rightarrow \text{Set}$ and $[-, G-]_C : C^{op} \times D \rightarrow \text{Set}$ are naturally isomorphic, and take a natural isomorphism $H : [F-, -]_D \rightarrow [-, G-]_C$. Let $\eta : 1_C \rightarrow GF$ be the corresponding natural transformation. Take $X \in \text{Obj}(C)$, $Y \in \text{Obj}(D)$, and $f : X \rightarrow GY$. There is a unique $g : FX \rightarrow Y$ such that $Hg = f$, since $H$ is a natural isomorphism. But $Hg = Gg \circ \eta_X$ by the fundamental theorem. This shows (ii)(a).

$(ii)(a) \implies (i)$. Suppose that there is a natural transformation $\eta : 1_{C} \rightarrow G F$ such that, for each $X \in \text{Obj}(C)$, each $Y \in \text{Obj}(D)$, and each morphism $f : X \rightarrow GY$ in $C$, there is a unique morphism $g : FX \rightarrow Y$ in $\text{Mor}(D)$ such that $Gg \circ \eta_X =f$. Let $H : [F-, -]_D \rightarrow [-, G-]_C$ be the natural transformation corresponding to $\eta$. Take $X \in \text{Obj}(C)$ and $Y \in \text{Obj}(D)$. $H_{X, Y}g = Gg \circ \eta_X$ for each $g : X \rightarrow GY$, so that, for each $f \in [X, GY]_C$, there is a unique $g \in [FX, Y]_D$ such that $H_{X, Y}g = Gg \circ \eta_X = f$. This shows (i).

$(i) \implies (ii)(b)$. Suppose that the functors $[F-, -]_D : C^{op} \times D \rightarrow \text{Set}$ and $[-, G-]_C : C^{op} \times D \rightarrow \text{Set}$ are naturally isomorphic, and take a natural isomorphism $H : [-, G-]_C \rightarrow [F-, -]_D$. Let $\epsilon : FG \rightarrow 1_D$ be the corresponding natural transformation. Take $X \in \text{Obj}(C)$, $Y \in \text{Obj}(D)$, and $g : FX \rightarrow Y$. There is a unique $f : X \rightarrow GY$ such that $Hf = g$, since $H$ is a natural isomorphism. But $Hf = \epsilon_Y \circ Ff$ by the fundamental theorem. This shows (ii)(b).

$(ii)(b) \implies (i)$. Suppose that there is a natural transformation $\epsilon : FG \rightarrow 1_{D}$ such that, for each $X \in \text{Obj}(C)$, each $Y \in \text{Obj}(D)$, and each morphism $g : FX \rightarrow Y$ in $D$, there is a unique morphism $f : X \rightarrow GY$ in $\text{Mor}(D)$ such that $\epsilon_Y \circ Ff \circ = g$. Let $H : [-, G-]_C \rightarrow [F-, -]_D$ be the natural transformation corresponding to $\eta$. Take $X \in \text{Obj}(C)$ and $Y \in \text{Obj}(D)$. $H_{X, Y}f = \epsilon_Y \circ Ff$ for each $f : X \rightarrow GY$, so that, for each $g \in [FX, Y]_C$, there is a unique $f \in [X, GY]_D$ such that $H_{X, Y}f = \epsilon_Y \circ Ff = g$. This shows (i).

$(i) \implies (iii)$. Suppose that the functors $[F-, -]_D : C^{op} \times D \rightarrow \text{Set}$ and $[-, G-]_C : C^{op} \times D \rightarrow \text{Set}$ are naturally isomorphic, and take a natural isomorphism $H : [F-, -]_D \rightarrow [-, G-]_C$. Let $\eta : 1_C \rightarrow GF$ be the natural transformation corresponding to $H$ and let $\epsilon : GF \rightarrow 1_D$ be the natural transformation corresponding to $H^{-1}$. For $X \in \text{Obj}(C)$, we have

and

$(iii) \implies (i)$. Suppose $(iii)$ holds. Let $E : [F-, -] \rightarrow [-, G-]$ be the natural transformation induced by $\epsilon : FG \rightarrow 1_D$, and let $H : [-, G-] \rightarrow [F-, -]$ be the natural transformation induced by $\eta : 1_C \rightarrow GF$.

Take $Y \in \text{Obj}(D)$. Write $(EH)_{-, Y} : [-, GY] \rightarrow [-, GY]$ for the induced natural transformation. The following diagram commutes by the Yoneda lemma:

So $(EH)_{X, Y} (f) = [f, GY] \circ (EH)_{GY, Y} (1_{GY})= (EH)_{GY, Y}(1_{GY}) \circ f = f$. So $(EH)_{-, Y}$ is the identity natural transformation. Hence $EH$ is the identity natural transformation.

Take $Y \in \text{Obj}(D)$. Write $(HE)_{X, -} : [FX, -] \rightarrow [FX, -]$ for the induced natural transformation. The following diagram commutes by the Yoneda lemma:

So $(HE)_{X, Y} (f) = [FX, f] \circ (HE)_{X, FX} (1_{FX}) = f \circ (HE)_{X, FX}(1_{FX}) = f$. So $(HE)_{X,-}$ is the identity natural tarnsformation. Hence $HE$ is the identity natural transformation.

It follows that $H$ and $E$ are inverse natural transformations, and therefore natural isomorphisms. This shows (i).