Proposition 2.4.3.1.5 (0070): Properties of Powersets: Monoidality

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`

Let $X$ be a set.

Symmetric Strong Monoidality With Respect to Coproducts I. The powerset functor $\mathcal{P}_{*}$ of Item 1 of Proposition 2.4.3.1.4 has a symmetric strong monoidal structure
\[ \webleft (\mathcal{P}_{*},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \]

being equipped with isomorphisms

\[ \begin{gathered} \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \xrightarrow {\cong }\mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ),\\ \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Symmetric Strong Monoidality With Respect to Coproducts II. The powerset functor $\mathcal{P}^{-1}$ of Item 2 of Proposition 2.4.3.1.4 has a symmetric strong monoidal structure
\[ \webleft (\mathcal{P}^{-1},\mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}},\mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets}^{\mathsf{op}},\times ^{\mathsf{op}},\text{pt}\webright ) \to \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \]

being equipped with isomorphisms

\[ \begin{gathered} \mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \xrightarrow {\cong }\mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ),\\ \mathcal{P}^{-1|\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Symmetric Strong Monoidality With Respect to Coproducts III. The powerset functor $\mathcal{P}_{!}$ of Item 3 of Proposition 2.4.3.1.4 has a symmetric strong monoidal structure
\[ \webleft (\mathcal{P}_{!},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!},\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }},\emptyset \webright ) \]

being equipped with isomorphisms

\[ \begin{gathered} \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \xrightarrow {\cong }\mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ),\\ \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{!|\mathbb {1}} \colon \text{pt}\xrightarrow {\cong }\mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Symmetric Lax Monoidality With Respect to Products I. The powerset functor $\mathcal{P}_{*}$ of Item 1 of Proposition 2.4.3.1.4 has a symmetric lax monoidal structure
\[ \webleft (\mathcal{P}_{*},\mathcal{P}^{\otimes }_{*},\mathcal{P}^{\otimes }_{*|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \]

being equipped with morphisms

\[ \begin{gathered} \mathcal{P}^{\times }_{*|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \to \mathcal{P}\webleft (X\times Y\webright ),\\ \mathcal{P}^{\times }_{*|\mathbb {1}} \colon \text{pt}\to \mathcal{P}\webleft (\text{pt}\webright ), \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, where
- The map $\mathcal{P}^{\times }_{*|X,Y}$ is given by
  
  \[ \mathcal{P}^{\times }_{*|X,Y}\webleft (U,V\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}U\times V \]
  
  for each $\webleft (U,V\webright )\in \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )$,
- The map $\mathcal{P}^{\times }_{*|\mathbb {1}}$ is given by
  
  \[ \mathcal{P}^{\times }_{*|\mathbb {1}}\webleft (\star \webright )=\text{pt}. \]
Symmetric Lax Monoidality With Respect to Products II. The powerset functor $\mathcal{P}^{-1}$ of Item 2 of Proposition 2.4.3.1.4 has a symmetric lax monoidal structure
\[ \webleft (\mathcal{P}^{-1},\mathcal{P}^{-1|\otimes },\mathcal{P}^{-1|\otimes }_{\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets}^{\mathsf{op}},\times ^{\mathsf{op}},\text{pt}\webright ) \to \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \]

being equipped with morphisms

\[ \begin{gathered} \mathcal{P}^{-1|\times }_{X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \to \mathcal{P}\webleft (X\times Y\webright ),\\ \mathcal{P}^{\times }_{\mathbb {1}} \colon \text{pt}\to \mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, defined as in Item 4.
Symmetric Lax Monoidality With Respect to Products III. The powerset functor $\mathcal{P}_{!}$ of Item 3 of Proposition 2.4.3.1.4 has a symmetric lax monoidal structure
\[ \webleft (\mathcal{P}_{!},\mathcal{P}^{\otimes }_{!},\mathcal{P}^{\otimes }_{!|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \to \webleft (\mathsf{Sets},\times ,\text{pt}\webright ) \]

being equipped with morphisms

\[ \begin{gathered} \mathcal{P}^{\times }_{!|X,Y} \colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \to \mathcal{P}\webleft (X\times Y\webright ),\\ \mathcal{P}^{\times }_{!|\mathbb {1}} \colon \text{pt}\to \mathcal{P}\webleft (\emptyset \webright ), \end{gathered} \]

natural in $X,Y\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, defined as in Item 4.

Item 1: Symmetric Strong Monoidality With Respect to Coproducts I

The isomorphism

\[ \mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|X,Y}\colon \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )\to \mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright ) \]

is given by sending $\webleft (U,V\webright )\in \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )$ to $U\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}V$, with inverse given by sending a subset $S$ of $X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y$ to the pair $\webleft (S_{X},S_{Y}\webright )\in \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright )$ with

\begin{align*} S_{X} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ \webleft (0,x\webright )\in S\webright\} \\ S_{Y} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ y\in Y\ \middle |\ \webleft (1,y\webright )\in S\webright\} . \end{align*}

The isomorphism $\text{pt}\cong \mathcal{P}\webleft (\emptyset \webright )$ is given by $\star \mapsto \emptyset \in \mathcal{P}\webleft (\emptyset \webright )$.

Naturality for the isomorphism $\mathcal{P}^{\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}}_{*|X,Y}$ is the statement that, given maps of sets $f\colon X\to X'$ and $g\colon Y\to Y'$, the diagram

commutes, which is clear, as it acts on elements as

where we are using Item 7 of Proposition 2.4.4.1.4.

Finally, monoidality, unity, and symmetry of $\mathcal{P}_{*}$ as a monoidal functor follow by checking the commutativity of the relevant diagrams on elements.

Item 2: Symmetric Strong Monoidality With Respect to Coproducts II

The proof is similar to Item 1, and is hence omitted.

Item 3: Symmetric Strong Monoidality With Respect to Coproducts III

The proof is similar to Item 1, and is hence omitted.

Item 4: Symmetric Lax Monoidality With Respect to Products I

Naturality for the morphism $\mathcal{P}^{\times }_{*|X,Y}$ is the statement that, given maps of sets $f\colon X\to X'$ and $g\colon Y\to Y'$, the diagram

commutes, which is clear, as it acts on elements as

where we are using Item 8 of Proposition 2.4.4.1.4.

Finally, monoidality, unity, and symmetry of $\mathcal{P}_{*}$ as a monoidal functor follow by checking the commutativity of the relevant diagrams on elements.

Item 5: Symmetric Lax Monoidality With Respect to Products II

The proof is similar to Item 4, and is hence omitted.

Item 6: Symmetric Lax Monoidality With Respect to Products III

The proof is similar to Item 4, and is hence omitted.