Theorem: Diagonal Functor on Product Category has Right Adjoint Iff Category has Binary Products/Necessary 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 $\Delta$ have a right adjoint.
Then $\mathbf C$ has all binary products such that the right adjoint is the product functor.

Proof:
Let $\otimes:\mathbf {C \times C} \to \mathbf C$ be a right adjoint of $\Delta_{\mathbf J}$.
==== $\mathbf C$ has all Binary Products ====
By definition of right adjoint there exists an adjunction $\tuple{\Delta, \otimes, \alpha}$.
Let $\pi : \Delta \otimes \to \operatorname{id}_{\mathbf {C \times C} }$ denote the counit of adjunction $\tuple{\Delta, \otimes, \alpha}$.
From Morphism of Counit of Adjunction is Universal:
:for each object $\tuple{C_1, C_2} \in \mathbf {C \times C}$:
::the morphism $\pi_{\tuple{C_1, C_2} }: \map {\paren{\Delta \otimes} } {C_1, C_2} \to \tuple{C_1, C_2}$ is a universal morphism from $\Delta$ to $\map \otimes {C_1, C_2}$
By definition of diagonal functor:
:$(1):\quad$for each object $\tuple{C_1, C_2} \in \mathbf {C \times C}$:
::$\map {\paren{\Delta \otimes} } {C_1, C_2} = \tuple{\map \otimes {C_1, C_2}, \map \otimes {C_1, C_2}}$
and:
:$(2):\quad$for each morphism $\tuple{f_1, f_2} \in \mathbf {C \times C}$:
::$\map {\paren{\Delta \otimes} } {f_1, f_2} = \tuple{\map \otimes {f_1, f_2}, \map \otimes {f_1, f_2}}$
By definition of a morphism of product cateogry:
:$(3):\quad$there exists morphisms $p_1: \otimes \tuple{C_1, C_2} \to C_1$ and $p_2: \otimes \tuple{C_1, C_2} \to C_2$ such that:
::$\pi_{\tuple{C_1, C_2}} = \tuple{p_1, p_2}$
By definition of universal morphism:
:$(4):\quad$for each object $\tuple{C_1, C_2} \in \mathbf {C \times C}$ and for each morphism $f: \Delta X \to \tuple{C_1, C_2} \in \mathbf{C_1 \times C_2}$:
::$\exists f': X \to \otimes \tuple{C_1, C_2} : \pi_{\tuple{C_1, C_2} } \circ \Delta f' = f$
It will be shown that for objects $C_1, C_2 \in \mathbf C$:
:$\tuple{\otimes \tuple{C_1, C_2}, p_1, p_2}$ is a binary product.
Let $f_1: X \to C_1, f_2: X \to C_2$ be morphisms of $\mathbf C$.
Consider the morphism $\tuple{f_1, f_2} : \tuple{X, X} \to \tuple{C_1, C_2}$ of the product category $\mathbf{C \times C}$.
By definition of diagonal functor:
:$\tuple{f_1, f_2} : \Delta X \to \tuple{C_1, C_2} \in \mathbf{C \times C}$
By $(4)$:
:$\exists f': X \to \otimes \tuple{C_1, C_2} : \pi_{\tuple{C_1, C_2} } \circ \Delta f' = \tuple{f_1, f_2}$
By $(3)$:
:$\exists f': X \to \otimes \tuple{C_1, C_2} : \tuple{p_1, p_2} \circ \tuple{f', f'} = \tuple{f_1, f_2}$
By definition of composition in product category:
:$\exists f': X \to \otimes \tuple{C_1, C_2} : \tuple{p_1 \circ f', p_2 \circ f'} = \tuple{f_1, f_2}$
That is:
:$\exists f': X \to \otimes \tuple{C_1, C_2} : p_1 \circ f' = f_1, p_2 \circ f' = f_2$
Hence $\tuple {\map \otimes {C_1,  C_2}, p_1, p_2 }$ is a binary product by definition. 
It follows that for all objects $\tuple{C_1, C_2} \in \mathbf {C \times C}$:
:$(5):\quad$there exists morphisms $p_1: \map \otimes {C_1, C_2} \to C_1$ and $p_2: \map \otimes {C_1, C_2} \to C_2$ such that:
::$\tuple {\map \otimes {C_1,  C_2}, p_1, p_2 }$ is a binary product
:and:
::$\pi_{\tuple{C_1, C_2}} = \tuple{p_1, p_2}$
It follows that $\mathbf C$ has all binary products.
{{qed|lemma}}
==== Right Adjoint $\otimes$ is Product functor ====
Let $\times$ denote the product functor.
{{Recall|Product Functor}}
{{:Definition:Product Functor}}
For all objects $\tuple{C_1, C_2} \in \mathbf {C \times C}$ we have:
{{begin-eqn}}
{{eqn | n = 6
      | l = \times \tuple {C_1, C_2}
      | r = C_1 \times C_2
      | c = {{Defof|Product Functor}}
}}
{{eqn | r = \otimes \tuple{C_1, C_2}
      | c = By $(5)$
}}
{{end-eqn}}
By definition of product of morphisms 
:$\times \tuple {f_1, f_2}$ denotes the unique morphism guaranteed by the binary product UMP that makes the following diagram commute:
::<nowiki>$\begin{xy}
<-8em,0em>*+{C_1} = "TL",
<0em,0em>*+{C_1 \times C_2} = "TM",
<8em,0em>*+{C_2} = "TR",
<-8em,-6em>*+{ {C_1}'} = "BL",
<0em,-6em>*+{ {C_1}' \times {C_2}'} = "BM",
<8em,-6em>*+{ {C_2}'} = "BR",
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f_1},
"TM";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{p_1},
"TM";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{p_2},
"BM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{q_1},
"BM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{q_2},
"TM";"BM" **@{--} ?>*@{>} ?<>(.5)*!/_2.7em/{f_1 \times f_2},
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f_2},
\end{xy}$</nowiki>
where $\tuple{C_1 \times C_2, p_1, p_2}$ and $\tuple{ {C_1}' \times {C_2}', q_1, q_2}$ are the binary products of $C_1, C_2$ and ${C_1}', {C_2}'$ respectively.
Let $\tuple{f_1: C_1 \to {C_1}', f_2: C_2 \to {C_2}'} \in \mathbf {C \times C}$ be a morphism of the product category $\mathbf {C \times C}$.
Let: 
:$\tuple {\map \otimes {C_1,  C_2}, p_1, p_2 }$
and:
:$\tuple {\map \otimes { {C_1},  '{C_2}'}, q_1, q_2 }$
denote the binary products of $\tuple{C_1,  C_2}$ and $\tuple { {C_1},  '{C_2}'}$ respectively.
By the definition of counit of adjunction:
:$\pi : \Delta \otimes \to \operatorname{id}_{\mathbf {C \times C} }$ is a natural transformation.
By definition of natural transformation, the following diagram commutes:
::<nowiki>$\begin{xy}
<-6em,0em>*+{\paren{\Delta \otimes} {\tuple{C_1, C_2} } } = "TL",
<6em,0em>*+{\tuple{ C_1, C_2} } = "TR",
<-6em,-6em>*+{\paren{\Delta \otimes} {\tuple{ {C_1}', {C_2}'} } } = "BL",
<6em,-6em>*+{\tuple{ {C_1}', {C_2}'} } = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\pi_{\tuple{C_1, C_2} } },
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\pi_{\tuple{ {C_1}', {C_2}'} } },
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^3.2em/{\paren{\Delta \otimes} {\tuple{f_1, f_2} } },
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_2em/{\tuple{f_1, f_2} },
\end{xy}$</nowiki>
Substituting $(2)$, $(5)$, and $(6)$ into the diagram above, the following diagram commutes:
::<nowiki>$\begin{xy}
<-6em,0em>*+{\tuple{C_1 \times C_2, C_1 \times C_2} } = "TL",
<6em,0em>*+{\tuple{ C_1, C_2} } = "TR",
<-6em,-6em>*+{\tuple{ {C_1}' \times {C_2}', {C_1}' \times {C_2}' } } = "BL",
<6em,-6em>*+{\tuple{ {C_1}', {C_2}'} } = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\tuple{p_1, p_2} },
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\tuple{q_1, q_2} },
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^5.2em/{\tuple{\otimes \tuple{f_1, f_2}, \otimes \tuple{f_1, f_2} }  },
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_2em/{\tuple{f_1, f_2} },
\end{xy}$</nowiki>
By definition of composition in product category the above diagram commutes in each component of the product category.
Hence the following diagram commutes:
::<nowiki>$\begin{xy}
<-8em,0em>*+{C_1} = "TL",
<0em,0em>*+{C_1 \times C_2} = "TM",
<8em,0em>*+{C_2} = "TR",
<-8em,-6em>*+{ {C_1}'} = "BL",
<0em,-6em>*+{ {C_1}' \times {C_2}'} = "BM",
<8em,-6em>*+{ {C_2}'} = "BR",
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f_1},
"TM";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{p_1},
"TM";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{p_2},
"BM";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{q_1},
"BM";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{q_2},
"TM";"BM" **@{-} ?>*@{>} ?<>(.5)*!/_2.7em/{\otimes \tuple{f_1, f_2} },
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f_2},
\end{xy}$</nowiki>
By uniqueness of $\times \tuple {f_1, f_2}$:
:$\otimes \tuple {f_1, f_2} = \times \tuple {f_1, f_2}$
This completes the proof that $\otimes = \times$.
Hence the right adjoint $\otimes:\mathbf {C \times C} \to \mathbf C$ of $\Delta$ is the product functor.