7.5.1 Foundations

    Let $(X,x_{0})$ and $(Y,y_{0})$ be pointed sets.

    The smash product of $(X,x_{0})$ and $(Y,y_{0})$1 is the pointed set $X\wedge Y$2 satisfying the bijection

    \[ \mathsf{Sets}_{*}(X\wedge Y,Z) \cong \operatorname {\mathrm{Hom}}^{\otimes }_{\mathsf{Sets}_{*}}(X\times Y,Z), \]

    naturally in $(X,x_{0}),(Y,y_{0}),(Z,z_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$.


    1. 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 $(X,x_{0})$ and $(Y,y_{0})$ or the tensor product of $(X,x_{0})$ and $(Y,y_{0})$ over $\mathbb {F}_{1}$.
    2. 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(x_{0},y) & = z_{0},\\ f(x,y_{0}) & = 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 $(X,x_{0})$ and $(Y,y_{0})$ is the pair $((X\wedge Y,x_{0}\wedge y_{0}),\iota )$ consisting of

      • A pointed set $(X\wedge Y,x_{0}\wedge y_{0})$;

      • A bilinear morphism of pointed sets $\iota \colon (X\times Y,(x_{0},y_{0}))\to X\wedge Y$;

      satisfying the following universal property:

      • (★)
      • Given another such pair $((Z,z_{0}),f)$ consisting of
        • A pointed set $(Z,z_{0})$;

        • A bilinear morphism of pointed sets $f\colon (X\times Y,(x_{0},y_{0}))\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 $(X,x_{0})$ and $(Y,y_{0})$ is the pointed set $(X\wedge Y,x_{0}\wedge y_{0})$ consisting of:

    • The Underlying Set. The set $X\wedge Y$ defined by

      \[ X\wedge Y\cong (X\times Y)/\mathord {\sim }_{R}, \]

      where $\mathord {\sim }_{R}$ is the equivalence relation on $X\times Y$ obtained by declaring

      \begin{align*} (x_{0},y) & \sim _{R} (x_{0},y'),\\ (x,y_{0}) & \sim _{R} (x’,y_{0}) \end{align*}

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

    • The Basepoint. The element $[(x_{0},y_{0})]$ of $X\wedge Y$ given by the equivalence class of $(x_{0},y_{0})$ under the equivalence relation $\mathord {\sim }$ on $X\times Y$.

    By Chapter 10: Conditions on Relations, Unresolved reference, we have a natural bijection

    \[ \mathsf{Sets}_{*}(X\wedge Y,Z) \cong \operatorname {\mathrm{Hom}}^{R}_{\mathsf{Sets}}(X\times Y,Z), \]

    where $\operatorname {\mathrm{Hom}}^{R}_{\mathsf{Sets}}(X\times Y,Z)$ is the set

    \[ \operatorname {\mathrm{Hom}}^{R}_{\mathsf{Sets}}(X\times Y,Z)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ f\in \operatorname {\mathrm{Hom}}_{\mathsf{Sets}}(X\times Y,Z)\ \middle |\ \begin{aligned} & \text{for each $x,y\in X$, if}\\ & \text{$(x,y)\sim _{R}(x',y')$, then}\\ & \text{$f(x,y)=f(x',y')$}\end{aligned} \right\} . \]
    However, the condition $(x,y)\sim _{R}(x',y')$ only holds when:

    1. 1.

      We have $x=x'$ and $y=y'$.

    2. 2.

      The following conditions are satisfied:

      1. (a)

        We have $x=x_{0}$ or $y=y_{0}$.

  • (b)

    We have $x'=x_{0}$ or $y'=y_{0}$.

  • So, given $f\in \operatorname {\mathrm{Hom}}_{\mathsf{Sets}}(X\times Y,Z)$ with a corresponding $\overline{f}\colon X\wedge Y\to Z$, the latter case above implies

    \begin{align*} f(x_{0},y) & = f(x,y_{0})\\ & = f(x_{0},y_{0}), \end{align*}

    and since $\overline{f}\colon X\wedge Y\to Z$ is a pointed map, we have

    \begin{align*} f(x_{0},y_{0}) & = \overline{f}(x_{0},y_{0})\\ & = z_{0}. \end{align*}

    Thus the elements $f$ in $\operatorname {\mathrm{Hom}}^{R}_{\mathsf{Sets}}(X\times Y,Z)$ are precisely those functions $f\colon X\times Y\to Z$ satisfying the equalities

    \begin{align*} f(x_{0},y) & = z_{0},\\ f(x,y_{0}) & = z_{0} \end{align*}

    for each $x\in X$ and each $y\in Y$, giving an equality

    \[ \operatorname {\mathrm{Hom}}^{R}_{\mathsf{Sets}}(X\times Y,Z)=\operatorname {\mathrm{Hom}}^{\otimes }_{\mathsf{Sets}_{*}}(X\times Y,Z) \]

    of sets, which when composed with our earlier isomorphism

    \[ \mathsf{Sets}_{*}(X\wedge Y,Z) \cong \operatorname {\mathrm{Hom}}^{R}_{\mathsf{Sets}}(X\times Y,Z), \]

    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 $(\left\{ x_{0}\right\} \times Y)\cup (X\times \left\{ y_{0}\right\} )$ of $X\times Y$, and having the quotient be defined by declaring $(x,y)\sim (x',y')$ iff we have $(x,y),(x',y')\in X\vee Y$.

    Alternatively, the smash product of $(X,x_{0})$ and $(Y,y_{0})$ may be constructed as the pointed set $X\wedge Y$ given by

    \begin{align*} X\wedge Y & \cong \bigvee _{x\in X^{-}}Y\\ & \cong \bigvee _{y\in Y^{-}}X.\end{align*}

    Indeed, since $X\cong \bigvee _{x\in X^{-}}S^{0}$, we have

    \begin{align*} X\wedge Y & \cong (\bigvee _{x\in X^{-}}S^{0})\wedge Y\\ & \cong \bigvee _{x\in X^{-}}S^{0}\wedge Y\\ & \cong \bigvee _{x\in X^{-}}Y, \end{align*}

    where we have used that $\wedge $ preserves colimits in both variables via Unresolved reference for the second isomorphism above, since it has right adjoints in both variables by Item 2.

    A similar proof applies to the isomorphism $X\wedge Y\cong \bigvee _{y\in Y^{-}}X$.

    We write $x\wedge y$ for the element $[(x,y)]$ of $X\wedge Y\cong X\times Y/\mathord {\sim }$.

    Employing the notation introduced in Notation 7.5.1.1.7, 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. 1.

      Smashing With $\mathrm{pt}$. For any pointed set $X$, we have isomorphisms of pointed sets

      \begin{align*} \mathrm{pt}\wedge X & \cong \mathrm{pt},\\ X\wedge \mathrm{pt}& \cong \mathrm{pt}. \end{align*}
    2. 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 $(X,x_{0})$ and $(Y,y_{0})$ be pointed sets.

    1. 1.

      Functoriality. The assignments $X,Y,(X,Y)\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 (X,x_{0}) \to (A,a_{0}),\\ g & \colon (Y,y_{0}) \to (B,b_{0}), \end{align*}

      the induced map

      \[ f\wedge g\colon X\wedge Y\to A\wedge B \]

      is given by

      \[ [f\wedge g](x\wedge y)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f(x)\wedge g(y) \]

      for each $x\wedge y\in X\wedge Y$.

    2. 2.

      Adjointness. We have adjunctions

      witnessed by bijections

      \begin{align*} \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X\wedge Y,Z) & \cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X,\boldsymbol {\mathsf{Sets}}_{*}(Y,Z)),\\ \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X\wedge Y,Z) & \cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X,\boldsymbol {\mathsf{Sets}}_{*}(A,Z)), \end{align*}

      natural in $(X,x_{0}),(Y,y_{0}),(Z,z_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$.

    3. 3.

      Enriched Adjointness. We have $\mathsf{Sets}_{*}$-enriched adjunctions

      witnessed by isomorphisms of pointed sets

      \begin{align*} \boldsymbol {\mathsf{Sets}}_{*}(X\wedge Y,Z) & \cong \boldsymbol {\mathsf{Sets}}_{*}(X,\boldsymbol {\mathsf{Sets}}_{*}(Y,Z)),\\ \boldsymbol {\mathsf{Sets}}_{*}(X\wedge Y,Z) & \cong \boldsymbol {\mathsf{Sets}}_{*}(X,\boldsymbol {\mathsf{Sets}}_{*}(A,Z)), \end{align*}

      natural in $(X,x_{0}),(Y,y_{0}),(Z,z_{0})\in \operatorname {\mathrm{Obj}}(\boldsymbol {\mathsf{Sets}}_{*})$.

    4. 4.

      As a Pushout. We have an isomorphism

      natural in $X,Y\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$, where the pushout is taken in $\mathsf{Sets}$, and the embedding $\iota \colon X\vee Y\hookrightarrow X\times Y$ is defined following Remark 7.5.1.1.5.

    5. 5.

      Distributivity Over Wedge Sums. We have isomorphisms of pointed sets

      \begin{align*} X\wedge (Y\vee Z) & \cong (X\wedge Y)\vee (X\wedge Z),\\ (X\vee Y)\wedge Z & \cong (X\wedge Z)\vee (Y\wedge Z), \end{align*}

      natural in $(X,x_{0}),(Y,y_{0}),(Z,z_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$.

    Item 1: Functoriality
    The map $f\wedge g$ comes from Chapter 10: Conditions on Relations, Item 4 of Proposition 10.6.2.1.3 via the map

    \[ f\wedge g\colon X\times Y\to A\wedge B \]

    sending $(x,y)$ to $f(x)\wedge g(y)$, which we need to show satisfies

    \[ [f\wedge g](x,y)=[f\wedge g](x',y') \]

    for each $(x,y),(x',y')\in X\times Y$ with $(x,y)\sim _{R}(x',y')$, where $\mathord {\sim }_{R}$ is the relation constructing $X\wedge Y$ as

    \[ X\wedge Y\cong (X\times Y)/\mathord {\sim }_{R} \]

    in Construction 7.5.1.1.4. The condition defining $\mathord {\sim }$ is that at least one of the following conditions is satisfied:

    1. 1.

      We have $x=x'$ and $y=y'$;

    2. 2.

      Both of the following conditions are satisfied:

      1. (a)

        We have $x=x_{0}$ or $y=y_{0}$.

      2. (b)

        We have $x'=x_{0}$ or $y'=y_{0}$.

    We have five cases:

    1. 1.

      In the first case, we clearly have

      \[ [f\wedge g](x,y)=[f\wedge g](x',y') \]

      since $x=x'$ and $y=y'$.

    2. 2.

      If $x=x_{0}$ and $x'=x_{0}$, we have

      \begin{align*} [f\wedge g](x_{0},y) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f(x_{0})\wedge g(y)\\ & = a_{0}\wedge g(y)\\ & = a_{0}\wedge g(y')\\ & = f(x_{0})\wedge g(y')\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[f\wedge g](x_{0},y’).\end{align*}
    3. 3.

      If $x=x_{0}$ and $y'=y_{0}$, we have

      \begin{align*} [f\wedge g](x_{0},y) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f(x_{0})\wedge g(y)\\ & = a_{0}\wedge g(y)\\ & = a_{0}\wedge b_{0}\\ & = f(x')\wedge b_{0}\\ & = f(x')\wedge g(y_{0})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[f\wedge g](x’,y_{0}).\end{align*}
    4. 4.

      If $y=y_{0}$ and $x'=x_{0}$, we have

      \begin{align*} [f\wedge g](x,y_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f(x)\wedge g(y_{0})\\ & = f(x)\wedge b_{0}\\ & = a_{0}\wedge b_{0}\\ & = a_{0}\wedge g(y')\\ & = f(x_{0})\wedge g(y')\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[f\wedge g](x_{0},y’).\end{align*}
    5. 5.

      If $y=y_{0}$ and $y'=y_{0}$, we have

      \begin{align*} [f\wedge g](x,y_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f(x)\wedge g(y_{0})\\ & = f(x)\wedge b_{0}\\ & = f(x')\wedge b_{0}\\ & = f(x)\wedge g(y_{0})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[f\wedge g](x’,y_{0}).\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*} [\operatorname {\mathrm{id}}_{X}\wedge \operatorname {\mathrm{id}}_{Y}](x\wedge y) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{id}}_{X}(x)\wedge \operatorname {\mathrm{id}}_{Y}(y)\\ & = x\wedge y\\ & = [\operatorname {\mathrm{id}}_{X\wedge Y}](x\wedge y) \end{align*}

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

      \[ \operatorname {\mathrm{id}}_{X}\wedge \operatorname {\mathrm{id}}_{Y}=\operatorname {\mathrm{id}}_{X\wedge Y}. \]
    • Preservation of Composition. Given pointed maps

      \begin{align*} f & \colon (X,x_{0}) \to (X',x'_{0}),\\ h & \colon (X',x'_{0}) \to (X'',x''_{0}),\\ g & \colon (Y,y_{0}) \to (Y',y'_{0}),\\ k & \colon (Y’,y’_{0}) \to (Y^{\prime \prime },y^{\prime \prime }_{0}), \end{align*}

      we have

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

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

      \[ (h\circ f)\wedge (k\circ g)=(h\wedge k)\circ (f\wedge g). \]

    This finishes the proof.

    Item 2: Adjointness
    We prove only the adjunction $-\wedge Y\dashv \boldsymbol {\mathsf{Sets}}_{*}(Y,-)$, witnessed by a natural bijection

    \[ \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X\wedge Y,Z)\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X,\boldsymbol {\mathsf{Sets}}_{*}(Y,Z)), \]

    as the proof of the adjunction $X\wedge -\dashv \boldsymbol {\mathsf{Sets}}_{*}(X,-)$ is similar. We claim we have a bijection

    \[ \operatorname {\mathrm{Hom}}^{\otimes }_{\mathsf{Sets}_{*}}(X\times Y,Z)\cong \operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X,\boldsymbol {\mathsf{Sets}}_{*}(Y,Z)) \]

    natural in $(X,x_{0}),(Y,y_{0}),(Z,z_{0})\in \operatorname {\mathrm{Obj}}(\mathsf{Sets}_{*})$, impliying the desired adjunction. Indeed, this bijection is a restriction of the bijection

    \[ \mathsf{Sets}(X\times Y,Z)\cong \mathsf{Sets}(X,\mathsf{Sets}(Y,Z)) \]

    of Chapter 4: Constructions With Sets, Item 2 of Proposition 4.1.3.1.3:

    • A map

      \[ \xi \colon X\times Y\to Z \]

      in $\operatorname {\mathrm{Hom}}^{\otimes }_{\mathsf{Sets}_{*}}(X\times Y,Z)$ gets sent to the pointed map

      where $\xi ^{\dagger }_{x}\colon Y\to Z$ is the map defined by

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

      for each $y\in Y$, where:

      • The map $\xi ^{\dagger }$ is indeed pointed, as we have

        \begin{align*} \xi ^{\dagger }_{x_{0}}(y) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (x_{0},y)\\ & \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 $\boldsymbol {\mathsf{Sets}}_{*}(Y,Z)$, as we have

        \begin{align*} \xi ^{\dagger }_{x}(y_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi (x,y_{0})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}z_{0}.\end{align*}
    • Conversely, a map

      in $\operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}(X,\boldsymbol {\mathsf{Sets}}_{*}(Y,Z))$ gets sent to the map

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

      defined by

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

      for each $(x,y)\in X\times Y$, which indeed lies in $\operatorname {\mathrm{Hom}}^{\otimes }_{\mathsf{Sets}_{*}}(X\times Y,Z)$, as:

      • Left Bilinearity. We have

        \begin{align*} \xi ^{\dagger }(x_{0},y) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{x_{0}}(y)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Delta _{z_{0}}(y)\\ & \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 }(x,y_{0}) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\xi _{x}(y_{0})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}z_{0}\end{align*}

        for each $x\in X$, since $\xi _{x}\in \boldsymbol {\mathsf{Sets}}_{*}(Y,Z)$ is a morphism of pointed sets.

    This finishes the proof.

    Item 3: Enriched Adjointness
    This follows from Item 2 and Unresolved reference, Unresolved reference of Unresolved reference.

    Item 4: As a Pushout
    Following the description of Chapter 4: Constructions With Sets, Remark 4.2.4.1.3, we have

    \[ \mathrm{pt}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X\vee Y}(X\times Y)\cong (\mathrm{pt}\times (X\times Y))/\mathord {\sim }, \]

    where $\mathord {\sim }$ identifies the elemenet $\star $ in $\mathrm{pt}$ with all elements of the form $(x_{0},y)$ and $(x,y_{0})$ in $X\times Y$. Thus Chapter 10: Conditions on Relations, Item 4 of Proposition 10.6.2.1.3 coupled with Remark 7.5.1.1.8 then gives us a well-defined map

    \[ \mathrm{pt}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X\vee Y}(X\times Y)\to X\wedge Y \]

    via $[(\star ,(x,y))]\mapsto x\wedge y$, with inverse

    \[ X\wedge Y\to \mathrm{pt}\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}_{X\vee Y}(X\times Y) \]

    given by $x\wedge y\mapsto [(\star ,(x,y))]$.

    Item 5: Distributivity Over Wedge Sums
    This follows from Proposition 7.5.9.1.1, Unresolved reference, Unresolved reference of Unresolved reference, and the fact that $\vee $ is the coproduct in $\mathsf{Sets}_{*}$ (Chapter 6: Pointed Sets, Definition 6.3.3.1.1).


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


You can also use the contact form below: