The Clowder Project

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

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

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

   2. (b)

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

So, given $f\in \operatorname {\mathrm{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

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

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

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

of sets, which when composed with our earlier isomorphism

gives our desired natural bijection, finishing the proof.

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

where we have used that $\wedge $ preserves colimits in both variables by 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$.

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

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

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

   \[ \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. 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. 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. 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. 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 [\operatorname {\mathrm{id}}_{X}\wedge \operatorname {\mathrm{id}}_{Y}\webright ]\webleft (x\wedge y\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{id}}_{X}\webleft (x\webright )\wedge \operatorname {\mathrm{id}}_{Y}\webleft (y\webright )\\ & = x\wedge y\\ & = \webleft [\operatorname {\mathrm{id}}_{X\wedge Y}\webright ]\webleft (x\wedge y\webright ) \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 \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^{\prime \prime },y^{\prime \prime }_{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.

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

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

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}_{*}}\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 $\boldsymbol {\mathsf{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 $\operatorname {\mathrm{Hom}}_{\mathsf{Sets}_{*}}\webleft (X,\boldsymbol {\mathsf{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 $\operatorname {\mathrm{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 \boldsymbol {\mathsf{Sets}}_{*}\webleft (Y,Z\webright )$ is a morphism of pointed sets.

This finishes the proof.

where $\mathord {\sim }$ identifies the elemenet $\star $ in $\mathrm{pt}$ with all elements of the form $\webleft (x_{0},y\webright )$ and $\webleft (x,y_{0}\webright )$ 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

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

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