The Clowder Project

This follows from the bijection

natural in $(K,k_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$ constructed in the proof of Remark 7.2.1.1.2.

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}_{*}(K,A\pitchfork X)\to \mathsf{Sets}(A,\mathsf{Sets}_{*}(K,X)), \]

   by sending a morphism of pointed sets

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

   to the map of sets

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

   is the morphism of pointed sets defined by

   \[ \xi _{a}(k)=\begin{cases} x^{k}_{a} & \text{if $\xi (k)\neq [(x_{0})_{a\in A}]$,}\\ x_{0} & \text{if $\xi (k)=[(x_{0})_{a\in A}]$}\end{cases} \]

   for each $k\in K$, where $x^{k}_{a}$ is the $a$th component of $\xi (k)=[(x^{k}_{a})_{a\in A}]$. Note that:

   1. (a)

      The definition of $\xi _{a}(k)$ is independent of the choice of equivalence class. Indeed, suppose we have

      \begin{align*} \xi (k) & = [(x^{k}_{a})_{a\in A}]\\ & = [(y^{k}_{a})_{a\in A}] \end{align*}

      with $x^{k}_{a}\neq y^{k}_{a}$ for some $a\in A$. Then there exist $a_{x},a_{y}\in A$ such that $x^{k}_{a_{x}}=y^{k}_{a_{y}}=x_{0}$. The equivalence relation $\mathord {\sim }$ on $\prod _{a\in A}X$ then forces

      \begin{align*} [(x^{k}_{a})_{a\in A}] & = [(x_{0})_{a\in A}],\\ [(y^{k}_{a})_{a\in A}] & = [(x_{0})_{a\in A}], \end{align*}

      however, and $\xi _{a}(k)$ is defined to be $x_{0}$ in this case.

   2. (b)

      The map $\xi _{a}$ is indeed a morphism of pointed sets, as we have

      \[ \xi _{a}(k_{0})=x_{0} \]

      since $\xi (k_{0})=[(x_{0})_{a\in A}]$ as $\xi $ is a morphism of pointed sets and $\xi _{a}(k_{0})$, defined to be the $a$th component of $[(x_{0})_{a\in A}]$, is equal to $x_{0}$.

2. 2.

   Map II. We define a map

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

   given by sending a map

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

   defined by

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

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

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

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

3. 3.

   Invertibility I. We claim that

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

   Indeed, given a morphism of pointed sets

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

   we have

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

   Now, we have two cases:

   1. (a)

      If $\xi (k)=[(x_{0})_{a\in A}]$, we have

      \begin{align*} [\Psi _{K}\circ \Phi _{K}](\xi ) & = [\mspace {-3mu}[k\mapsto [(\xi _{a}(k))_{a\in A}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[k\mapsto [(x_{0})_{a\in A}]]\mspace {-3mu}]\\ & = [\mspace {-3mu}[k\mapsto \xi (k)]\mspace {-3mu}]\\ & = \xi .\end{align*}
   2. (b)

      If $\xi (k)\neq [(x_{0})_{a\in A}]$ and $\xi (k)=[(x^{k}_{a})_{a\in A}]$ instead, we have

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

   In both cases, we have $[\Psi _{K}\circ \Phi _{K}](\xi )=\xi $, and thus we are done.

4. 4.

   Invertibility II. We claim that

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

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

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

   Naturality of $\Psi $. 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 map of sets
   
   we have
   \begin{align*} [\Psi _{K}\circ (\phi ^{*})_{*}](\xi ) & = \Psi _{K}((\phi ^{*})_{*}(\xi ))\\ & = \Psi _{K}((\phi ^{*})_{*}([\mspace {-3mu}[a\mapsto \xi _{a}]\mspace {-3mu}]))\\ & = \Psi _{K}(([\mspace {-3mu}[a\mapsto \phi ^{*}(\xi _{a})]\mspace {-3mu}]))\\ & = \Psi _{K}(([\mspace {-3mu}[a\mapsto [\mspace {-3mu}[k\mapsto \xi _{a}(\phi (k))]\mspace {-3mu}]]\mspace {-3mu}]))\\ & = [\mspace {-3mu}[k\mapsto [(\xi _{a}(\phi (k)))_{a\in A}]]\mspace {-3mu}]\\ & = \phi ^{*}([\mspace {-3mu}[k'\mapsto [(\xi _{a}(k'))_{a\in A}]]\mspace {-3mu}])\\ & = \phi ^{*}(\Psi _{K'}(\xi ))\\ & = [\phi ^{*}\circ \Psi _{K'}](\xi ). \end{align*}
6. 6.

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

This finishes the proof.