The Clowder Project

This follows from the bijection

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

We claim we have a bijection

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

1. 1.

   Map I. We define a map

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

   by sending a morphism of pointed sets

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

   to the map of sets

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

   is the morphism of pointed sets defined by

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

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

   1. (a)

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

      \begin{align*} \xi \webleft (k\webright ) & = \webleft [\webleft (x^{k}_{a}\webright )_{a\in A}\webright ]\\ & = \webleft [\webleft (y^{k}_{a}\webright )_{a\in A}\webright ] \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*} \webleft [\webleft (x^{k}_{a}\webright )_{a\in A}\webright ] & = \webleft [\webleft (x_{0}\webright )_{a\in A}\webright ],\\ \webleft [\webleft (y^{k}_{a}\webright )_{a\in A}\webright ] & = \webleft [\webleft (x_{0}\webright )_{a\in A}\webright ], \end{align*}

      however, and $\xi _{a}\webleft (k\webright )$ 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}\webleft (k_{0}\webright )=x_{0} \]

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

2. 2.

   Map II. We define a map

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

   given by sending a map

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

   defined by

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

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

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

   where we have used that $\xi _{a}\in \mathsf{Sets}_{*}\webleft (K,X\webright )$ 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}_{*}\webleft (K,A\pitchfork X\webright )}. \]

   Indeed, given a morphism of pointed sets

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

   we have

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

   Now, we have two cases:

   1. (a)

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

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

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

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

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

4. 4.

   Invertibility II. We claim that

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

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

   \begin{align*} \webleft [\Phi _{K}\circ \Psi _{K}\webright ]\webleft (\xi \webright ) & = \Phi _{K}\webleft (\Psi _{K}\webleft (\xi \webright )\webright )\\ & = \Phi _{K}\webleft ([\mspace {-3mu}[k\mapsto \webleft [\webleft (\xi _{a}\webleft (k\webright )\webright )_{a\in A}\webright ]]\mspace {-3mu}]\webright )\\ & = [\mspace {-3mu}[a\mapsto [\mspace {-3mu}[k\mapsto \xi _{a}\webleft (k\webright )]\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 \webleft (K,k_{0}\webright )\to \webleft (K',k'_{0}\webright ), \]

   the diagram

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