Theorem: Left Adjoint Functor is Unique up to Natural Isomorphism

Let $\mathbf C$, $\mathbf D$ be locally small categories.
Let  $\tuple {F, G, \alpha}$ be an adjunction between $\mathbf C$ and $\mathbf D$.
Then:
:the left adjoint functor $F$ of $G$ is unique up to isomorphism in the functor category $\operatorname{Funct} \tuple{C, D}$.
That is:
:left adjoint functor $F$ is unique up to natural isomorphism.

Proof:
Let $\tuple {F, G, \alpha}$ and $\tuple {H, G, \gamma}$ be adjunctions between $\mathbf C$ and $\mathbf D$.
From Characterization of Adjunction Using Unit of Adjunction:
:there exists a natural transformation $\eta: \operatorname {id}_{\mathbf D} \to GF$ such that:
::for each object $D$ in $\mathbf D$ the morphism $\eta_D:D \to GFD$ is a universal morphism from object $FD$ to functor $G$
and:
:there exists a natural transformation $\phi: \operatorname {id}_{\mathbf D} \to GH$ such that:
::for each object $D$ in $\mathbf D$ the morphism $\phi_D:D \to GHD$ is a universal morphism from object $HD$ to functor $G$
From Universal Morphism from Object to Functor is Unique up to Isomorphism:
:for each object $D$ in $\mathbf D$ there exists an isomorphism $\theta_D:FD \to HD \in \mathbf C$:
::$(1):\quad \phi_D = G \theta_D \circ \eta_D$
It will be shown that $\theta: F \to H$ is a natural isomorphism.
Let $f: D_1 \to D_2 \in \mathbf D$ is a morphism.
By definition of natrual transformation:
:$(2):\quad \eta_{D_2} \circ f = GFf \circ \eta{D_1}$
:$(3):\quad \phi_{D_2} \circ f = GHf \circ \phi{D_1}$
From $(1)$, $(2)$ and $(3)$ the following diagram commutes:
::<nowiki>$\begin{xy}
<0em,10em>*+{GFD_1} = "TL",
<18em,10em>*+{GFD_2} = "TR",
<4.5em,5em>*+{D_1} = "ML",
<13.5em,5em>*+{D_2} = "MR",
<0em,0em>*+{GHD_1} = "BL",
<18em,0em>*+{GHD_2} = "BR",
<1.5em,5em>*+{(1)} = "L",
<9em,2.5em>*+{(3)} = "T",
<9em,8em>*+{(2)} = "B",
<16.5em,5em>*+{(1)} = "R",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{GFf},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{GHf},
"ML";"MR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^2em/{G\theta_{D_1} },
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_2em/{G\theta_{D_2} },
"ML";"TL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\eta_{D_1} },
"ML";"BL" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\phi_{D_1} },
"MR";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\eta_{D_2} },
"MR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\phi_{D_2} },
\end{xy}$</nowiki>
We have:
{{begin-eqn}}
{{eqn | l = \phi_{D_2} \circ f
      | r = G \theta_{D_2} \circ \eta_{D_2} \circ f
      | c = By $(1)$
}}
{{eqn | r = G \theta_{D_2} \circ GFf \circ \eta_{D_1}
      | c = By $(2)$
}}
{{eqn | r = \map G {\theta_{D_2} \circ Ff} \circ \eta_{D_1}
      | c = {{Defof|Covariant Functor}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \phi_{D_2} \circ f
      | r = GHf \circ \phi_{D_1}
      | c = By $(3)$
}}
{{eqn | r = GHf \circ G \theta_{D_1} \circ \eta_{D_1}
      | c = By $(1)$
}}
{{eqn | r = \map G {Hf \circ \theta_{D_1} } \circ \eta_{D_1}
      | c = {{Defof|Covariant Functor}}
}}
{{end-eqn}}
By universality of $\eta_{D_1}$ applied to $\phi_{D_2} \circ f$:
:$\exists ! g: FD_1 \to HD_2 \in \mathbf C : \phi_{D_2} \circ f = Gg \circ \eta_{D_1}$
Hence:
:$\theta_{D_2} \circ Ff = Hf \circ \theta_{D_1}$
It follows that $\theta$ is a natural isomorphism by definition.
{{qed}}
Category:Adjunctions
Category:Natural Isomorphisms
62rltzi2tc0u8hu4gccgvijq3w6l1zm