The Clowder Project

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 4.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 ). \]

as the proof of the adjunction $X\wedge -\dashv \textbf{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 \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, impliying the desired adjunction. Indeed, this bijection is a restriction of the bijection

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.

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

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