Theorem: Uniqueness of Representing Objects

Let $C$ be a locally small category.
Let $\mathbf{Set}$ be the category of sets.
Let $F : \mathbf C \to \mathbf{Set}$ be a covariant functor.
Let $(A, \eta)$ and $(B, \xi)$ be representations of $F$.
Then there exists a unique isomorphism $f : A \to B$ such that $\eta \circ h^f = \xi$, where:
:$h^f$ is the precomposition natural transformation
:$\circ$ denotes vertical composition of natural transformations

Proof:
As $\eta : \map {\operatorname {Hom} } {A, \cdot} \to F$ is a natural isomorphism, it has an inverse:
:$\eta' : F \to \map {\operatorname {Hom} } {A, \cdot}$
Similarly, $\xi : \map {\operatorname {Hom} } {B, \cdot} \to F$ also has an inverse:
:$\xi' : F \to \map {\operatorname {Hom} } {B, \cdot}$
Let $\phi = \eta' \circ \xi$ be the vertical composition.
By Vertical Composition of Natural Transformations is Natural Transformation:
:$\phi : \map {\operatorname {Hom} } {B, \cdot} \to \map {\operatorname {Hom} } {A, \cdot}$
is a natural transformation.
$\phi$ is a natural isomorphism, as $\xi$ and $\eta'$ are so.
{{ExtractTheorem|Vertical Composition of Natural Isomorphisms is Natural Isomorphism}}
Specifically, let $\phi' := \xi' \circ \eta$.
Then:
:$\phi' : \map {\operatorname {Hom} } {A, \cdot} \to \map {\operatorname {Hom} } {B, \cdot}$
is a natural transformation such that:
:$\phi' \circ \phi = \operatorname{id}_{\map {\operatorname {Hom} } {B, \cdot} }$
:$\phi \circ \phi' = \operatorname{id}_{\map {\operatorname {Hom} } {A, \cdot} }$
That is, $\phi'$ is an inverse to $\phi$.
Observe also that $\phi$ satisfies:
{{begin-eqn}}
{{eqn | l = \eta \circ \phi
      | r = \eta \circ \paren {\eta' \circ \xi}
}}
{{eqn | r = \paren {\eta \circ \eta'} \circ \xi
      | c = Vertical Composition of Natural Transformations is Associative
}}
{{eqn | r = \operatorname{id}_F \circ \xi
      | c = {{Defof|Inverse Natural Isomorphism between Covariant Functors}}
}}
{{eqn | r = \xi
      | c = Identity Natural Transformation is Left Identity
}}
{{end-eqn}}
Now we need to find an $f \in \map {\operatorname {Hom} } {A, B}$ such that $\phi = h^f$.
If such an $f$ exists, it must satisfy:
:$f = \map {\paren {h^f}_B} {\operatorname{id}_B}$
Thus a unique candidate is:
:$f := \map {\phi_B} {\operatorname{id}_B}$
Let $C$ be an object of $\mathbf C$.
Let $g \in \map {\operatorname {Hom} } {B, C}$.
As $\phi$ is natural, the following commutes:
:<nowiki>$\xymatrix{
\map {\operatorname {Hom} } {B, B} \ar[r]^{ \map {\operatorname {Hom} } {B, g} }\ar[d]_{\phi_B} & \map {\operatorname {Hom} } {B, C}  \ar[d]^{\phi_C} \\
\map {\operatorname {Hom} } {A, B} \ar[r]_{ \map {\operatorname {Hom} } {A, g} } & \map {\operatorname {Hom} } {A, C} }$
</nowiki>
In particular:
{{begin-eqn}}
{{eqn | l = \map {\phi_C} g
      | r = \map {\phi_C} {g \circ \operatorname{id}_B}
      | c = definition of $\operatorname{id}_B$
}}
{{eqn | r = \map {\phi_C} {\map {\map {\operatorname {Hom} } {B, g} } {\operatorname{id}_B} }
      | c = definition of $\map {\operatorname {Hom} } {B, g}$
}}
{{eqn | r = \map {\paren {\phi_C \circ \map {\operatorname {Hom} } {B, g} } } {\operatorname{id}_B}
      | c = definition of $\circ$
}}
{{eqn | r = \map {\paren {\map {\operatorname {Hom} } {A, g} \circ \phi_B} }{\operatorname{id}_B}
      | c = above commutative diagram
}}
{{eqn | r = \map {\map {\operatorname {Hom} } {A, g} } {\map {\phi_B} { \operatorname{id}_B} }
      | c = definition of $\circ$
}}
{{eqn | r = \map {\map {\operatorname {Hom} } {A, g} } f
      | c = definition of $f$
}}
{{eqn | r = g \circ f
      | c = definition of $\map {\operatorname {Hom} } {A, g}$
}}
{{eqn | r = \map {\paren {h^f}_C} g
      | c = definition of $h^f$
}}
{{end-eqn}}
Therefore $\phi = h^f$.
Finally, we show that $f$ is an isomorphism.
Let $f' := \map {\phi' _A} {\operatorname{id}_A}$
Then $f' \circ f = \operatorname{id}_A$ follows from the commutative diagram:
:<nowiki>$\xymatrix{
\map {\operatorname {Hom} } {B, B} \ar[r]^{ \map {\operatorname {Hom} } {B, f'} }\ar[d]_{\phi_B} & \map {\operatorname {Hom} } {B, A}  \ar[d]^{\phi_A} \\
\map {\operatorname {Hom} } {A, B} \ar[r]_{ \map {\operatorname {Hom} } {A, f'} } & \map {\operatorname {Hom} } {A, A} }$
</nowiki>
Indeed:
{{begin-eqn}}
{{eqn | l = f' \circ f
      | r = \map {\map {\operatorname {Hom} } {A, f'} } f
      | c = definition of $\map {\operatorname {Hom} } {A, f'}$
}}
{{eqn | r = \map {\map {\operatorname {Hom} } {A, f'} } {\map {\phi_B} {\operatorname{id}_B } }
      | c = definition of $f$
}}
{{eqn | r = \map {\paren {\map {\operatorname {Hom} } {A, f'} \circ \phi_B} }{\operatorname{id}_B }
      | c = definition of $\circ$
}}
{{eqn | r = \map {\paren {\phi_A \circ \map {\operatorname {Hom} } {B, f'} } }{\operatorname{id}_B }
      | c = above commutative diagram
}}
{{eqn | r = \map {\phi_A}{\map {\map {\operatorname {Hom} } {B, f'} } {\operatorname{id}_B} }
      | c = definition of $\circ$
}}
{{eqn | r = \map {\phi_A} {f'}
      | c = definition of $\map {\operatorname {Hom} } {B, f'}$
}}
{{eqn | r = \map {\phi_A} {\map {\phi' _A} {\operatorname{id}_A} }
      | c = definition of $f'$
}}
{{eqn | r = \map {\paren {\phi_A \circ \phi' _A} } {\operatorname{id}_A}
      | c = definition of $\circ$
}}
{{eqn | r = \map {\paren {\phi \circ \phi'}_A } {\operatorname{id}_A}
      | c = definition of $\circ$
}}
{{eqn | r = \map { \paren { \operatorname{id}_{\map {\operatorname {Hom} } {A, \cdot} } }_A } {\operatorname{id}_A}
      | c = $\phi'$ is an inverse to $\phi$
}}
{{eqn | r = \map { \operatorname{id}_{\map {\operatorname {Hom} } {A, A} } } {\operatorname{id}_A}
      | c = definition of $\operatorname{id}_{\map {\operatorname {Hom} } {A, \cdot} }$
}}
{{eqn | r = \operatorname{id}_A
      | c = definition of $\operatorname{id}_{\map {\operatorname {Hom} } {A, A} }$
}}
{{end-eqn}}
Similarly, $f \circ f' = \operatorname{id}_B$ follows from the commutative diagram:
:<nowiki>$\xymatrix{
\map {\operatorname {Hom} } {A, A} \ar[r]^{ \map {\operatorname {Hom} } {B, f} }\ar[d]_{\phi' _A} & \map {\operatorname {Hom} } {A, B}  \ar[d]^{\phi' _B} \\
\map {\operatorname {Hom} } {B, A} \ar[r]_{ \map {\operatorname {Hom} } {A, f} } & \map {\operatorname {Hom} } {B, B} }$
</nowiki>
{{qed}}
Category:Functors
n5whdnfel32kgxuscn77ie62j3k16b1