Construction 4.5.1.1.4 (00FY): Smash Products of 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`

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:
1. We have $x=x_{0}$ or $y=y_{0}$.
2. 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.