Subsection 5.3.5 (00E4): The Left Skew Left 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 left unitor of the left tensor product of pointed sets is the natural transformation

whose component

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

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

\begin{align*} S^{0}\lhd X & \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*}

for each $x\in X$.

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

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

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

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

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

given by

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

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

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

so that

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

and

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

but

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

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

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

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

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

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

is indeed a morphism of pointed sets, as we have

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

Next, we claim that $\lambda ^{\mathsf{Sets}_{*},\lhd }$ 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 $\lambda ^{\mathsf{Sets}_{*},\lhd }$ to be a natural transformation. This finishes the proof.

The Clowder Project

5.3.5 The Left Skew Left Unitor