5.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 )$1 is the pointed set $X\wedge Y$2 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 )$.


1Further Terminology: In the context of monoids with zero as models for $\mathbb {F}_{1}$-algebras, the smash product $X\wedge Y$ is also called the tensor product of $\mathbb {F}_{1}$-modules of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ or the tensor product of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ over $\mathbb {F}_{1}$.
2Further Notation: In the context of monoids with zero as models for $\mathbb {F}_{1}$-algebras, the smash product $X\wedge Y$ is also denoted $X\otimes _{\mathbb {F}_{1}}Y$.

That is to say, the smash product of pointed sets is defined so as to induce a bijection between the following data:

  • Pointed maps $f\colon X\wedge Y\to Z$.
  • Maps of sets $f\colon X\times Y\to Z$ satisfying

    \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$.

The smash product of pointed sets may be described as follows:

  • The smash product of $\webleft (X,x_{0}\webright )$ and $\webleft (Y,y_{0}\webright )$ is the pair $\webleft (\webleft (X\wedge Y,x_{0}\wedge y_{0}\webright ),\iota \webright )$ consisting of
    • A pointed set $\webleft (X\wedge Y,x_{0}\wedge y_{0}\webright )$;
    • A bilinear morphism of pointed sets $\iota \colon \webleft (X\times Y,\webleft (x_{0},y_{0}\webright )\webright )\to X\wedge Y$;
    satisfying the following universal property:

    • Given another such pair $\webleft (\webleft (Z,z_{0}\webright ),f\webright )$ consisting of
      • A pointed set $\webleft (Z,z_{0}\webright )$;
      • A bilinear morphism of pointed sets $f\colon \webleft (X\times Y,\webleft (x_{0},y_{0}\webright )\webright )\to X\wedge Y$;
      there exists a unique morphism of pointed sets $X\wedge Y\overset {\exists !}{\to }Z$ making the diagram

      commute.

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 , of , 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:

  1. We have $x=x'$ and $y=y'$.
  2. 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.

It is also somewhat common to write

\[ X\wedge Y\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\frac{X\times Y}{X\vee Y}, \]

identifying $X\vee Y$ with the subspace $\webleft (\webleft\{ x_{0}\webright\} \times Y\webright )\cup \webleft (X\times \webleft\{ y_{0}\webright\} \webright )$ of $X\times Y$, and having the quotient be defined by declaring $\webleft (x,y\webright )\sim \webleft (x',y'\webright )$ iff we have $\webleft (x,y\webright ),\webleft (x',y'\webright )\in X\vee Y$.

We write $x\wedge y$ for the element $\webleft [\webleft (x,y\webright )\webright ]$ of

\[ X\wedge Y\cong X\times Y/\mathord {\sim }. \]

Employing the notation introduced in Notation 5.5.1.1.6, we have

\begin{align*} x_{0}\wedge y_{0} & = x\wedge y_{0},\\ & = x_{0}\wedge y\end{align*}

for each $x\in X$ and each $y\in Y$, and

\begin{align*} x\wedge y_{0} & = x'\wedge y_{0},\\ x_{0}\wedge y & = x_{0}\wedge y’\end{align*}

for each $x,x'\in X$ and each $y,y'\in Y$.

Here are some examples of smash products of pointed sets.

  1. 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*}
  2. 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.

  1. Functoriality. The assignments $X,Y,\webleft (X,Y\webright )\mapsto X\wedge Y$ define functors
    \[ \begin{array}{ccc} X\wedge -\colon \mkern -15mu & \mathsf{Sets}_{*} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets}_{*},\\ -\wedge Y\colon \mkern -15mu & \mathsf{Sets}_{*} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets}_{*},\\ -_{1}\wedge -_{2}\colon \mkern -15mu & \mathsf{Sets}_{*}\times \mathsf{Sets}_{*} \mkern -17.5mu& {}\mathbin {\to }\mathsf{Sets}_{*}. \end{array} \]

    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$.

  2. 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 )$.

  3. 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 )$.

  4. 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 5.5.1.1.5.
  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 )$.

Item 1: Functoriality
The map $f\wedge g$ comes from , of 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 5.5.1.1.4. The condition defining $\mathord {\sim }$ is that at least one of the following conditions is satisfied:

  1. We have $x=x'$ and $y=y'$;
  2. Both of 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}$.

We have five cases:

  1. 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'$.

  2. 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*}
  3. 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*}
  4. 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*}
  5. 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.
Item 2: Adjointness
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.3:

  • 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.
Item 3: Enriched Adjointness
This follows from Item 2 and , of .
Item 4: As a Pushout
Following the description of Chapter 2: Constructions With Sets, Remark 2.2.4.1.3, 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 , of coupled with Remark 5.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 5.5.9.1.1, , of , and the fact that $\vee $ is the coproduct in $\mathsf{Sets}_{*}$ (Chapter 4: Pointed Sets, Definition 4.3.3.1.1).


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


You can also use the contact form below: