Item 1c (020R) — The Clowder Project

4.4.1 Foundations

Let $X$ be a set.

The powerset of $X$ is the set $\mathcal{P}\webleft (X\webright )$ defined by

\[ \mathcal{P}\webleft (X\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ U\in P\ \middle |\ U\subset X\right\} , \]

where $P$ is the set in the axiom of powerset, of .

Remark 4.4.1.1.2 ▶ Powersets as Decategorifications of Co/Presheaf Categories

Under the analogy that $\{ \mathsf{t},\mathsf{f}\} $ should be the $\webleft (-1\webright )$-categorical analogue of $\mathsf{Sets}$, we may view the powerset of a set as a decategorification of the category of presheaves of a category (or of the category of copresheaves):

•
The powerset of a set $X$ is equivalently (Item 2 of Proposition 4.5.1.1.4) the set

\[ \mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright ) \]

of functions from $X$ to the set $\{ \mathsf{t},\mathsf{f}\} $ of classical truth values.
•
The category of presheaves on a category $\mathcal{C}$ is the category

\[ \mathsf{Fun}\webleft (\mathcal{C}^{\mathsf{op}},\mathsf{Sets}\webright ) \]

of functors from $\mathcal{C}^{\mathsf{op}}$ to the category $\mathsf{Sets}$ of sets.

Let $X$ be a set.

1.
We write $\mathcal{P}_{0}\webleft (X\webright )$ for the set of nonempty subsets of $X$.
2.
We write $\mathcal{P}_{\mathrm{fin}}\webleft (X\webright )$ for the set of finite subsets of $X$.

Proposition 4.4.1.1.4 ▶ Elementary Properties of Powersets

Let $X$ be a set.

1.
Co/Completeness. The (posetal) category (associated to) $\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )$ is complete and cocomplete:
1. (a)
  Products. The products in $\mathcal{P}\webleft (X\webright )$ are given by intersection of subsets.
2. (b)
  Coproducts. The coproducts in $\mathcal{P}\webleft (X\webright )$ are given by union of subsets.

(c)
Co/Equalisers. Being a posetal category, $\mathcal{P}\webleft (X\webright )$ only has at most one morphisms between any two objects, so co/equalisers are trivial.

Cartesian Closedness. The category $\mathcal{P}\webleft (X\webright )$ is Cartesian closed.

Powersets as Sets of Relations. We have bijections

\begin{align*} \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (\mathrm{pt},X\webright ),\\ \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (X,\mathrm{pt}\webright ), \end{align*}

natural in $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$.

Interaction With Products I. The map

is an isomorphism of sets, natural in $X,Y\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ with respect to each of the functor structures $\mathcal{P}_{!}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{*}$ on $\mathcal{P}$ of Proposition 4.4.2.1.1. Moreover, this makes each of $\mathcal{P}_{!}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{*}$ into a symmetric monoidal functor.

Interaction With Products II. The map

where¹

\[ U\boxtimes _{X\times Y}V\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \webleft (u,v\webright )\in X\times Y\ \middle |\ \text{$u\in U$ and $v\in V$}\right\} \]

is an inclusion of sets, natural in $X,Y\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ with respect to each of the functor structures $\mathcal{P}_{!}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{*}$ on $\mathcal{P}$ of Proposition 4.4.2.1.1. Moreover, this makes each of $\mathcal{P}_{!}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{*}$ into a symmetric monoidal functor.

Interaction With Products III. We have an isomorphism

\[ \mathcal{P}\webleft (X\webright )\otimes \mathcal{P}\webleft (Y\webright )\cong \mathcal{P}\webleft (X\times Y\webright ), \]

natural in $X,Y\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$ with respect to each of the functor structures $\mathcal{P}_{!}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{*}$ on $\mathcal{P}$ of Proposition 4.4.2.1.1, where $\otimes $ denotes the tensor product of suplattices of . Moreover, this makes each of $\mathcal{P}_{!}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{*}$ into a symmetric monoidal functor.

¹The set $U\boxtimes _{X\times Y}V$ is usually denoted simply $U\times V$. Here we denote it in this somewhat weird way to highlight the similarity to external tensor products in six-functor formalisms (see also Section 4.6.4).

Proof of Proposition 4.4.1.1.4.

Item 1: Co/Completeness

Omitted.

Item 2: Cartesian Closedness

See Section 4.4.7.

Item 3: Powersets as Sets of Relations

Indeed, we have

\begin{align*} \mathrm{Rel}\webleft (\mathrm{pt},X\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathcal{P}\webleft (\mathrm{pt}\times X\webright )\\ & \cong \mathcal{P}\webleft (X\webright ) \end{align*}

and

\begin{align*} \mathrm{Rel}\webleft (X,\mathrm{pt}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathcal{P}\webleft (X\times \mathrm{pt}\webright )\\ & \cong \mathcal{P}\webleft (X\webright ), \end{align*}

where we have used Item 5 of Proposition 4.1.3.1.3.

Item 4: Interaction With Products I

The inverse of the map in the statement is the map

\[ \Phi \colon \mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )\to \mathcal{P}\webleft (X\webright )\times \mathcal{P}\webleft (Y\webright ) \]

defined by

\[ \Phi \webleft (S\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (S_{X},S_{Y}\webright ) \]

for each $S\in \mathcal{P}\webleft (X\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}Y\webright )$, where

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

The rest of the proof is omitted.

Item 5: Interaction With Products II

Omitted.

Item 6: Interaction With Products III

Omitted.