Theorem: Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Sufficient Condition

Let $\mathbf C$ be a locally small category.
Let $\mathbf C \times \mathbf C$ be the product category of $\mathbf C$ with itself.
Let $\Delta: \mathbf C \to \mathbf C \times \mathbf C$ denote the diagonal functor.
Let $\mathbf C$ have all binary products.
Then $\Delta$ has a right adjoint.

Proof:
Let $\times: \mathbf {C \times C} \to \mathbf C$ denote the product functor.
It will be shown that there exists an adjunction $\tuple {\Delta, \times, \alpha}$.
==== Construction of $\alpha$ ====
We construct $\alpha$ as follows.
Let $X \in \mathbf C$ and $\tuple{C_1, C_2} \in \mathbf{C \times C}$ be objects.
Let $\tuple {C_1 \times  C_2, p_1, p_2 }$ be the binary product of $C_1$ and $C_2$ with projections $p_1: C_1 \times  C_2 \to C_1$, $p_2: C_1 \times  C_2 \to C_2$.
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 C_1
&
 C_1 \times C_2
  \ar[l]_*+{p_1}
  \ar[r]^*+{p_2}
&
 C_2
}\end{xy}$</nowiki>
By definition of binary product, the triple $\tuple {C_1 \times  C_2, p_1, p_2 }$ is subject to the binary product UMP.
Let:
:$\alpha_{\tuple{X, \tuple{C_1, C_2}}} : \map {\operatorname{Hom}_{\mathbf {C \times C} } } {\tuple{X, X}, \tuple{C_1, C_2}} \to \map {\operatorname{Hom}_{\mathbf C} } {X, C_1 \times C_2}$
be the mapping defined by:
:$\forall$ morphisms $\tuple{f_1, f_2} : \tuple{X, X} \to \tuple{C_1, C_2} \in \mathbf {C \times C}$:
::$\map {\alpha_{\tuple{X, \tuple{C_1, C_2}}}} {f_1, f_2} = \family{f_1, f_2}$
:where $\family{f_1, f_2}$ denotes the unique morphism guaranteed by the UMP and represented in the commutative diagram:
::<nowiki>$\begin{xy}
<0em,0em>*+{X} = "TM",
<-8em,-6em>*+{C_1} = "BL",
<0em,-6em>*+{C_1 \times C_2} = "BM",
<8em,-6em>*+{C_2} = "BR",
"TM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f_1},
"TM";"BM" **@{--} ?>*@{>} ?<>(.7)*!/_2em/{\family{f_1, f_2} },
"TM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f_2},
"BM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{p_1},
"BM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{p_2},
\end{xy}$</nowiki>
==== $\alpha_{\tuple{X, \tuple{C_1, C_2}}}$ is Surjective ====
Let $f: X \to C_1 \times C_2 \in \map {\operatorname{Hom}_{\mathbf C} } {X, C_1 \times C_2}$.
Let $f_1 = p_1 \circ f$ and $f_2 = p_2 \circ f$.
::<nowiki>$\begin{xy}\xymatrix@+1em@L+3px{
 C_1
&
 X
  \ar[l]_*+{f_1}
  \ar[r]^*+{f_2}
&
 C_2
}\end{xy}$</nowiki>
The following diagram commutes:
::<nowiki>$\begin{xy}
<0em,0em>*+{X} = "TM",
<-8em,-6em>*+{C_1} = "BL",
<0em,-6em>*+{C_1 \times C_2} = "BM",
<8em,-6em>*+{C_2} = "BR",
"TM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f_1},
"TM";"BM" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f},
"TM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f_2},
"BM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{p_1},
"BM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{p_2},
\end{xy}$</nowiki>
By the uniqueness of $\family{f_1, f_2}$:
:$\family{f_1, f_2} = f$
We also have:
:$\tuple{f_1, f_2} \in \map {\operatorname{Hom}_{\mathbf {C \times C} } } {\tuple{X, X}, \tuple{C_1, C_2}}$
Hence:
:$\map {\alpha_{\tuple{X, \tuple{C_1, C_2}}}} {f_1, f_2} = f$
It follows that $\alpha_{\tuple{X, \tuple{C_1, C_2}}}$ is surjective by definition.
{{qed|lemma}}
==== $\alpha_{\tuple{X, \tuple{C_1, C_2}}}$ is Injective ====
Let $\tuple{f_1, f_2}, \tuple{g_1, g_2} \in \map {\operatorname{Hom}_{\mathbf {C \times C} } } {\tuple{X, X}, \tuple{C_1, C_2}}$ such that:
:$\map {\alpha_{\tuple{X, \tuple{C_1, C_2}}}} {f_1, f_2} = \map {\alpha_{\tuple{X, \tuple{C_1, C_2}}}} {g_1, g_2}$
That is:
:$\family{f_1, f_2} = \family{g_1, g_2}$
We have:
{{begin-eqn}}
{{eqn | l = f_1
      | r = p_1 \circ \family{f_1, f_2}
      | c = {{Defof|Binary Product UMP (Category Theory)}}
}}
{{eqn | r = p_1 \circ \family{g_1, g_2}
      | c = {{hypothesis}}
}}
{{eqn | r = g_1
      | c = {{Defof|Binary Product UMP (Category Theory)}}
}}
{{end-eqn}}
Similarly:
:$f_2 = g_2$
Hence:
:$\tuple{f_1, f_2} = \tuple{g_1, g_2}$
It follows that $\alpha_{\tuple{X, \tuple{C_1, C_2}}}$ is injective by definition.
{{qed|lemma}}
Hence $\alpha_{\tuple{X, \tuple{C_1, C_2}}}$ is a bijection by definition.
==== $\tuple{\Delta, \times, \alpha}$ is an Adjunction ====
It will be shown that $\tuple{\Delta, \times, \alpha}$ is an adjunction using Characterization of Adjunction Using Right Adjuncts of Triple Compositions.
===== Lemma 1 =====
{{:Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Lemma 1}}{{qed|lemma}}
===== Lemma 2 =====
{{:Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Lemma 2}}{{qed|lemma}}
Let:
:$f:X \to Y \in \mathbf C$
:$\tuple{h_1, h_2} : \tuple{Y, Y} \to \tuple{C_1, C_2} \in \mathbf {C \times C}$
:$\tuple{g_1, g_2} : \tuple{C_1, C_2} \to \tuple{K_1, K_2} \in \mathbf {C \times C}$
We have:
{{begin-eqn}}
{{eqn | l = \map {\alpha_{\tuple{X, \tuple{K_1, K_2} } } } {\tuple{g_1, g_2} \circ \tuple{h_1, h_2} \circ \Delta f}
      | r = \map {\alpha_{\tuple{X, \tuple{K_1, K_2} } } } {\tuple{g_1, g_2} \circ \tuple{h_1, h_2} \circ \tuple{f, f} }
      | c = {{Defof|Diagonal Functor}}
}}
{{eqn | r = \map {\alpha_{\tuple{X, \tuple{K_1, K_2} } } } {g_1 \circ h_1 \circ f, g_2 \circ h_2 \circ f }
      | c = {{Defof|Product Category|Composition in Product Category}}
}}
{{eqn | r = \family{g_1 \circ h_1 \circ f, g_2 \circ h_2 \circ f}
      | c = Definition of $\alpha_{\tuple{X, \tuple{K_1, K_2} } }$
}}
{{eqn | r = \paren{g_1 \times g_2} \circ \family{h_1 \circ f, h_2 \circ f}
      | c = Lemma 2
}}
{{eqn | r = \paren{g_1 \times g_2} \circ \family{h_1, h_2} \circ f
      | c = Lemma 1
}}
{{eqn | r = \map \times {g_1, g_2} \circ \family{h_1, h_2} \circ f
      | c = {{Defof|Product Functor}}
}}
{{eqn | r = \map \times {g_1, g_2} \circ \map {\alpha_{\tuple{Y, \tuple{C_1, C_2} } } } {h_1, h_2} \circ f
      | c = Definition of $\alpha_{\tuple{Y, \tuple{C_1, C_2} } }$
}}
{{end-eqn}}
This establishes the condition for Characterization of Adjunction Using Right Adjuncts of Triple Compositions. 
Hence $\tuple{\Delta, \times, \alpha}$ is an adjunction.
{{qed|lemma}}
It follows that $\times:\mathbf {C \times C} \to \mathbf C$ is a right adjoint of $\Delta$.