Proof that a category is cartesian closed

category-theorytopos-theory

Suppose that a small category $\mathbf C$ has all the finite products. Then the category $\mathbf{Set}^{\mathbf{C}^{\mathrm {op}}}$ is cartesian closed.

Fix a $P\in \mathbf{C}^{\mathrm {op}}$. Then we know how $-\times P$ is defined, and from Yoneda's lemma we can find its right adjoint $-^P$. In fact, for any $Q\in \mathbf{C}^{\mathrm {op}}$, we have that on an object $C\in \mathbf{C}$ our functor $Q^P(C)$ is defined by $\operatorname {nat}(H_C,Q^P)$, and so by $\operatorname {nat}(H_C\times P,Q)$. My difficulties are in proving the universal property of the counit $\epsilon: Q^P\times P\xrightarrow{_.} Q$, that is defined by $\epsilon_C:(\theta,z)\mapsto \theta(1_C,z)$ for any $C$.

I must prove that (for $R\in \mathbf{C}^{\mathrm {op}}$) given a natural transformation $\phi:R \times P \xrightarrow{_.} Q$, there is a unique $\bar{\phi}$ such that $\epsilon\circ (\bar{\phi}\times 1_{P})=\phi$. So take a natural transformation $\alpha:R\xrightarrow{_.} Q^P$ and suppose that it makes the triangular diagram of the counit commutative. Then for any object $C\in \mathbf{C}$, study the $\alpha_C$; we must define $\alpha_C$ on the elements $x\in RC$. That means, we must define the natural transformation $\alpha_C(x):H_C\times P\xrightarrow{_.} Q$ at every level, i.e. define any $[\alpha_C(x)]_D$ for $D\in \mathbf{C}$. Since I know that $[\alpha_C(x)]_C(1_C,z)$ is equal to $\phi(x,z)$, I presume that the kind of argument that I should use involves Yoneda / universal elements. However in general I must define $[\alpha_C(x)]_D:H_C(D)\times PD\to QD$: starting from $1_C$ I can surely catch any $f:D\to C$, but I don't know how to catch any $y\in PD$ starting from $z\in PC$ (using $Pf$?). I hope I explained well the problem, thanks for any clarify

Best Answer

The point is that when you map $H_D \times P$ to $H_C \times P$ via $Hf$, $\operatorname{1_D}$ goes to $f$ and $z$ is left intact.

What you know is that $\alpha: R\xrightarrow{} Q^P$ will be a natural transformation, so for $f: D \to C$ this has to commute: $\require{AMScd}$ \begin{CD} R(C) @>{\alpha_C}>> \{H_C \times P \to Q\} \\ @VRfVV @VVprecomposition \>with\> Hf \times idV \\ R(D) @>{\alpha_D}>> \{H_D \times P \to Q\}. \end{CD}

This means that this commutes: \begin{CD} H_D \times P @>{\alpha_D(Rf(x))}>> Q \\ @VHf \times idVV @VV=V \\ H_C \times P @>{\alpha_C(x)}>> Q. \end{CD}

In particular, plugging in $(\operatorname{1_D}, z) \in H_D(D) \times P(D)$ gives $\alpha_C(x)(f,z) = \alpha_D(Rf(x))((\operatorname{1_D}, z)) = \phi(Rf(x),z)$.

Related Question