Subsection 4.4.6 (00FH): The Right Skew Right Unitor

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`

The skew right unitor of the right tensor product of pointed sets is the natural transformation

whose component

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X} \colon X\rhd S^{0}\to X \]

at $\webleft (X,x_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$ is given by the composition

\begin{align*} X\rhd S^{0} & \cong |X|\odot S^{0}\\ & \cong \bigvee _{x\in X}S^{0}\\ & \rightarrow X, \end{align*}

where $\bigvee _{x\in X}S^{0}\to X$ is the map given by

\begin{align*} \webleft [\webleft (x,0\webright )\webright ] & \mapsto x_{0},\\ \webleft [\webleft (x,1\webright )\webright ] & \mapsto x. \end{align*}

In other words, $\smash {\rho ^{\mathsf{Sets}_{*},\rhd }_{X}}$ acts on elements as

\begin{align*} \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (x\rhd 0\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x_{0},\\ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (x\rhd 1\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x\end{align*}

for each $x\rhd 1\in X\rhd S^{0}$.

The morphism $\smash {\rho ^{\mathsf{Sets}_{*},\rhd }_{X}}$ is almost invertible, with its would-be-inverse

\[ \phi _{X}\colon X\to X\rhd S^{0} \]

given by

\[ \phi _{X}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x\rhd 1 \]

for each $x\in X$. Indeed, we have

\begin{align*} \webleft [\rho ^{\mathsf{Sets}_{*},\rhd }_{X}\circ \phi \webright ]\webleft (x\webright ) & = \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (\phi \webleft (x\webright )\webright )\\ & = \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (x\rhd 1\webright )\\ & = x\\ & = \webleft [\text{id}_{X}\webright ]\webleft (x\webright ) \end{align*}

so that

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\circ \phi =\text{id}_{X} \]

and

\begin{align*} \webleft [\phi \circ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webright ]\webleft (x\rhd 1\webright ) & = \phi \webleft (\rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (x\rhd 1\webright )\webright )\\ & = \phi \webleft (x\webright )\\ & = x\rhd 1\\ & = \webleft [\text{id}_{X\rhd S^{0}}\webright ]\webleft (x\rhd 1\webright ), \end{align*}

but

\begin{align*} \webleft [\phi \circ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webright ]\webleft (x\rhd 0\webright ) & = \phi \webleft (\rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (x\rhd 0\webright )\webright )\\ & = \phi \webleft (x_{0}\webright )\\ & = 1\rhd x_{0}, \end{align*}

where $x\rhd 0\neq 1\rhd x_{0}$. Thus

\[ \phi \circ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{?}}}=}}\text{id}_{X\rhd S^{0}} \]

holds for all elements in $X\rhd S^{0}$ except one.

Firstly, note that, given $\webleft (X,x_{0}\webright )\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, the map

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X} \colon X\rhd S^{0}\to X \]

is indeed a morphism of pointed sets as we have

\[ \rho ^{\mathsf{Sets}_{*},\rhd }_{X}\webleft (x_{0}\rhd 0\webright )=x_{0}. \]

Next, we claim that $\rho ^{\mathsf{Sets}_{*},\rhd }$ is a natural transformation. We need to show that, given a morphism of pointed sets

\[ f\colon \webleft (X,x_{0}\webright )\to \webleft (Y,y_{0}\webright ), \]

the diagram

commutes. Indeed, this diagram acts on elements as

and

and hence indeed commutes, showing $\rho ^{\mathsf{Sets}_{*},\rhd }$ to be a natural transformation. This finishes the proof.

The Clowder Project

4.4.6 The Right Skew Right Unitor