Proposition 2.4.1.1.4 (01J3): Elementary Properties of Powersets

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.

Co/Completeness. The (posetal) category (associated to) $\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )$ is complete and cocomplete:
1. Products. The products in $\mathcal{P}\webleft (X\webright )$ are given by intersection of subsets.
2. Coproducts. The coproducts in $\mathcal{P}\webleft (X\webright )$ are given by union of subsets.
3. 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 (\text{pt},X\webright ),\\ \mathcal{P}\webleft (X\webright ) & \cong \mathrm{Rel}\webleft (X,\text{pt}\webright ), \end{align*}

natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Interaction With Products I. The map
is an isomorphism of sets, natural in $X,Y\in \text{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 2.4.2.1.1. Moreover, this makes $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ into symmetric monoidal functors.
Interaction With Products II. The map
where
\[ U\boxtimes _{X\times Y}V\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ \webleft (u,v\webright )\in X\times Y\ \middle |\ \text{$u\in U$ and $v\in V$}\webright\} \]

is an inclusion of sets, natural in $X,Y\in \text{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 2.4.2.1.1. Moreover, this makes $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ into symmetric monoidal functors.
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 \text{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 2.4.2.1.1, where $\otimes $ denotes the tensor product of suplattices of . Moreover, this makes $\mathcal{P}_{*}$, $\mathcal{P}^{-1}$, and $\mathcal{P}_{!}$ into symmetric monoidal functors.

Item 1: Co/Completeness

Omitted.

Item 2: Cartesian Closedness

Item 3: Powersets as Sets of Relations

Indeed, we have

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

and

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

where we have used Item 4 of Proposition 2.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}}}=}}\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 rest of the proof is omitted.

Item 5: Interaction With Products II

Omitted.

Item 6: Interaction With Products III

Omitted.