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 )$
By , 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 Taking inverses then gives 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.