4.5.1 Foundations
Let $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ be pointed sets.
The smash product of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ is the pointed set $X\wedge Y$ satisfying the bijection
\[ \mathsf{Sets}_{*}\webleft (X\wedge Y,Z\webright ) \cong \textup{Hom}^{\otimes }_{\mathsf{Sets}_{*}}\webleft (X\times Y,Z\webright ), \]
naturally in $\webleft (X,x_{0}\webright ),\webleft (Y,y_{0}\webright ),\webleft (Z,z_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Concretely, the smash product of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ is the pointed set $\webleft (X\wedge Y,x_{0}\wedge y_{0}\webright )$ consisting of
- The Underlying Set. The set $X\wedge Y$ defined by
\[ X\wedge Y\cong \webleft (X\times Y\webright )/\mathord {\sim }_{R}, \]
where $\mathord {\sim }_{R}$ is the equivalence relation on $X\times Y$ obtained by declaring
\begin{align*} \webleft (x_{0},y\webright ) & \sim _{R} \webleft (x_{0},y'\webright ),\\ \webleft (x,y_{0}\webright ) & \sim _{R} \webleft (x’,y_{0}\webright ) \end{align*}
for each $x,x'\in X$ and each $y,y'\in Y$;
- The Basepoint. The element $\webleft [\webleft (x_{0},y_{0}\webright )\webright ]$ of $X\wedge Y$ given by the equivalence class of $\webleft (x_{0},y_{0}\webright )$ under the equivalence relation $\mathord {\sim }$ on $X\times Y$.
By Chapter 7: Equivalence Relations and Apartness Relations, Item 6 of Proposition 7.5.2.1.3, we have a natural bijection
\[ \mathsf{Sets}_{*}\webleft (X\wedge Y,Z\webright ) \cong \textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright ). \]
Now, by definition, $\textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright )$ is the set
\[ \textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ f\in \textup{Hom}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright )\ \middle |\ \begin{aligned} & \text{for each $x,y\in X$, if}\\ & \text{$\webleft (x,y\webright )\sim _{R}\webleft (x',y'\webright )$, then}\\ & \text{$f\webleft (x,y\webright )=f\webleft (x',y'\webright )$}\end{aligned} \webright\} . \]
However, the condition $\webleft (x,y\webright )\sim _{R}\webleft (x',y'\webright )$ only holds when:
-
We have $x=x'$ and $y=y'$.
-
The following conditions are satisfied:
-
We have $x=x_{0}$ or $y=y_{0}$.
-
We have $x'=x_{0}$ or $y'=y_{0}$.
So, given $f\in \textup{Hom}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright )$ with a corresponding $\overline{f}\colon X\wedge Y\to Z$, the latter case above implies
\begin{align*} f\webleft (x_{0},y\webright ) & = f\webleft (x,y_{0}\webright )\\ & = f\webleft (x_{0},y_{0}\webright ), \end{align*}
and since $\overline{f}\colon X\wedge Y\to Z$ is a pointed map, we have
\begin{align*} f\webleft (x_{0},y_{0}\webright ) & = \overline{f}\webleft (x_{0},y_{0}\webright )\\ & = z_{0}. \end{align*}
Thus the elements $f$ in $\textup{Hom}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright )$ are precisely those functions $f\colon X\times Y\to Z$ satisfying the equalities
\begin{align*} f\webleft (x_{0},y\webright ) & = z_{0},\\ f\webleft (x,y_{0}\webright ) & = z_{0} \end{align*}
for each $x\in X$ and each $y\in Y$, giving an equality
\[ \textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright )=\textup{Hom}^{\otimes }_{\mathsf{Sets}_{*}}\webleft (X\times Y,Z\webright ) \]
of sets, which when composed with our earlier isomorphism
\[ \mathsf{Sets}_{*}\webleft (X\wedge Y,Z\webright ) \cong \textup{Hom}^{R}_{\mathsf{Sets}}\webleft (X\times Y,Z\webright ) \]
gives our desired natural bijection, finishing the proof.
We write $x\wedge y$ for the element $\webleft [\webleft (x,y\webright )\webright ]$ of
\[ X\wedge Y\cong X\times Y/\mathord {\sim }. \]
Here are some examples of smash products of pointed sets.
-
Smashing With $\text{pt}$. For any pointed set $X$, we have isomorphisms of pointed sets
\begin{align*} \text{pt}\wedge X & \cong \text{pt},\\ X\wedge \text{pt}& \cong \text{pt}. \end{align*}
-
Smashing With $S^{0}$. For any pointed set $X$, we have isomorphisms of pointed sets
\begin{align*} S^{0}\wedge X & \cong X,\\ X\wedge S^{0} & \cong X. \end{align*}
Let $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ be pointed sets.
-
Functoriality. The assignments $X,Y,\webleft (X,Y\webright )\mapsto X\wedge Y$ define functors
\begin{gather*} \begin{aligned} X\wedge - & \colon \mathsf{Sets}_{*} \to \mathsf{Sets}_{*},\\ -\wedge Y & \colon \mathsf{Sets}_{*} \to \mathsf{Sets}_{*},\\ \end{aligned}\\ -_{1}\wedge -_{2} \colon \mathsf{Sets}_{*}\times \mathsf{Sets}_{*} \to \mathsf{Sets}_{*}. \end{gather*}
In particular, given pointed maps
\begin{align*} f & \colon \webleft (X,x_{0}\webright ) \to \webleft (A,a_{0}\webright ),\\ g & \colon \webleft (Y,y_{0}\webright ) \to \webleft (B,b_{0}\webright ), \end{align*}
the induced map
\[ f\wedge g\colon X\wedge Y\to A\wedge B \]
is given by
\[ \webleft [f\wedge g\webright ]\webleft (x\wedge y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright )\wedge g\webleft (y\webright ) \]
for each $x\wedge y\in X\wedge Y$.
-
Adjointness. We have adjunctions witnessed by bijections
\begin{align*} \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X\wedge Y,Z\webright ) & \cong \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X,\textbf{Sets}_{*}\webleft (Y,Z\webright )\webright ),\\ \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X\wedge Y,Z\webright ) & \cong \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X,\textbf{Sets}_{*}\webleft (A,Z\webright )\webright ), \end{align*}
natural in $\webleft (X,x_{0}\webright ),\webleft (Y,y_{0}\webright ),\webleft (Z,z_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
-
Enriched Adjointness. We have $\mathsf{Sets}_{*}$-enriched adjunctions witnessed by isomorphisms of pointed sets
\begin{align*} \textbf{Sets}_{*}\webleft (X\wedge Y,Z\webright ) & \cong \textbf{Sets}_{*}\webleft (X,\textbf{Sets}_{*}\webleft (Y,Z\webright )\webright ),\\ \textbf{Sets}_{*}\webleft (X\wedge Y,Z\webright ) & \cong \textbf{Sets}_{*}\webleft (X,\textbf{Sets}_{*}\webleft (A,Z\webright )\webright ), \end{align*}
natural in $\webleft (X,x_{0}\webright ),\webleft (Y,y_{0}\webright ),\webleft (Z,z_{0}\webright )\in \text{Obj}\webleft (\textbf{Sets}_{*}\webright )$.
-
As a Pushout. We have an isomorphism natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, where the pushout is taken in $\mathsf{Sets}$, and the embedding $\iota \colon X\vee Y\hookrightarrow X\times Y$ is defined following Remark 4.5.1.1.5.
-
Distributivity Over Wedge Sums. We have isomorphisms of pointed sets
\begin{align*} X\wedge \webleft (Y\vee Z\webright ) & \cong \webleft (X\wedge Y\webright )\vee \webleft (X\wedge Z\webright ),\\ \webleft (X\vee Y\webright )\wedge Z & \cong \webleft (X\wedge Z\webright )\vee \webleft (Y\wedge Z\webright ), \end{align*}
natural in $\webleft (X,x_{0}\webright ),\webleft (Y,y_{0}\webright ),\webleft (Z,z_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
The map $f\wedge g$ comes from Chapter 7: Equivalence Relations and Apartness Relations, Item 4 of Proposition 7.5.2.1.3 via the map
\[ f\wedge g\colon X\times Y\to A\wedge B \]
sending $\webleft (x,y\webright )$ to $f\webleft (x\webright )\wedge g\webleft (y\webright )$, which we need to show satisfies
\[ \webleft [f\wedge g\webright ]\webleft (x,y\webright )=\webleft [f\wedge g\webright ]\webleft (x',y'\webright ) \]
for each $\webleft (x,y\webright ),\webleft (x',y'\webright )\in X\times Y$ with $\webleft (x,y\webright )\sim _{R}\webleft (x',y'\webright )$, where $\mathord {\sim }_{R}$ is the relation constructing $X\wedge Y$ as
\[ X\wedge Y\cong \webleft (X\times Y\webright )/\mathord {\sim }_{R} \]
in Construction 4.5.1.1.4. The condition defining $\mathord {\sim }$ is that at least one of the following conditions is satisfied:
-
We have $x=x'$ and $y=y'$;
-
Both of the following conditions are satisfied:
-
We have $x=x_{0}$ or $y=y_{0}$.
-
We have $x'=x_{0}$ or $y'=y_{0}$.
We have five cases:
-
In the first case, we clearly have
\[ \webleft [f\wedge g\webright ]\webleft (x,y\webright )=\webleft [f\wedge g\webright ]\webleft (x',y'\webright ) \]
since $x=x'$ and $y=y'$.
-
If $x=x_{0}$ and $x'=x_{0}$, we have
\begin{align*} \webleft [f\wedge g\webright ]\webleft (x_{0},y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x_{0}\webright )\wedge g\webleft (y\webright )\\ & = a_{0}\wedge g\webleft (y\webright )\\ & = a_{0}\wedge g\webleft (y'\webright )\\ & = f\webleft (x_{0}\webright )\wedge g\webleft (y'\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f\wedge g\webright ]\webleft (x_{0},y’\webright ).\end{align*}
-
If $x=x_{0}$ and $y'=y_{0}$, we have
\begin{align*} \webleft [f\wedge g\webright ]\webleft (x_{0},y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x_{0}\webright )\wedge g\webleft (y\webright )\\ & = a_{0}\wedge g\webleft (y\webright )\\ & = a_{0}\wedge b_{0}\\ & = f\webleft (x'\webright )\wedge b_{0}\\ & = f\webleft (x'\webright )\wedge g\webleft (y_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f\wedge g\webright ]\webleft (x’,y_{0}\webright ).\end{align*}
-
If $y=y_{0}$ and $x'=x_{0}$, we have
\begin{align*} \webleft [f\wedge g\webright ]\webleft (x,y_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright )\wedge g\webleft (y_{0}\webright )\\ & = f\webleft (x\webright )\wedge b_{0}\\ & = a_{0}\wedge b_{0}\\ & = a_{0}\wedge g\webleft (y'\webright )\\ & = f\webleft (x_{0}\webright )\wedge g\webleft (y'\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f\wedge g\webright ]\webleft (x_{0},y’\webright ).\end{align*}
-
If $y=y_{0}$ and $y'=y_{0}$, we have
\begin{align*} \webleft [f\wedge g\webright ]\webleft (x,y_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright )\wedge g\webleft (y_{0}\webright )\\ & = f\webleft (x\webright )\wedge b_{0}\\ & = f\webleft (x'\webright )\wedge b_{0}\\ & = f\webleft (x\webright )\wedge g\webleft (y_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f\wedge g\webright ]\webleft (x’,y_{0}\webright ).\end{align*}
Thus $f\wedge g$ is well-defined. Next, we claim that $\wedge $ preserves identities and composition:
- Preservation of Identities. We have
\begin{align*} \webleft [\text{id}_{X}\wedge \text{id}_{Y}\webright ]\webleft (x\wedge y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{id}_{X}\webleft (x\webright )\wedge \text{id}_{Y}\webleft (y\webright )\\ & = x\wedge y\\ & = \webleft [\text{id}_{X\wedge Y}\webright ]\webleft (x\wedge y\webright ) \end{align*}
for each $x\wedge y\in X\wedge Y$, and thus
\[ \text{id}_{X}\wedge \text{id}_{Y}=\text{id}_{X\wedge Y}. \]
- Preservation of Composition. Given pointed maps
\begin{align*} f & \colon \webleft (X,x_{0}\webright ) \to \webleft (X',x'_{0}\webright ),\\ h & \colon \webleft (X',x'_{0}\webright ) \to \webleft (X'',x''_{0}\webright ),\\ g & \colon \webleft (Y,y_{0}\webright ) \to \webleft (Y',y'_{0}\webright ),\\ k & \colon \webleft (Y’,y’_{0}\webright ) \to \webleft (Y”,y”_{0}\webright ), \end{align*}
we have
\begin{align*} \webleft [\webleft (h\circ f\webright )\wedge \webleft (k\circ g\webright )\webright ]\webleft (x\wedge y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}h\webleft (f\webleft (x\webright )\webright )\wedge k\webleft (g\webleft (y\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [h\wedge k\webright ]\webleft (f\webleft (x\webright )\wedge g\webleft (y\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [h\wedge k\webright ]\webleft (\webleft [f\wedge g\webright ]\webleft (x\wedge y\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [\webleft (h\wedge k\webright )\circ \webleft (f\wedge g\webright )\webright ]\webleft (x\wedge y\webright ) \end{align*}
for each $x\wedge y\in X\wedge Y$, and thus
\[ \webleft (h\circ f\webright )\wedge \webleft (k\circ g\webright )=\webleft (h\wedge k\webright )\circ \webleft (f\wedge g\webright ). \]
This finishes the proof.
We prove only the adjunction $-\wedge Y\dashv \textbf{Sets}_{*}\webleft (Y,-\webright )$, witnessed by a natural bijection
\[ \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X\wedge Y,Z\webright )\cong \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X,\textbf{Sets}_{*}\webleft (Y,Z\webright )\webright ), \]
as the proof of the adjunction $X\wedge -\dashv \textbf{Sets}_{*}\webleft (X,-\webright )$ is similar. We claim we have a bijection
\[ \textup{Hom}^{\otimes }_{\mathsf{Sets}_{*}}\webleft (X\times Y,Z\webright )\cong \textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X,\textbf{Sets}_{*}\webleft (Y,Z\webright )\webright ) \]
natural in $\webleft (X,x_{0}\webright ),\webleft (Y,y_{0}\webright ),\webleft (Z,z_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, impliying the desired adjunction. Indeed, this bijection is a restriction of the bijection
\[ \mathsf{Sets}\webleft (X\times Y,Z\webright )\cong \mathsf{Sets}\webleft (X,\mathsf{Sets}\webleft (Y,Z\webright )\webright ) \]
of Chapter 2: Constructions With Sets, Item 2 of Proposition 2.1.3.1.2:
- A map
\[ \xi \colon X\times Y\to Z \]
in $\textup{Hom}^{\otimes }_{\mathsf{Sets}_{*}}\webleft (X\times Y,Z\webright )$ gets sent to the pointed map
where $\xi ^{\dagger }_{x}\colon Y\to Z$ is the map defined by
\[ \xi ^{\dagger }_{x}\webleft (y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (x,y\webright ) \]
for each $y\in Y$, where:
- The map $\xi ^{\dagger }$ is indeed pointed, as we have
\begin{align*} \xi ^{\dagger }_{x_{0}}\webleft (y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (x_{0},y\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}z_{0}\end{align*}
for each $y\in Y$. Thus $\xi ^{\dagger }_{x_{0}}=\Delta _{z_{0}}$ and $\xi ^{\dagger }$ is pointed.
- The map $\xi ^{\dagger }_{x}$ indeed lies in $\textbf{Sets}_{*}\webleft (Y,Z\webright )$, as we have
\begin{align*} \xi ^{\dagger }_{x}\webleft (y_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi \webleft (x,y_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}z_{0}.\end{align*}
- Conversely, a map in $\textup{Hom}_{\mathsf{Sets}_{*}}\webleft (X,\textbf{Sets}_{*}\webleft (Y,Z\webright )\webright )$ gets sent to the map
\[ \xi ^{\dagger }\colon X\times Y\to Z \]
defined by
\[ \xi ^{\dagger }\webleft (x,y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{x}\webleft (y\webright ) \]
for each $\webleft (x,y\webright )\in X\times Y$, which indeed lies in $\textup{Hom}^{\otimes }_{\mathsf{Sets}_{*}}\webleft (X\times Y,Z\webright )$, as:
- Left Bilinearity. We have
\begin{align*} \xi ^{\dagger }\webleft (x_{0},y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{x_{0}}\webleft (y\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Delta _{z_{0}}\webleft (y\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}z_{0}\end{align*}
for each $y\in Y$, since $\xi _{x_{0}}=\Delta _{z_{0}}$ as $\xi $ is assumed to be a pointed map.
- Right Bilinearity. We have
\begin{align*} \xi ^{\dagger }\webleft (x,y_{0}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{x}\webleft (y_{0}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}z_{0}\end{align*}
for each $x\in X$, since $\xi _{x}\in \textbf{Sets}_{*}\webleft (Y,Z\webright )$ is a morphism of pointed sets.
This finishes the proof.
This follows from Item 2 and 
of .
Following the description of Chapter 2: Constructions With Sets, Remark 2.2.4.1.2, we have
\[ \text{pt}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X\vee Y}\webleft (X\times Y\webright )\cong \webleft (\text{pt}\times \webleft (X\times Y\webright )\webright )/\mathord {\sim }, \]
where $\mathord {\sim }$ identifies the elemenet $\star $ in $\text{pt}$ with all elements of the form $\webleft (x_{0},y\webright )$ and $\webleft (x,y_{0}\webright )$ in $X\times Y$. Thus Chapter 7: Equivalence Relations and Apartness Relations, Item 4 of Proposition 7.5.2.1.3 coupled with Remark 4.5.1.1.7 then gives us a well-defined map
\[ \text{pt}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X\vee Y}\webleft (X\times Y\webright )\to X\wedge Y \]
via $\webleft [\webleft (\star ,\webleft (x,y\webright )\webright )\webright ]\mapsto x\wedge y$, with inverse
\[ X\wedge Y\to \text{pt}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X\vee Y}\webleft (X\times Y\webright ) \]
given by $x\wedge y\mapsto \webleft [\webleft (\star ,\webleft (x,y\webright )\webright )\webright ]$.
Item 5: Distributivity Over Wedge Sums
This follows from Proposition 4.5.9.1.1, of , and the fact that $\vee $ is the coproduct in $\mathsf{Sets}_{*}$ (Chapter 3: Pointed Sets, Definition 3.3.3.1.1).