Proving some functor is adjoint to another. What to do with naturality condition?

Question

Whenever I want to prove that some functor is (left/right) adjoint to another, I (mostly using hom-set definition) go on smoothly to prove the "isomorphism of the corresponding hom-sets", until it turns to prove the naturality condition: It really sucks! I can't move anymore.

For example, in the case of $(-)\times A \dashv (-)^A$, where $(-)\times A , (-)^A$ are functors $\mathscr C \to \mathscr C $, I can easily confirm that the bijection $Hom_{\mathscr C}(X \times A,Y) \cong Hom_{\mathscr C}(X,Y^A)$ holds for any $X,Y \in \mathscr C$ (by the way this hold by the definition of an exponential, or in general, by its universal mapping property). What I can't prove is that this is natural.

Now I'm wondering if this is easier than I think, which it seems so, as in no reference I see people struggling with the naturality condition, they ignore it so that it's something quite obvious.

Any help will be thanked!

Answer 1

It's often easier to use the "initial object in a comma category" definition of the adjoint, because it's much more concrete. Given $A \in \mathcal{C}$, you must find $i_A : A \to GFA$ such that for any $f: A \to GX$, there is a unique $g: FA \to X$ such that $Gg: GFA \to GX$ has $Gg \circ i_A = f$.

Answer 2

I assume you mean naturality in $A$ in this case, as naturality in $X$ and $Y$ is either true by definition or usually comes for free for the style you are using. The basic result that you need, which you can prove once then forget, is called parameterized representability and is covered in Glynn Winskel's and Mario Cáccamo's lecture notes. That's a PostScript file which is a bit awkward, see also Cáccamo's thesis, A Formal Calculus for Categories.

The statement is: Say you have a bifunctor $B : \mathcal{C}\times\mathcal{D^{op}}\to\mathbf{Set}$ such that for each object $C$ in $\mathcal{C}$ you have a representation of $B(C,-)$, i.e. you have a function from objects of $\mathcal{C}$ to representing objects in $D$, say $F : \text{Ob}(\mathcal{C}) \to \text{Ob}(\mathcal{D})$ and a natural ismorphism $\tau_C : B(C,-)\cong\text{Hom}(-,F(C))$ for each $C$ not a priori natural in $C$. Then this uniquely extends to a functor $F : \mathcal{C} \to \mathcal{D}$ which does make $\tau$ natural in $C$. Prove this.

Applying it to your example, set $B_Y(A,X) = \text{Hom}(X\times A,Y)$ which is represented for each $A$ by $B_Y(A,-)\cong\text{Hom}(-,Y^A)$. Therefore, $Y^A$ is functorial in $A$ and the isomorphisms are natural in $A$.

The upshot is as long as everything is functorial, you never need to worry about naturality in "parameters"; it comes for free. This was important in Cáccamo's thesis where he defined a formal calculus where you really wouldn't want to have side-conditions everywhere to check naturality.