Theorem: Characterization of Adjunction Using Right Adjuncts of Triple Compositions

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let $F : \mathbf D \to \mathbf C$,  $G : \mathbf C \to \mathbf D$ be covariant functors.
Let $\mathbf D \times \mathbf C$ denote the product category of $\mathbf D$ with $\mathbf C$.
For each object $\tuple{D, C} \in \mathbf D \times \mathbf C$ let $\alpha$ associate $\tuple{D, C}$ with a bijection:
:$\alpha_{\tuple{D, C} } : \map {\operatorname{Hom}_{\mathbf C} } {FD, C} \to \map {\operatorname{Hom}_{\mathbf D} } {D, GC}$
Then:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:for every:
::$f:D_2 \to D_1 \in \mathbf D$
::$h:FD_1 \to C_1 \in \mathbf C$
::$g:C_1 \to C_2 \in \mathbf C$
:we have:
::$\map {\alpha_{\tuple{D_2, C_2} } } {g \circ h \circ Ff} = Gg \circ \map {\alpha_{\tuple{D_1, C_1} } } h \circ f$
That is, given commutative diagram in $\mathbf C$:
::<nowiki>$\begin{xy}
<5.5em,5em>*+{FD_1} = "TL",
<14.5em,5em>*+{FD_2} = "TR",
<5.5em,0em>*+{C_1} = "BL",
<14.5em,0em>*+{C_2} = "BR",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{h},
"TR";"BR" **@{.} ?>*@{>} ?<>(.5)*!/_2.5em/{g \circ h \circ F f},
\end{xy}$</nowiki>
the following diagram commutes in $\mathbf D$:
::<nowiki>$\begin{xy}
<0em,5em>*+{D_1} = "TL",
<9em,5em>*+{D_2} = "TR",
<0em,0em>*+{G C_1} = "BL",
<9em,0em>*+{G C_2} = "BR",
"TR";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{Gg},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^3.0em/{\map {\alpha_{\tuple{D_1, C_1} } } h},
"TR";"BR" **@{.} ?>*@{>} ?<>(.5)*!/_5.0em/{\map {\alpha_{\tuple{D_2, C_2} } } {g \circ h \circ F f} },
\end{xy}$</nowiki>

Proof:
By definition of adjunction:
:the triple $\tuple {F, G, \alpha}$ is an adjunction
{{iff}}:
:$(1)$ for all $f: D_2 \to D_1 \in \mathbf D$ and $g: C_1 \to C_2 \in \mathbf C$:
::$\alpha_{\tuple{D_2,C_2}} \circ \map {\operatorname{Hom}_{\mathbf C}} {Ff, g} = \map {\operatorname{Hom}_{\mathbf D}} {f, Gg} \circ \alpha_{\tuple{D_1,C_1}}$
:that is, the following diagram commutes:
::<nowiki>$\begin{xy}
<0em,6em>*+{\map {\operatorname{Hom}_{\mathbf C} } {FD_1, C_1} } = "C",
<15em,6em>*+{\map {\operatorname{Hom}_{\mathbf C} } {FD_2, C_2} } = "C2",
<0em,0em>*+{\map {\operatorname{Hom}_{\mathbf D} } {D_1, GC_1} } = "D",
<15em,0em>*+{\map {\operatorname{Hom}_{\mathbf D} } {D_2, GC_2} } = "D2",
"C";"C2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\map {\operatorname{Hom}_{\mathbf C} } {Ff, g} },
"D";"D2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\map {\operatorname{Hom}_{\mathbf D} } {f, Gg} },
"C";"D" **@{-} ?>*@{>} ?<>(.5)*!/^1.8em/{\alpha_{\tuple{D_1, C_1} } },
"C2";"D2" **@{-} ?>*@{>} ?<>(.5)*!/_1.8em/{\alpha_{\tuple{D_2, C_2} } },
\end{xy}$</nowiki>
:where:
::$\map {\operatorname{Hom}_{\mathbf C}} {Ff, g} : \map {\operatorname{Hom}_{\mathbf C} } {FD_1, C_1} \to \map {\operatorname{Hom}_{\mathbf C} } {FD_2, C_2}$ is the mapping defined by : $h \mapsto g \circ h \circ Ff$
::$\map {\operatorname{Hom}_{\mathbf D}} {f, Gg} : \map {\operatorname{Hom}_{\mathbf D} } {D_1, GC_1} \to \map {\operatorname{Hom}_{\mathbf D} } {D_2, GC_2}$ is the mapping defined by : $h \mapsto Gg \circ h \circ f$
From Equality of Mappings:
:$(1)$ holds
{{iff}}:
:$(2)$ for all $f: D_2 \to D_1 \in \mathbf D, g: C_1 \to C_2 \in \mathbf C$ and $h: FD_1 \to C_1 \in \mathbf C$:
::$\map {\paren{\alpha_{\tuple{D_2,C_2}} \circ \map {\operatorname{Hom}_{\mathbf C}} {Ff, g} } } h = \map {\paren{\map {\operatorname{Hom}_{\mathbf D}} {f, Gg} \circ \alpha_{\tuple{D_1,C_1} } } } h$
By definition of composite mapping:
:$(2)$ holds
{{iff}}:
:$(3)$ for all $f: D_2 \to D_1 \in \mathbf D, g: C_1 \to C_2 \in \mathbf C$ and $h: FD_1 \to C_1 \in \mathbf C$:
::$\map {\alpha_{\tuple{D_2,C_2} } } {\map {\map {\operatorname{Hom}_{\mathbf C} } {Ff, g} } h} = \map {\map {\operatorname{Hom}_{\mathbf D} } {f, Gg} } {\map {\alpha_{\tuple{D_1,C_1} } } h}$
By definition of $\map {\operatorname{Hom}_{\mathbf C} } {Ff, g}$ and $\map {\operatorname{Hom}_{\mathbf D} } {f, Gg}$:
:$(3)$ holds
{{iff}}:
:$(4)$ for all $f: D_2 \to D_1 \in \mathbf D, g: C_1 \to C_2 \in \mathbf C$ and $h: FD_1 \to C_1 \in \mathbf C$:
::$\map {\alpha_{\tuple{D_2, C_2} } } {g \circ h \circ Ff} = Gg \circ \map {\alpha_{\tuple{D_1, C_1} } } h \circ f$
{{qed}}