The Clowder Project

We claim that we have a bijection

natural in $(K,k_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$. Indeed, this bijection is a restriction of the bijection

of Chapter 4: Constructions With Sets, Item 2 of Proposition 4.1.3.1.3:

• •

  A map

  
  in $\mathsf{Sets}(A,\mathsf{Sets}_{*}(X,K))$ gets sent to the map
  \[ \xi ^{\dagger }\colon A\times X\to K \]

  defined by

  \[ \xi ^{\dagger }(a,x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}(x) \]

  for each $(a,x)\in A\times X$, which indeed lies in $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}(A\times X,K)$, as we have

  \begin{align*} \xi ^{\dagger }(a,x_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}(x_{0})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}k_{0}\end{align*}

  for each $a\in A$, where we have used that $\xi _{a}\in \mathsf{Sets}_{*}(X,K)$ is a morphism of pointed sets.

• •

  Conversely, a map

  \[ \xi \colon A\times X\to K \]

  in $\mathsf{Sets}^{\otimes }_{\mathbb {E}_{0}}(A\times X,K)$ gets sent to the map

  
  where
  \[ \xi ^{\dagger }_{a}\colon X \to K \]

  is the map defined by

  \[ \xi ^{\dagger }_{a}(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (a,x) \]

  for each $x\in X$, and indeed lies in $\mathsf{Sets}_{*}(X,K)$, as we have

  \begin{align*} \xi ^{\dagger }_{a}(x_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (a,x_{0})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}k_{0}.\end{align*}

This finishes the proof.

(Proven below in a bit.)

We claim we have a bijection

natural in $(K,k_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$.

1. 1.

   Map I. We define a map

   \[ \Phi _{K}\colon \mathsf{Sets}_{*}(A\odot X,K) \to \mathsf{Sets}(A,\mathsf{Sets}_{*}(X,K)) \]

   by sending a morphism of pointed sets

   \[ \xi \colon (A\odot X,a\odot x_{0})\to (K,k_{0}) \]

   to the map of sets

   
   where
   \[ \xi _{a}\colon (X,x_{0})\to (K,k_{0}) \]

   is the morphism of pointed sets defined by

   \[ \xi _{a}(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (a\odot x) \]

   for each $x\in X$. Note that we have

   \begin{align*} \xi _{a}(x_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (a\odot x_{0})\\ & = k_{0},\end{align*}

   so that $\xi _{a}$ is indeed a morphism of pointed sets, where we have used that $\xi $ is a morphism of pointed sets.

2. 2.

   Map II. We define a map

   \[ \Psi _{K}\colon \mathsf{Sets}(A,\mathsf{Sets}_{*}(X,K))\to \mathsf{Sets}_{*}(A\odot X,K) \]

   given by sending a map

   
   to the morphism of pointed sets
   \[ \xi ^{\dagger }\colon (A\odot X,a\odot x_{0})\to (K,k_{0}) \]

   defined by

   \[ \xi ^{\dagger }(a\odot x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}(x) \]

   for each $a\odot x\in A\odot X$. Note that $\xi ^{\dagger }$ is indeed a morphism of pointed sets, as we have

   \begin{align*} \xi ^{\dagger }(a\odot x_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{a}(x_{0})\\ & = k_{0}, \end{align*}

   where we have used that $\xi (a)\in \mathsf{Sets}_{*}(X,K)$ is a morphism of pointed sets.

3. 3.

   Invertibility I. We claim that

   \[ \Psi _{K}\circ \Phi _{K}=\operatorname {\mathrm{id}}_{\mathsf{Sets}_{*}(A\odot X,K)}. \]

   Indeed, given a morphism of pointed sets

   \[ \xi \colon (A\odot X,a\odot x_{0})\to (K,k_{0}), \]

   we have

   \begin{align*} [\Psi _{K}\circ \Phi _{K}](\xi ) & = \Psi _{K}(\Phi _{K}(\xi ))\\ & = \Psi _{K}([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[x\mapsto \xi (a\odot x)]\mspace {-3mu}]]\mspace {-3mu}])\\ & = \Psi _{K}([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[x'\mapsto \xi (a'\odot x')]\mspace {-3mu}]]\mspace {-3mu}])\\ & = [\mspace {-3mu}[a\odot x\mapsto \mathrm{ev}_{x}(\mathrm{ev}_{a}([\mspace {-3mu}[a'\mapsto [\mspace {-3mu}[x'\mapsto \xi (a'\odot x')]\mspace {-3mu}]]\mspace {-3mu}]))]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\odot x\mapsto \mathrm{ev}_{x}([\mspace {-3mu}[x'\mapsto \xi (a\odot x')]\mspace {-3mu}])]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\odot x\mapsto \xi (a\odot x)]\mspace {-3mu}]\\ & = \xi .\end{align*}
4. 4.

   Invertibility II. We claim that

   \[ \Phi _{K}\circ \Psi _{K}=\operatorname {\mathrm{id}}_{\mathsf{Sets}(A,\mathsf{Sets}_{*}(X,K))}. \]

   Indeed, given a morphism $\xi \colon A\to \mathsf{Sets}_{*}(X,K)$, we have

   \begin{align*} [\Phi _{K}\circ \Psi _{K}](\xi ) & = \Phi _{K}(\Psi _{K}(\xi ))\\ & = \Phi _{K}([\mspace {-3mu}[a\odot x\mapsto \xi _{a}(x)]\mspace {-3mu}])\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[x\mapsto \xi _{a}(x)]\mspace {-3mu}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto \xi (a)]\mspace {-3mu}]\\ & = \xi .\end{align*}
5. 5.

   Naturality of $\Phi $. We need to show that, given a morphism of pointed sets

   \[ \phi \colon (K,k_{0})\to (K',k'_{0}), \]

   the diagram

   
   commutes. Indeed, given a morphism of pointed sets
   \[ \xi \colon (A\odot X,a\odot x_{0})\to (K,k_{0}), \]

   we have

   \begin{align*} [\Phi _{K'}\circ \phi _{*}](\xi ) & = \Phi _{K'}(\phi _{*}(\xi ))\\ & = \Phi _{K'}(\phi \circ \xi )\\ & = (\phi \circ \xi )^{\dagger }\\ & = [\mspace {-3mu}[a\mapsto \phi \circ \xi (a\odot -)]\mspace {-3mu}]\\ & = [\mspace {-3mu}[a\mapsto \phi _{*}(\xi (a\odot -))]\mspace {-3mu}]\\ & = (\phi _{*})_{*}([\mspace {-3mu}[a\mapsto \xi (a\odot -]\mspace {-3mu}]))\\ & = (\phi _{*})_{*}(\Phi _{K}(\xi ))\\ & = [(\phi _{*})_{*}\circ \Phi _{K}](\xi ). \end{align*}
6. 6.

   Naturality of $\Psi $. Since $\Phi $ is natural and $\Phi $ is a componentwise inverse to $\Psi $, it follows from Chapter 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\Psi $ is also natural.

This finishes the proof.