Theorem: Diagonal Functor on Product Category has Left Adjoint Iff Category has Binary Coproducts/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 coproducts.
Then $\Delta$ has a left adjoint.

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