Proposition 2.4.3.1.6 (0077): Properties of Powersets: As Sets of Functions/Relations

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.

Powersets as Sets of Functions I. The assignment $U\mapsto \chi _{U}$ defines a bijection
\[ \chi _{\webleft (-\webright )} \colon \mathcal{P}\webleft (X\webright ) \xrightarrow {\cong }\mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright ), \]

for each $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.
Powersets as Sets of Functions II. The bijection
\[ \mathcal{P}\webleft (X\webright )\cong \mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright ) \]

of Item 1 is natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, refining to a natural isomorphism of functors

\[ \mathcal{P}^{-1}\cong \mathsf{Sets}\webleft (-,\{ \mathsf{t},\mathsf{f}\} \webright ). \]
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 )$.

Item 1: Powersets as Sets of Functions I

Indeed, the inverse of $\chi _{\webleft (-\webright )}$ is given by sending a function $f\colon X\to \{ \mathsf{t},\mathsf{f}\} $ to the subset $U_{f}$ of $\mathcal{P}\webleft (X\webright )$ defined by

\[ U_{f}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft\{ x\in X\ \middle |\ f\webleft (x\webright )=\mathsf{true}\webright\} , \]

i.e. by $U_{f}=f^{-1}\webleft (\mathsf{true}\webright )$. That $\chi _{\webleft (-\webright )}$ and $f\mapsto U_{f}$ are inverses is then straightforward to check.

Item 2: Powersets as Sets of Functions II

We need to check that, given a function $f\colon X\to Y$, the diagram

commutes, i.e. that for each $V\in \mathcal{P}\webleft (Y\webright )$, we have

\[ \chi _{V}\circ f=\chi _{f^{-1}\webleft (V\webright )}. \]

And indeed, we have

\begin{align*} \webleft [\chi _{V}\circ f\webright ]\webleft (v\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\chi _{V}\webleft (f\webleft (v\webright )\webright )\\ & = \begin{cases} \mathsf{true}& \text{if $f\webleft (v\webright )\in V$,}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & = \begin{cases} \mathsf{true}& \text{if $v\in f^{-1}\webleft (V\webright )$,}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\chi _{f^{-1}\webleft (V\webright )}\webleft (v\webright )\end{align*}

for each $v\in V$.

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.2.