Proving that $\text{Set}^{\mathcal{C}}$ is cartesian closed

133 Views Asked by At

Let $\mathcal{C}$ be a small category. I am trying to prove that $\text{Set}^\mathcal{C}$ is cartesian closed.

Given functors $F, G: \mathcal{C} \rightarrow \text{Set}$, define their product to be the functor $F \times G: \mathcal{C}\rightarrow \text{Set}$ determined by:

\begin{equation} \begin{split} X \quad & \mapsto \quad FX \times GX \\ X \xrightarrow{f} Y \quad & \mapsto \quad FX \times GX \xrightarrow{Ff \times Gf} FY \times GY \end{split} \end{equation}

Let $\pi_1: F \times G \Rightarrow F$ be the natural transformation whose component at $X \in \mathcal{C}$ is the projection $\pi_1: FX \times GX \rightarrow FX$. Define $\pi_2: F \times G \Rightarrow G$ similarly.

It can be checked that I have defined products in $\text{Set}^\mathcal{C}$.

Given $X \in \mathcal{C}$, let $G^FX = \text{Nat}(\mathcal{C}(X,-) \times F, G)$. Given a morphism $f: X \rightarrow Y$ in $\mathcal{C}$, let $G^Ff: G^FX \rightarrow G^FY$ be the function that takes a natural transformation $\theta: \mathcal{C}(X, -) \times F \Rightarrow G$, and sends it to the natural transformation $G^Ff(\theta)$ commuting the diagram below

enter image description here

It can be verified that $G^F$ so defined is a functor.

Given $X \in \mathcal{C}$, let $eval_X: G^FX \times FX \Rightarrow GX$ be given by

$$eval_X(\theta, x) = \theta_X(1_X, x)$$

It can be verified that those maps are the components of a natural transformation $eval: G^F \times F \Rightarrow G$.

I want to prove that for every natural transformation $\eta: H \times F \Rightarrow G$, there exists a unique $\hat{\eta}: H \Rightarrow G^F$ that makes the diagram below commute

enter image description here

1

There are 1 best solutions below

0
On

After reading this, I have just figured out how to answer my own question.

Suppose $\hat{\eta}: H \Rightarrow G^F \times F$ makes the triangle commute. Let be given $X, Y \in \mathcal C$, $x \in HX$, $a \in FY$, $X \xrightarrow{f} Y$ in $\mathcal{C}$, applying the naturality of $\hat{\eta}$ to $f$ yields the commutative square below:

enter image description here

But this allows us to prove that the triangles below commute

enter image description here

enter image description here

If we push $(1_Y, a)$ through both paths in the triangle above, we get

$${\hat{\eta}_X(x)}_Y(f,a) = {\hat{\eta}_Y(Hf(x))}_Y(1_Y, a) = \eta_Y(Hf(x), a)$$

So, define $\hat{\eta}: H \Rightarrow G^F \times F$ by the equation above. It remains to prove that $\hat{\eta}$ so defined is natural, and that $\hat{\eta}_X(x)$ is natural for every $X \in \mathcal{C}$, $x \in HX$.