Subsection 3.1.8 (01NZ): The Diagonal

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 diagonal of the product of sets is the natural transformation

whose component

\[ \Delta _{X}\colon X\to X\times X \]

at $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ is given by

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

for each $x\in X$.

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, showing $\Delta $ to be natural.

Let $X$ be a set.

Monoidality. The diagonal map
\[ \Delta \colon \text{id}_{\mathsf{Sets}}\Longrightarrow \mathord {\times }\circ {\Delta ^{\mathsf{Cats}_{\mathsf{2}}}_{\mathsf{Sets}}}, \]

is a monoidal natural transformation:
1. Compatibility With Strong Monoidality Constraints. For each $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the diagram
  
  commutes.
2. Compatibility With Strong Unitality Constraints. The diagrams
  commute, i.e. we have
  \begin{align*} \Delta _{\text{pt}} & = \lambda ^{\mathsf{Sets},-1}_{\text{pt}}\\ & = \rho ^{\mathsf{Sets},-1}_{\text{pt}}, \end{align*}
  
  where we recall that the equalities
  
  \begin{align*} \lambda ^{\mathsf{Sets}}_{\text{pt}} & = \rho ^{\mathsf{Sets}}_{\text{pt}},\\ \lambda ^{\mathsf{Sets},-1}_{\text{pt}} & = \rho ^{\mathsf{Sets},-1}_{\text{pt}}\end{align*}
  
  are always true in any monoidal category by , of .
The Diagonal of the Unit. The component
\[ \Delta _{\text{pt}} \colon \text{pt}\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\text{pt}\times \text{pt} \]

of $\Delta $ at $\text{pt}$ is an isomorphism.

Item 1: Monoidality

We claim that $\Delta $ is indeed monoidal:

Item (a): Compatibility With Strong Monoidality Constraints: We need to show that the diagram

commutes. Indeed, this diagram acts on elements as
and hence indeed commutes.
Item (b): Compatibility With Strong Unitality Constraints: As shown in the proof of Definition 3.1.5.1.1, the inverse of the left unitor of $\mathsf{Sets}$ with respect to to the product at $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ is given by
\[ \lambda ^{\mathsf{Sets},-1}_{X}\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\star ,x\webright ) \]

for each $x\in X$, so when $X=\text{pt}$, we have

\[ \lambda ^{\mathsf{Sets},-1}_{\text{pt}}\webleft (\star \webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}{\webleft (\star ,\star \webright ),} \]

and also

\[ \Delta ^{\mathsf{Sets}}_{\text{pt}}\webleft (\star \webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}{\webleft (\star ,\star \webright ),} \]

so we have $\Delta _{\text{pt}}=\lambda ^{\mathsf{Sets},-1}_{\text{pt}}$.

This finishes the proof.

Item 2: The Diagonal of the Unit

This follows from Item 1 and the invertibility of the left/right unitor of $\mathsf{Sets}$ with respect to $\times $, proved in the proof of Definition 3.1.5.1.1 for the left unitor or the proof of Definition 3.1.6.1.1 for the right unitor.

The Clowder Project

3.1.8 The Diagonal