Proposition 3.4.1.1.2 (00BY): Properties of Free Pointed Sets

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

Proposition 3.4.1.1.2 ▶ Properties of Free Pointed Sets

Let $X$ be a set.

Functoriality. The assignment $X\mapsto X^{+}$ defines a functor
\[ \webleft (-\webright )^{+} \colon \mathsf{Sets}\to \mathsf{Sets}_{*}, \]

where
- Action on Objects. For each $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
  
  \[ \webleft [\webleft (-\webright )^{+}\webright ]\webleft (X\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}X^{+}, \]
  
  where $X^{+}$ is the pointed set of Definition 3.4.1.1.1;
- Action on Morphisms. For each morphism $f\colon X\to Y$ of $\mathsf{Sets}$, the image
  
  \[ f^{+}\colon X^{+}\to Y^{+} \]
  
  of $f$ by $\webleft (-\webright )^{+}$ is the map of pointed sets defined by
  
  \[ f^{+}\webleft (x\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} f\webleft (x\webright ) & \text{if $x\in X$,}\\ \star _{Y} & \text{if $x=\star _{X}$.} \end{cases} \]
Adjointness. We have an adjunction
witnessed by a bijection of sets
\begin{align*} \mathsf{Sets}_{*}\webleft (\webleft (X^{+},\star _{X}\webright ),\webleft (Y,y_{0}\webright )\webright )\cong \mathsf{Sets}\webleft (X,Y\webright ),\end{align*}

natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $\webleft (Y,y_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Symmetric Strong Monoidality With Respect to Wedge Sums. The free pointed set functor of Item 1 has a symmetric strong monoidal structure
\[ \webleft (\webleft (-\webright )^{+},\webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \to \webleft (\mathsf{Sets}_{*},\vee ,\text{pt}\webright ), \]

being equipped with isomorphisms of pointed sets

\[ \begin{gathered} \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y} \colon X^{+}\vee Y^{+} \xrightarrow {\cong }\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+},\\ \webleft (-\webright )^{+,\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\emptyset ^{+}, \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Symmetric Strong Monoidality With Respect to Smash Products. The free pointed set functor of Item 1 has a symmetric strong monoidal structure
\[ \webleft (\webleft (-\webright )^{+},\webleft (-\webright )^{+,\times },\webleft (-\webright )^{+,\times }_{\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets}_{*},\wedge ,S^{0}\webright ), \]

being equipped with isomorphisms of pointed sets

\[ \begin{gathered} \webleft (-\webright )^{+,\times }_{X,Y} \colon X^{+}\wedge Y^{+} \xrightarrow {\cong }\webleft (X\times Y\webright )^{+},\\ \webleft (-\webright )^{+,\times }_{\mathbb {1}} \colon S^{0} \xrightarrow {\cong }\text{pt}^{+}, \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

Proof of Proposition 3.4.1.1.2.

Item 1: Functoriality

Clear.

Item 2: Adjointness

We claim there’s an adjunction $\webleft (-\webright )^{+}\dashv {\text{忘}}$, witnessed by a bijection of sets

\begin{align*} \mathsf{Sets}_{*}\webleft (\webleft (X^{+},\star _{X}\webright ),\webleft (Y,y_{0}\webright )\webright )\cong \mathsf{Sets}\webleft (X,Y\webright ),\end{align*}

natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $\webleft (Y,y_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.

Map I. We define a map

\[ \Phi _{X,Y}\colon \mathsf{Sets}_{*}\webleft (\webleft (X^{+},\star _{X}\webright ),\webleft (Y,y_{0}\webright )\webright )\to \mathsf{Sets}\webleft (X,Y\webright ) \]

by sending a pointed function

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

to the function

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

given by

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

for each $x\in X$.
Map II. We define a map

\[ \Psi _{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright )\to \mathsf{Sets}_{*}\webleft (\webleft (X^{+},\star _{X}\webright ),\webleft (Y,y_{0}\webright )\webright ) \]

given by sending a function $\xi \colon X\to Y$ to the pointed function

\[ \xi ^{\dagger }\colon \webleft (X^{+},\star _{X}\webright )\to \webleft (Y,y_{0}\webright ) \]

defined by

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

for each $x\in X^{+}$.
Invertibility I. We claim that

\[ \Psi _{X,Y}\circ \Phi _{X,Y}=\text{id}_{\mathsf{Sets}_{*}\webleft (\webleft (X^{+},\star _{X}\webright ),\webleft (Y,y_{0}\webright )\webright )}, \]

which is clear.
Invertibility II. We claim that

\[ \Phi _{X,Y}\circ \Psi _{X,Y}=\text{id}_{\mathsf{Sets}\webleft (X,Y\webright )}, \]

which is clear.
Naturality for $\Phi $, Part I. We need to show that, given a pointed function $g\colon \webleft (Y,y_{0}\webright )\to \webleft (Y',y'_{0}\webright )$, the diagram

commutes. Indeed, given a pointed function

\[ \xi ^{\dagger }\colon \webleft (X^{+},\star _{X}\webright )\to \webleft (Y,y_{0}\webright ) \]

we have

\begin{align*} \webleft [\Phi _{X,Y'}\circ g_{*}\webright ]\webleft (\xi \webright ) & = \Phi _{X,Y'}\webleft (g_{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{X,Y'}\webleft (g\circ \xi \webright )\\ & = g\circ \xi \\ & = g\circ \Phi _{X,Y'}\webleft (\xi \webright )\\ & = g_{*}\webleft (\Phi _{X,Y'}\webleft (\xi \webright )\webright )\\ & = \webleft [g_{*}\circ \Phi _{X,Y'}\webright ]\webleft (\xi \webright ). \end{align*}
Naturality for $\Phi $, Part II. We need to show that, given a pointed function $f\colon \webleft (X,x_{0}\webright )\to \webleft (X',x'_{0}\webright )$, the diagram

commutes. Indeed, given a function

\[ \xi \colon X'\to Y, \]

we have

\begin{align*} \webleft [\Phi _{X,Y}\circ f^{*}\webright ]\webleft (\xi \webright ) & = \Phi _{X,Y}\webleft (f^{*}\webleft (\xi \webright )\webright )\\ & = \Phi _{X,Y}\webleft (\xi \circ f\webright )\\ & = \xi \circ f\\ & = \Phi _{X',Y}\webleft (\xi \webright )\circ f\\ & = f^{*}\webleft (\Phi _{X',Y}\webleft (\xi \webright )\webright )\\ & = f^{*}\webleft (\Phi _{X',Y}\webleft (\xi \webright )\webright )\\ & = \webleft [f^{*}\circ \Phi _{X',Y}\webright ]\webleft (\xi \webright ). \end{align*}
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 8: Categories, Item 2 of Proposition 8.8.6.1.2 that $\Psi $ is also natural in each argument.

Item 3: Symmetric Strong Monoidality With Respect to Wedge Sums

The isomorphism

\[ \phi \colon X^{+}\vee Y^{+}\xrightarrow {\cong }\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+} \]

is given by

\[ \phi \webleft (z\webright )=\begin{cases} x & \text{if $z=\webleft [\webleft (0,x\webright )\webright ]$ with $x\in X$,}\\ y & \text{if $z=\webleft [\webleft (1,y\webright )\webright ]$ with $y\in Y$,}\\ \star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y} & \text{if $z=\webleft [\webleft (0,\star _{X}\webright )\webright ]$,}\\ \star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y} & \text{if $z=\webleft [\webleft (1,\star _{Y}\webright )\webright ]$}\end{cases} \]

for each $z\in X^{+}\vee Y^{+}$, with inverse

\[ \phi ^{-1} \colon \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+} \xrightarrow {\cong }X^{+}\vee Y^{+} \]

given by

\[ \phi ^{-1}\webleft (z\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} \webleft [\webleft (0,x\webright )\webright ] & \text{if $z=\webleft [\webleft (0,x\webright )\webright ]$,}\\ \webleft [\webleft (0,y\webright )\webright ] & \text{if $z=\webleft [\webleft (1,y\webright )\webright ]$,}\\ p_{0} & \text{if $z=\star _{X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y}$} \end{cases} \]

for each $z\in \webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )^{+}$.

Meanwhile, the isomorphism $\text{pt}\cong \emptyset ^{+}$ is given by sending $\star _{X}$ to $\star _{\emptyset }$.

That these isomorphisms satisfy the coherence conditions making the functor $\webleft (-\webright )^{+}$ symmetric strong monoidal can be directly checked element by element.

Item 4: Symmetric Strong Monoidality With Respect to Smash Products

The isomorphism

\[ \phi \colon X^{+}\wedge Y^{+}\xrightarrow {\cong }\webleft (X\times Y\webright )^{+} \]

is given by

\[ \phi \webleft (x\wedge y\webright )=\begin{cases} \webleft (x,y\webright ) & \text{if $x\neq \star _{X}$ and $y\neq \star _{Y}$}\\ \star _{X\times Y} & \text{otherwise}\end{cases} \]

for each $x\wedge y\in X^{+}\wedge Y^{+}$, with inverse

\[ \phi ^{-1} \colon \webleft (X\times Y\webright )^{+} \xrightarrow {\cong }X^{+}\wedge Y^{+} \]

given by

\[ \phi ^{-1}\webleft (z\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\begin{cases} x\wedge y & \text{if $z=\webleft (x,y\webright )$ with $\webleft (x,y\webright )\in X\times Y$,}\\ \star _{X}\wedge \star _{Y} & \text{if $z=\star _{X\times Y}$,}\\ \end{cases} \]

Meanwhile, the isomorphism $S^{0}\cong \text{pt}^{+}$ is given by sending $\star $ to $1\in S^{0}=\webleft\{ 0,1\webright\} $ and $\star _{\text{pt}}$ to $0\in S^{0}$.

That these isomorphisms satisfy the coherence conditions making the functor $\webleft (-\webright )^{+}$ symmetric strong monoidal can be directly checked element by element.

Noticed something off, or have any comments? Feel free to reach out!

You can also use the contact form below: