Theorem 5.5.10.1.1 (01VZ): The Universal Property of $\webleft (\mathsf{Sets}_{*},\wedge ,S^{0}\webright )$

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`

Unwinding the Statement

Let $\webleft (\mathsf{Sets}_{*},\otimes _{\mathsf{Sets}_{*}},\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}},\mathbb {1}_{\mathsf{Sets}_{*}},\lambda ',\rho ',\sigma '\webright )$ be a closed symmetric monoidal category satisfying Item 1 and Item 2. We need to show that the identity functor

\[ \text{id}_{\mathsf{Sets}_{*}}\colon \mathsf{Sets}_{*}\to \mathsf{Sets}_{*} \]

admits a unique closed symmetric monoidal functor structure

\[ \begin{array}{cccc} \phantom{\text{id}^{\otimes }_{\mathsf{Sets}_{*}}}\mathllap {\text{id}^{\otimes }_{\mathsf{Sets}_{*}}} \colon \mkern -10mu & X\otimes _{\mathsf{Sets}_{*}}Y \mkern -10mu& {}\mathbin {\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}& \mkern -10mu{}X\wedge Y,\\ \phantom{\text{id}^{\otimes }_{\mathsf{Sets}_{*}}}\mathllap {\text{id}^{\textup{Hom}}_{\mathsf{Sets}_{*}}} \colon \mkern -10mu & \webleft [X,Y\webright ]_{\mathsf{Sets}_{*}} \mkern -10mu& {}\mathbin {\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}& \mkern -10mu{}\mathsf{Sets}_{*}\webleft (X,Y\webright ),\\ \phantom{\text{id}^{\otimes }_{\mathsf{Sets}_{*}}}\mathllap {\text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}_{*}}} \colon \mkern -10mu & \mathbb {1}_{\mathsf{Sets}_{*}} \mkern -10mu& {}\mathbin {\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}& \mkern -10mu{}S^{0}, \end{array} \]

making it into a symmetric monoidal strongly closed isomorphism of categories from $\webleft(\phantom{\mathrlap {\lambda '}}\mathsf{Sets}_{*}\right.$, $\otimes _{\mathsf{Sets}_{*}}$, $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}$, $\mathbb {1}_{\mathsf{Sets}_{*}}$, $\lambda '$, $\rho '$, $\left.\sigma '\webright)$ to the closed symmetric monoidal category $\webleft(\phantom{\mathrlap {\lambda ^{\mathsf{Sets}_{*}}}}\mathsf{Sets}_{*}\right.$, $\times $, $\mathsf{Sets}_{*}\webleft (-_{1},-_{2}\webright )$, $\mathbb {1}_{\mathsf{Sets}_{*}}$, $\lambda ^{\mathsf{Sets}_{*}}$, $\rho ^{\mathsf{Sets}_{*}}$, $\left.\sigma ^{\mathsf{Sets}_{*}}\webright)$ of Proposition 5.5.9.1.1.

Constructing an Isomorphism $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}\cong \mathsf{Sets}_{*}\webleft (-_{1},-_{2}\webright )$

, we have a natural isomorphism

\[ \mathsf{Sets}_{*}\webleft (S^{0},\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}\webright )\cong \mathsf{Sets}_{*}\webleft (-_{1},-_{2}\webright ). \]

By Chapter 4: Pointed Sets, Item 4 of Proposition 4.1.4.1.1, we also have a natural isomorphism

\[ \mathsf{Sets}_{*}\webleft (S^{0},\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}\webright )\cong \webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}. \]

Composing both natural isomorphisms, we obtain a natural isomorphism

\[ \mathsf{Sets}_{*}\webleft (-_{1},-_{2}\webright )\cong \webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}. \]

Given $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, we will write

\[ \text{id}^{\textup{Hom}}_{X,Y}\colon \mathsf{Sets}_{*}\webleft (X,Y\webright )\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }\webleft [X,Y\webright ]_{\mathsf{Sets}_{*}} \]

for the component of this isomorphism at $\webleft (X,Y\webright )$.

Constructing an Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

Since $\otimes _{\mathsf{Sets}_{*}}$ is adjoint in each variable to $\webleft [-_{1},-_{2}\webright ]_{\mathsf{Sets}_{*}}$ by assumption and $\wedge $ is adjoint in each variable to $\mathsf{Sets}_{*}\webleft (-_{1},-_{2}\webright )$ by Chapter 2: Constructions With Sets, Item 2 of Proposition 2.3.5.1.2, uniqueness of adjoints (

) gives us natural isomorphisms

\begin{align*} X\otimes _{\mathsf{Sets}_{*}}- & \cong X\wedge -,\\ -\otimes _{\mathsf{Sets}_{*}}Y & \cong Y\wedge -. \end{align*}

By , we then have $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$. We will write

\[ \text{id}^{\otimes }_{\mathsf{Sets}_{*}|X,Y}\colon X\otimes _{\mathsf{Sets}_{*}}Y\overset {\scriptstyle \mathord {\sim }}{\dashrightarrow }X\wedge Y \]

for the component of this isomorphism at $\webleft (X,Y\webright )$.

Alternative Construction of an Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

Alternatively, we may construct a natural isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$ as follows:

Let $X\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Since $\otimes _{\mathsf{Sets}_{*}}$ is part of a closed monoidal structure, it preserves colimits in each variable by .
Since $X\cong \bigvee _{x\in X^{-}}S^{0}$ and $\otimes _{\mathsf{Sets}_{*}}$ preserves colimits in each variable, we have
\begin{align*} X\otimes _{\mathsf{Sets}_{*}}Y & \cong \webleft (\bigvee _{x\in X^{-}}S^{0}\webright )\otimes _{\mathsf{Sets}_{*}}Y\\ & \cong \bigvee _{x\in X^{-}}\webleft (S^{0}\otimes _{\mathsf{Sets}_{*}}Y\webright )\\ & \cong \bigvee _{x\in X^{-}}Y\\ & \cong \bigvee _{x\in X^{-}}S^{0}\wedge Y\\ & \cong \webleft (\bigvee _{x\in X^{-}}S^{0}\webright )\wedge Y\\ & \cong X\wedge Y, \end{align*}

naturally in $Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, where we have used that $S^{0}$ is the monoidal unit for $\otimes _{\mathsf{Sets}_{*}}$. Thus $X\otimes _{\mathsf{Sets}_{*}}-\cong X\wedge -$ for each $X\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
Similarly, $-\otimes _{\mathsf{Sets}_{*}}Y\cong -\wedge Y$ for each $Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$.
By , we then have $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$.

Below, we’ll show that if a natural isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$ exists, then it must be unique. This will show that the isomorphism constructed above is equal to the isomorphism $\text{id}^{\otimes }_{\mathsf{Sets}_{*}|X,Y}\colon X\otimes _{\mathsf{Sets}_{*}}Y\to X\wedge Y$ from before.

Constructing an Isomorphism $\text{id}^{\otimes }_{\mathbb {1}}\colon \mathbb {1}_{\mathsf{Sets}_{*}}\to S^{0}$

We define an isomorphism $\text{id}^{\otimes }_{\mathbb {1}}\colon \mathbb {1}_{\mathsf{Sets}_{*}}\to S^{0}$ as the composition

\[ \mathbb {1}_{\mathsf{Sets}_{*}}\overset {\rho ^{\mathsf{Sets}_{*},-1}_{\mathbb {1}_{\mathsf{Sets}_{*}}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\mathbb {1}_{\mathsf{Sets}_{*}}\wedge S^{0}\overset {\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|\mathbb {1}_{\mathsf{Sets}_{*}}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}\mathbb {1}_{\mathsf{Sets}_{*}}\otimes _{\mathsf{Sets}_{*}} S^{0}\overset {\lambda '_{ S^{0}}}{\underset {\scriptstyle \mathord {\sim }}{\dashrightarrow }}S^{0} \]

in $\mathsf{Sets}_{*}$.

Monoidal Left Unity of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

We have to show that the diagram

commutes. To this end, we will first show that the diagram

corresponding to the case $X=S^{0}$, commutes. Indeed, consider the diagram

whose boundary diagram corresponds to the diagram $\webleft (\dagger \webright )$ above. In this diagram:

Subdiagrams $\webleft (1\webright )$, $\webleft (2\webright )$, and $\webleft (3\webright )$ commute by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (4\webright )$ commutes by .
Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\rho ^{\mathsf{Sets}_{*},-1}$.
Subdiagram $\webleft (6\webright )$ commutes trivially.
Subdiagram $\webleft (7\webright )$ commutes by the naturality of $\rho ^{\mathsf{Sets}_{*}}$, where the equality $\rho ^{\mathsf{Sets}_{*}}_{S^{0}}=\lambda ^{\mathsf{Sets}_{*}}_{S^{0}}$ comes from .

Since all subdiagrams commute, so does the boundary diagram, i.e. the diagram $\webleft (\dagger \webright )$ above. As a result, the diagram

also commutes. Now, let $X\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, let $x\in X$, and consider the diagram

Since:

Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\lambda ^{\prime ,-1}$.
Subdiagram $\webleft (\ddagger \webright )$ commutes, as proved above.
Subdiagram $\webleft (4\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (1\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (3\webright )$ commutes by the naturality of $\lambda ^{\mathsf{Sets}_{*},-1}$.

it follows that the diagram

also commutes. Here’s an interactive step-by-step showcase of this argument:

We then have

\begin{align*} \lambda ^{\prime ,-1}_{X}\webleft (x\webright ) & = \webleft [\lambda ^{\prime ,-1}_{X}\circ \webleft [x\webright ]\webright ]\webleft (1\webright )\\ & = \webleft [\webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}\wedge \text{id}_{X}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|S^{0},X}\circ \lambda ^{\mathsf{Sets}_{*},-1}_{X}\circ \webleft [x\webright ]\webright ]\webleft (1\webright )\\ & = \webleft [\webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}\wedge \text{id}_{X}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|S^{0},X}\circ \lambda ^{\mathsf{Sets}_{*},-1}_{X}\webright ]\webleft (x\webright ) \end{align*}

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

\[ \lambda ^{\prime ,-1}_{X}=\webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}\wedge \text{id}_{X}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|S^{0},X}\circ \lambda ^{\mathsf{Sets}_{*},-1}_{X}. \]

Taking inverses then gives

\[ \lambda ^{\prime }_{X}=\lambda ^{\mathsf{Sets}_{*}}_{X}\circ \text{id}^{\otimes }_{\mathsf{Sets}_{*}|S^{0},X}\circ \webleft (\text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}_{*}}\wedge \text{id}_{X}\webright ), \]

showing that the diagram

indeed commutes.

Braidedness of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

We have to show that the diagram

commutes. To this end, we will first show that the diagram

commutes. To that end, we will first show that the diagram

commutes, and, to this end, we will first show that the diagram

commutes. Indeed, consider the diagram

whose boundary diagram corresponds to diagram $\webleft (\S \webright )$ above. Since:

Subdiagram $\webleft (1\webright )$ commutes by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$;
Subdiagrams $\webleft (2\webright )$ and $\webleft (3\webright )$ commute by the functoriality of $\otimes $;
Subdiagram $\webleft (4\webright )$ commutes by the left monoidal unity of $\webleft (\text{id}^{\otimes },\text{id}^{\otimes }_{\mathbb {1}}\webright )$, which we proved above;
Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\lambda '$;
Subdiagram $\webleft (6\webright )$ commutes by the naturality of $\rho '$, where the equality $\rho '_{\mathbb {1}_{\mathsf{Sets}_{*}}}=\lambda '_{\mathbb {1}_{\mathsf{Sets}_{*}}}$ comes from ;

it follows that the boundary diagram, i.e. diagram $\webleft (\S \webright )$, also commutes. Next, consider the diagram

whose boundary diagram corresponds to the diagram $\webleft (\ddagger \webright )$ above. Since:

Subdiagrams $\webleft (1\webright )$ and $\webleft (6\webright )$ commute by ;
Subdiagram $\webleft (2\webright )$ commutes by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$;
Subdiagram $\webleft (\S \webright )$ commutes, as was shown above;
Subdiagram $\webleft (3\webright )$ commutes by the naturality of $\lambda ^{\mathsf{Sets}_{*}}$;
Subdiagram $\webleft (4\webright )$ commutes trivially;
Subdiagram $\webleft (5\webright )$ commutes by of of , whose proof uses only the left monoidal unity of $\webleft (\text{id}^{\otimes },\text{id}^{\otimes }_{\mathbb {1}}\webright )$, which has been proven above;

it follows that the boundary diagram, i.e. diagram $\webleft (\ddagger \webright )$, also commutes. Next, consider the diagram

whose boundary diagram corresponds to the diagram $\webleft (\dagger \webright )$. Since:

Subdiagram $\webleft (1\webright )$ commutes by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$;
Subdiagram $\webleft (2\webright )$ commutes by the naturality of $\sigma '$ and the fact that $\text{id}^{\otimes }_{\mathbb {1}}$ is invertible;
Subdiagram $\webleft (\ddagger \webright )$ commutes as proved above;
Subdiagram $\webleft (3\webright )$ commutes by the naturality of $\sigma ^{\mathsf{Sets}_{*}}$ and the fact that $\text{id}^{\otimes }_{\mathbb {1}}$ is invertible;
Subdiagram $\webleft (4\webright )$ commutes by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$;

it follows that the boundary diagram, i.e. diagram $\webleft (\dagger \webright )$ also commutes. Taking inverses for the diagram $\webleft (\dagger \webright )$, we see that the diagram

commutes as well. Now, let $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, let $x\in X$, let $y\in Y$, and consider the diagram

which we partition into subdiagrams as follows:

Since:

Subdiagram $\webleft (2\webright )$ commutes by the naturality of $\sigma ^{\mathsf{Sets}_{*},-1}$.
Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}$.
Subdiagram $\webleft (¶\webright )$ commutes, as proved above.
Subdiagram $\webleft (4\webright )$ commutes by the naturality of $\sigma ^{\prime ,-1}$.
Subdiagram $\webleft (1\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}$.

it follows that the diagram

commutes. We then have

\begin{align*} \webleft [\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y}\circ \sigma ^{\mathsf{Sets}_{*},-1}_{X,Y}\webright ]\webleft (y,x\webright ) & = \webleft [\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y}\circ \sigma ^{\mathsf{Sets}_{*},-1}_{X,Y}\circ \webleft (\webleft [y\webright ]\wedge \webleft [x\webright ]\webright )\webright ]\webleft (1,1\webright )\\ & = \webleft [\sigma ^{\prime ,-1}_{X,Y}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|Y,X}\circ \webleft (\webleft [y\webright ]\wedge \webleft [x\webright ]\webright )\webright ]\webleft (1,1\webright )\\ & = \webleft [\sigma ^{\prime ,-1}_{X,Y}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|Y,X}\webright ]\webleft (y,x\webright ) \end{align*}

for each $\webleft (y,x\webright )\in Y\wedge X$, and thus we have

\[ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y}\circ \sigma ^{\mathsf{Sets}_{*},-1}_{X,Y}=\sigma ^{\prime ,-1}_{X,Y}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|Y,X}. \]

Taking inverses then gives

\[ \sigma ^{\mathsf{Sets}_{*}}_{X,Y}\circ \text{id}^{\otimes }_{\mathsf{Sets}_{*}|X,Y}=\text{id}^{\otimes }_{\mathsf{Sets}_{*}|Y,X}\circ \sigma ^{\prime }_{X,Y}, \]

showing that the diagram

indeed commutes.

Monoidal Right Unity of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

We have to show that the diagram

commutes. To this end, we will first show that the diagram

corresponding to the case $X=S^{0}$, commutes. First, notice that we may write

\[ \sigma '_{S^{0},\mathbb {1}_{\mathsf{Sets}_{*}}}\colon S^{0}\otimes _{\mathsf{Sets}_{*}}\mathbb {1}_{\mathsf{Sets}_{*}}\to \mathbb {1}_{\mathsf{Sets}_{*}}\otimes _{\mathsf{Sets}_{*}}S^{0} \]

as the composition

Indeed, we may write this composition as part of the diagram

which commutes since:

Subdiagram $\webleft (1\webright )$ commutes by the braidedness of $\text{id}^{\otimes }$, as proved above.
Subdiagram $\webleft (2\webright )$ commutes by .

Next, consider the diagram

whose boundary diagram corresponds to the diagram $\webleft (\dagger \webright )$ above, since the composition in red is equal to $\sigma '_{S^{0},\mathbb {1}_{\mathsf{Sets}_{*}}}$ as proved above, and then the composition in red composed with $\lambda '_{S^{0}}$ is equal to $\rho '_{S^{0}}$ by

. In this diagram:

Subdiagrams $\webleft (1\webright )$, $\webleft (2\webright )$, and $\webleft (3\webright )$ commute by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$.
Subdiagrams $\webleft (4\webright )$, $\webleft (5\webright )$, and $\webleft (6\webright )$ commute by the naturality of $\lambda ^{\mathsf{Sets}_{*}}$, where the equality $\lambda ^{\mathsf{Sets}_{*}}_{S^{0}}=\rho ^{\mathsf{Sets}_{*}}_{S^{0}}$ comes from .

Since all subdiagrams commute, so does the boundary diagram, i.e. the diagram $\webleft (\dagger \webright )$ above. As a result, the diagram

also commutes. Now, let $X\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, let $x\in X$, and consider the diagram

Since:

Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\rho ^{\prime ,-1}$.
Subdiagram $\webleft (\dagger \webright )$ commutes, as proved above.
Subdiagram $\webleft (4\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (1\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (3\webright )$ commutes by the naturality of $\rho ^{\mathsf{Sets}_{*},-1}$.

it follows that the diagram

also commutes. Here’s an interactive step-by-step showcase of this argument:

We then have

\begin{align*} \rho ^{\prime ,-1}_{X}\webleft (a\webright ) & = \webleft [\rho ^{\prime ,-1}_{X}\circ \webleft [x\webright ]\webright ]\webleft (1\webright )\\ & = \webleft [\webleft (\text{id}_{X}\wedge \text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|S^{0},X}\circ \rho ^{\mathsf{Sets}_{*},-1}_{X}\circ \webleft [x\webright ]\webright ]\webleft (1\webright )\\ & = \webleft [\webleft (\text{id}_{X}\wedge \text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|S^{0},X}\circ \rho ^{\mathsf{Sets}_{*},-1}_{X}\webright ]\webleft (a\webright ) \end{align*}

for each $a\in X$, and thus we have

\[ \rho ^{\prime ,-1}_{X}=\webleft (\text{id}_{X}\wedge \text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}_{*}}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|S^{0},X}\circ \rho ^{\mathsf{Sets}_{*},-1}_{X}. \]

Taking inverses then gives

\[ \rho ^{\prime }_{X}=\rho ^{\mathsf{Sets}_{*}}_{X}\circ \text{id}^{\otimes }_{\mathsf{Sets}_{*}|S^{0},X}\circ \webleft (\text{id}_{X}\wedge \text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}_{*}}\webright ), \]

showing that the diagram

indeed commutes.

Monoidality of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

We have to show that the diagram

commutes. To this end, we will first prove that the diagram

commutes, and, to that end, we will first show that the diagram

commutes. Indeed, consider the diagram

whose boundary diagram corresponds to diagram $\webleft (\ddagger \webright )$ above. Since:

Subdiagrams $\webleft (1\webright )$, $\webleft (4\webright )$, $\webleft (5\webright )$, $\webleft (8\webright )$, and $\webleft (11\webright )$ commute by the naturality of $\text{id}^{\otimes }_{\mathsf{Sets}_{*}}$;
Subdiagram $\webleft (2\webright )$ commutes by the right monoidal unity of $\webleft (\text{id}^{\otimes }_{\mathsf{Sets}_{*}},\text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}_{*}}\webright )$;
Subdiagram $\webleft (3\webright )$ commutes by the triangle identity for $\webleft (\alpha ',\lambda ',\rho '\webright )$;
Subdiagram $\webleft (6\webright )$ commutes by ;
Subdiagram $\webleft (7\webright )$ commutes by the naturality of $\rho ^{\mathsf{Sets}_{*}}$;
Subdiagram $\webleft (9\webright )$ commutes by ;
Subdiagram $\webleft (10\webright )$ commutes by ;

it follows that the boundary diagram, i.e. diagram $\webleft (\ddagger \webright )$, also commutes. Consider now the diagram

whose boundary corresponds to diagram $\webleft (\dagger \webright )$ above. Since:

Subdiagrams $\webleft (1\webright )$, $\webleft (3\webright )$, $\webleft (4\webright )$, and $\webleft (6\webright )$ commute by the naturality of $\text{id}^{\otimes }_{Sets_{*}}$;
Subdiagram $\webleft (\ddagger \webright )$ commutes, as proved above;
Subdiagram $\webleft (2\webright )$ commutes by the naturality of $\alpha '$;
Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\alpha ^{\mathsf{Sets}_{*}}$;

it follows that the boundary diagram, i.e. diagram $\webleft (\dagger \webright )$, also commutes. Taking inverses on the diagram $\webleft (\dagger \webright )$, we see that the diagram

commutes as well. Now, let $X,Y,Z\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$, let $x\in X$, let $y\in Y$, let $z\in Z$, and consider the diagram

which we partition into subdiagrams as follows:

Since:

Subdiagram $\webleft (1\webright )$ commutes by the naturality of $\alpha ^{\mathsf{Sets}_{*},-1}$.
Subdiagram $\webleft (2\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (3\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (\dagger \webright )$ commutes, as proved above.
Subdiagram $\webleft (4\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (5\webright )$ commutes by the naturality of $\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}}$.
Subdiagram $\webleft (6\webright )$ commutes by the naturality of $\alpha ^{\prime ,-1}$.

it follows that the diagram

also commutes. We then have

\begin{align*} \webleft[\webleft (\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y}\otimes _{\mathsf{Sets}_{*}}\text{id}_{Z}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X\wedge Y,Z}\right.\\ \left.{}\circ \alpha ^{\mathsf{Sets}_{*},-1}_{X,Y,Z}\webright]\webleft (x,\webleft (y,z\webright )\webright ) & = \webleft[\webleft (\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y}\otimes _{\mathsf{Sets}_{*}}\text{id}_{Z}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X\wedge Y,Z}\right.\\ & \phantom{={}} \mkern 4mu\left.{}{}\circ \alpha ^{\mathsf{Sets}_{*},-1}_{X,Y,Z}\circ \webleft (\webleft [x\webright ]\wedge \webleft (\webleft [y\webright ]\wedge \webleft [z\webright ]\webright )\webright )\webright]\webleft (1,\webleft (1,1\webright )\webright )\\ & = \webleft[\alpha ^{\prime ,-1}_{X,Y,Z}\circ \webleft (\text{id}_{X}\wedge \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|Y,Z}\webright )\right.\\ & \phantom{={}} \mkern 4mu\left.{}\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y\wedge Z}\circ \webleft (\webleft [x\webright ]\wedge \webleft (\webleft [y\webright ]\wedge \webleft [z\webright ]\webright )\webright )\webright]\webleft (1,\webleft (1,1\webright )\webright )\\ & = \webleft [\alpha ^{\prime ,-1}_{X,Y,Z}\circ \webleft (\text{id}_{X}\wedge \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|Y,Z}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y\wedge Z}\webright ]\webleft (x,\webleft (y,z\webright )\webright ) \end{align*}

for each $\webleft (x,\webleft (y,z\webright )\webright )\in X\wedge \webleft (Y\wedge Z\webright )$, and thus we have

\[ \webleft (\text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y}\otimes _{\mathsf{Sets}_{*}}\text{id}_{Z}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X\wedge Y,Z}\circ \alpha ^{\mathsf{Sets}_{*},-1}_{X,Y,Z}=\alpha ^{\prime ,-1}_{X,Y,Z}\circ \webleft (\text{id}_{X}\wedge \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|Y,Z}\webright )\circ \text{id}^{\otimes ,-1}_{\mathsf{Sets}_{*}|X,Y\wedge Z}. \]

Taking inverses then gives

\[ \alpha ^{\mathsf{Sets}_{*}}_{X,Y,Z}\circ \text{id}^{\otimes }_{\mathsf{Sets}_{*}|X\wedge Y,Z}\circ \webleft (\text{id}^{\otimes }_{\mathsf{Sets}_{*}|X,Y}\otimes _{\mathsf{Sets}_{*}}\text{id}_{Z}\webright )=\text{id}^{\otimes }_{\mathsf{Sets}_{*}|X,Y\wedge Z}\circ \webleft (\text{id}_{X}\wedge \text{id}^{\otimes }_{\mathsf{Sets}_{*}|Y,Z}\webright )\circ \alpha ^{\prime }_{X,Y,Z}, \]

showing that the diagram

indeed commutes.

Uniqueness of the Isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\wedge }$

Let $\phi ,\psi \colon -_{1}\otimes _{\mathsf{Sets}_{*}}-_{2}\Rightarrow -_{1}\wedge -_{2}$ be natural isomorphisms. Since these isomorphisms are compatible with the unitors of $\mathsf{Sets}_{*}$ with respect to $\wedge $ and $\otimes $ (as shown above), we have

\begin{align*} \lambda '_{Y} & = \lambda ^{\mathsf{Sets}_{*}}_{Y}\circ \phi _{S^{0},Y}\circ \webleft (\text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\text{id}_{Y}\webright ),\\ \lambda '_{Y} & = \lambda ^{\mathsf{Sets}_{*}}_{Y}\circ \psi _{S^{0},Y}\circ \webleft (\text{id}^{\otimes }_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\text{id}_{Y}\webright ). \end{align*}

Postcomposing both sides with $\lambda ^{\mathsf{Sets}_{*},-1}_{Y}$ and then precomposing both sides with $\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\text{id}_{Y}$ gives

\begin{align*} \lambda ^{\mathsf{Sets}_{*},-1}_{Y}\circ \lambda '_{Y}\circ \webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\text{id}_{Y}\webright ) & = \phi _{S^{0},Y},\\ \lambda ^{\mathsf{Sets}_{*},-1}_{Y}\circ \lambda '_{Y}\circ \webleft (\text{id}^{\otimes ,-1}_{\mathbb {1}|\mathsf{Sets}}\otimes _{\mathsf{Sets}}\text{id}_{Y}\webright ) & = \psi _{S^{0},Y}, \end{align*}

and thus we have

\[ \phi _{S^{0},Y}=\psi _{S^{0},Y} \]

for each $Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$. Now, let $x\in X$ and consider the naturality diagrams

for $\phi $ and $\psi $ with respect to the morphisms $\webleft [x\webright ]$ and $\text{id}_{Y}$. Having shown that $\phi _{S^{0},Y}=\psi _{S^{0},Y}$, we have

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

for each $\webleft (x,y\webright )\in X\wedge Y$. Therefore we have

\[ \phi _{X,Y}=\psi _{X,Y} \]

for each $X,Y\in \text{Obj}\webleft (\mathsf{Sets}_{*}\webright )$ and thus $\phi =\psi $, showing the isomorphism $\mathord {\otimes _{\mathsf{Sets}_{*}}}\cong \mathord {\times }$ to be unique.