The Clowder Project

• •

  Preservation of Identities. Let $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$. We have

  \[ \operatorname {\mathrm{id}}^{-}_{X}(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x \]

  for each $x\in X^{-}$, so $\operatorname {\mathrm{id}}^{-}_{X}=\operatorname {\mathrm{id}}_{X^{-}}$.

• •

  Preservation of Composition. Given morphisms of pointed sets

  \begin{align*} f & \colon (X,x_{0}) \to (Y,y_{0}),\\ g & \colon (Y,y_{0}) \to (Z,z_{0}), \end{align*}

  we have

  \begin{align*} [g^{-}\circ f^{-}](x) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{-}(f^{-}(x))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g^{-}(f(x))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g(f(x))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[g\circ f]^{-}(x)\end{align*}

  for each $x\in X$, so $(g\circ f)^{-}=g^{-}\circ f^{-}$.

This finishes the proof.

1. 1.

   Map I. We define a map

   \[ \Phi _{X,Y}\colon \mathsf{Sets}(X^{-},Y)\to \mathsf{Sets}^{\mathrm{actv}}_{*}(X,Y^{+}) \]

   by sending a map $\xi \colon X^{-}\to Y$ to the active morphism of pointed sets

   \[ \xi ^{\dagger }\colon X\to Y^{+} \]

   given by

   \[ \xi ^{\dagger }(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \xi (x) & \text{if $x\in X^{-}$,}\\ \star _{Y} & \text{if $x=x_{0}$,} \end{cases} \]

   for each $x\in X$, where this morphism is indeed active since $\xi (x)\in Y=Y^{+}\setminus \left\{ \star _{Y}\right\} $ for all $x\in X^{-}$.

2. 2.

   Map II. We define a map

   \[ \Psi _{X,Y}\colon \mathsf{Sets}^{\mathrm{actv}}_{*}(X,Y^{+})\to \mathsf{Sets}(X^{-},Y) \]

   given by sending an active morphism of pointed sets $\xi \colon X\to Y^{+}$ to the map

   \[ \xi ^{\dagger }\colon X^{-}\to Y \]

   defined by

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

   for each $x\in X^{-}$, which is indeed well-defined (in that $\xi (x)\in Y$ for all $x\in X^{-}$) since $\xi $ is active.

3. 3.

   Invertibility I. Given a map of sets $\xi \colon X^{-}\to Y$, we have

   \begin{align*} [\Psi _{X,Y}\circ \Phi _{X,Y}](\xi ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}(\Phi _{X,Y}(\xi ))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}(\left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi (x)& \text{if $x\in X^{-}$}\\ \star _{Y}& \text{if $x=x_{0}$}\end{cases}}\right]\mspace {-6mu}\right])\\ & = [\mspace {-3mu}[x\mapsto \xi (x)]\mspace {-3mu}]\\ & = \xi \\ & = [\operatorname {\mathrm{id}}_{\mathsf{Sets}(X^{-},Y)}](\xi ). \end{align*}

   Therefore we have

   \[ \Psi _{X,Y}\circ \Phi _{X,Y}=\operatorname {\mathrm{id}}_{\mathsf{Sets}(X^{-},Y)}. \]
4. 4.

   Invertibility II. Given a morphism of pointed sets

   \[ \xi \colon (X,x_{0})\to (Y^{+},\star _{Y}), \]

   we have

   \begin{align*} [\Phi _{X,Y}\circ \Psi _{X,Y}](\xi ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}(\Psi _{X,Y}(\xi ))\\ & = \Phi _{X,Y}([\mspace {-3mu}[x\mapsto \xi (x)]\mspace {-3mu}])\\ & = \left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi (x)& \text{if $x\in X^{-}$}\\ \star _{Y}& \text{if $x=x_{0}$}\end{cases}}\right]\mspace {-6mu}\right]\\ & = \xi \\ & = [\operatorname {\mathrm{id}}_{\mathsf{Sets}^{\mathrm{actv}}_{*}(X,Y^{+})}](\xi ). \end{align*}

   Therefore we have

   \[ \Phi _{X,Y}\circ \Psi _{X,Y}=\operatorname {\mathrm{id}}_{\mathsf{Sets}^{\mathrm{actv}}_{*}(X,Y^{+})}. \]
5. 5.

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

   \[ f\colon (X,x_{0})\to (X',x'_{0}), \]

   the diagram

   
   commutes. Indeed, given a map of sets $\xi \colon X'\to Y$, we have
   \begin{align*} [\Phi _{X,Y}\circ f^{*}](\xi ) & = \Phi _{X,Y}(f^{*}(\xi ))\\ & = \Phi _{X,Y}(\xi \circ f)\\ & = \left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi (f(x))& \text{if $f(x)\in X^{\prime ,-}$}\\ \star _{Y}& \text{if $f(x)=x'_{0}$}\end{cases}}\right]\mspace {-6mu}\right]\\ & = f^{*}(\left[\mspace {-6mu}\left[x'\mapsto {\begin{cases} \xi (x')& \text{if $x'\in X^{\prime ,-}$}\\ \star _{Y}& \text{if $x'=x'_{0}$}\end{cases}}\right]\mspace {-6mu}\right])\\ & = f^{*}(\Phi _{X',Y}(\xi ))\\ & = [f^{*}\circ \Phi _{X',Y}](\xi ). \end{align*}

   Therefore we have

   \[ \Phi _{X,Y}\circ f^{*}=f^{*}\circ \Phi _{X',Y}, \]

   and the naturality diagram for $\Phi $ above indeed commutes.

6. 6.

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

   \[ g\colon (Y,y_{0})\to (Y',y'_{0}), \]

   the diagram

   
   commutes. Indeed, given a map of sets $\xi \colon X^{-}\to Y$, we have
   \begin{align*} [\Phi _{X,Y'}\circ g_{*}](\xi ) & = \Phi _{X,Y'}(g_{*}(\xi ))\\ & = \Phi _{X,Y'}(g\circ \xi )\\ & = \left[\mspace {-6mu}\left[x\mapsto {\begin{cases} g(\xi (x))& \text{if $x\in X^{-}$}\\ \star _{Y'}& \text{if $x=x_{0}$}\end{cases}}\right]\mspace {-6mu}\right]\\ & = g_{*}(\left[\mspace {-6mu}\left[x\mapsto {\begin{cases} \xi (x)& \text{if $x\in X^{-}$}\\ \star _{Y}& \text{if $x=x_{0}$}\end{cases}}\right]\mspace {-6mu}\right])\\ & = g_{*}(\Phi _{X,Y'}(\xi ))\\ & = [g_{*}\circ \Phi _{X,Y'}](\xi ). \end{align*}

   Therefore we have

   \[ \Phi _{X,Y'}\circ g_{*}=g_{*}\circ \Phi _{X,Y'}, \]

   and the naturality diagram for $\Phi $ above indeed commutes.

7. 7.

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

8. 8.

   Fully Faithfulness of $(-)^{-}$. We aim to show that the assignment $f\mapsto f^{-}$ sets up a bijection

   \[ (-)^{-}_{X,Y}\colon \mathsf{Sets}^{\mathrm{actv}}_{*}(X,Y)\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathsf{Sets}(X^{-},Y^{-}). \]

   Indeed, the inverse map

   \[ (-)^{-,-1}_{X,Y}\colon \mathsf{Sets}(X^{-},Y^{-})\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathsf{Sets}^{\mathrm{actv}}_{*}(X,Y) \]

   is given by sending a map of sets $f\colon X^{-}\to Y^{-}$ to the active morphism of pointed sets $f^{\dagger }\colon X\to Y$ defined by

   \[ f^{\dagger }(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} f(x) & \text{if $x\in X^{-}$,}\\ y_{0} & \text{if $x=x_{0}$} \end{cases} \]

   for each $x\in X$.

9. 9.

   Essential Surjectivity of $(-)^{-}$. We need to show that, given an object $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, there exists some $X'\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}^{\mathrm{actv}}_{*})$ such that $(X')^{-}\cong X$. Indeed, taking $X'=X^{+}$, we have

   \begin{align*} (X^{+})^{-} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(X\cup \left\{ \star _{X}\right\} )^{-}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(X\cup \left\{ \star _{X}\right\} )\setminus \left\{ \star _{X}\right\} \\ & = X, \end{align*}

   and thus we have in fact an equality $(X^{+})^{-}=X$, showing $(-)^{-}$ to be essentially surjective.

10. 10.

    The Functor $(-)^{-}$ Is an Equivalence. Since $(-)^{-}$ is fully faithful and essentially surjective, it is an equivalence by Chapter 11: Categories, Item 1 of Proposition 11.6.7.1.2.

This finishes the proof.

• •

  The Strong Monoidality Constraints. The isomorphism

  \[ (-)^{-,\vee }_{X,Y}\colon X^{-}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y^{-}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(X\vee Y)^{-} \]

  is given by

  \[ (-)^{-,\vee }_{X,Y}(z)=\begin{cases} [(0,x)] & \text{if $z=(0,x)$ with $x\in X$,}\\ [(1,y)] & \text{if $z=(1,y)$ with $y\in Y$}\end{cases} \]

  for each $z\in X^{-}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y^{-}$, with inverse

  \[ (-)^{-,\vee ,-1}_{X,Y} \colon (X\vee Y)^{-} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X^{-}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y^{-} \]

  given by

  \[ (-)^{-,\vee ,-1}_{X,Y}(z)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} (0,x) & \text{if $z=[(0,x)]$,}\\ (1,y) & \text{if $z=[(1,y)]$,} \end{cases} \]

  for each $z\in (X\vee Y)^{-}$.

• •

  The Strong Monoidal Unity Constraint. The isomorphism

  \[ (-)^{+,\vee ,\mathbb {1}}_{X,Y}\colon \text{Ø}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\mathrm{pt}^{-} \]

  is an equality.

The verification that these isomorphisms satisfy the coherence conditions making the functor $(-)^{-}$ into a symmetric strong monoidal functor is omitted.

• •

  The Strong Monoidality Constraints. The isomorphism

  \[ (-)^{-}_{X,Y}\colon X^{-}\times Y^{-}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(X\wedge Y)^{-} \]

  is given by

  \[ (-)^{-}_{X,Y}(x,y)=x\wedge y \]

  for each $(x,y)\in X^{-}\times Y^{-}$, with inverse

  \[ (-)^{-,-1}_{X,Y} \colon (X\wedge Y)^{-} \overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X^{-}\times Y^{-} \]

  given by

  \[ (-)^{-,-1}_{X,Y}(x\wedge y)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(x,y) \]

  for each $x\wedge y\in (X\wedge Y)^{-}$.

• •

  The Strong Monoidal Unity Constraint. The isomorphism

  \[ (-)^{-,\mathbb {1}}_{X,Y}\colon \mathrm{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }(S^{0})^{-} \]

  is given by sending $\star $ to $1$.

The verification that these isomorphisms satisfy the coherence conditions making the functor $(-)^{+}$ into a symmetric strong monoidal functor is omitted.