Definition 5.1.6.1.1 (01NW): The Right Unitor of $\times $

The right unitor of the product of sets is the natural isomorphism

whose component

\[ \rho ^{\mathsf{Sets}}_{X} \colon X\times \mathrm{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X \]

at $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$ is given by

\[ \rho ^{\mathsf{Sets}}_{X}(x,\star )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x \]

for each $(x,\star )\in X\times \mathrm{pt}$.

Invertibility

The inverse of $\rho ^{\mathsf{Sets}}_{X}$ is the morphism

\[ \rho ^{\mathsf{Sets},-1}_{X}\colon X\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X\times \mathrm{pt} \]

defined by

\[ \rho ^{\mathsf{Sets},-1}_{X}(x)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(x,\star ) \]

for each $x\in X$. Indeed:

•
Invertibility I. We have

\begin{align*} [\rho ^{\mathsf{Sets},-1}_{X}\circ \rho ^{\mathsf{Sets}}_{X}](x,\star ) & = \rho ^{\mathsf{Sets},-1}_{X}(\rho ^{\mathsf{Sets}}_{X}(x,\star ))\\ & = \rho ^{\mathsf{Sets},-1}_{X}(x)\\ & = (x,\star )\\ & = [\operatorname {\mathrm{id}}_{X\times \mathrm{pt}}](x,\star ) \end{align*}

for each $(x,\star )\in X\times \mathrm{pt}$, and therefore we have

\[ \rho ^{\mathsf{Sets},-1}_{X}\circ \rho ^{\mathsf{Sets}}_{X}=\operatorname {\mathrm{id}}_{X\times \mathrm{pt}}. \]
•
Invertibility II. We have

\begin{align*} [\rho ^{\mathsf{Sets}}_{X}\circ \rho ^{\mathsf{Sets},-1}_{X}](x) & = \rho ^{\mathsf{Sets}}_{X}(\rho ^{\mathsf{Sets},-1}_{X}(x))\\ & = \rho ^{\mathsf{Sets},-1}_{X}(x,\star )\\ & = x\\ & = [\operatorname {\mathrm{id}}_{X}](x) \end{align*}

for each $x\in X$, and therefore we have

\[ \rho ^{\mathsf{Sets}}_{X}\circ \rho ^{\mathsf{Sets},-1}_{X}=\operatorname {\mathrm{id}}_{X}. \]

Therefore $\rho ^{\mathsf{Sets}}_{X}$ is indeed an isomorphism.

Naturality

We need to show that, given a function $f\colon X\to Y$, the diagram

commutes. Indeed, this diagram acts on elements as

and hence indeed commutes. Therefore $\rho ^{\mathsf{Sets}}$ is a natural transformation.

Being a Natural Isomorphism

Since $\rho ^{\mathsf{Sets}}$ is natural and $\rho ^{\mathsf{Sets},-1}$ is a componentwise inverse to $\rho ^{\mathsf{Sets}}$, it follows from Chapter 11: Categories, Item 2 of Proposition 11.9.7.1.2 that $\rho ^{\mathsf{Sets},-1}$ is also natural. Thus $\rho ^{\mathsf{Sets}}$ is a natural isomorphism.

The Clowder Project

5.1.6 The Right Unitor