Subsection 2.4.5 (01JK): Powersets as Free Cocompletions

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`

2.4.5 Powersets as Free Cocompletions

Let $X$ be a set.

Proposition 2.4.5.1.1 ▶ Powersets as Free Cocompletions: Universal Property

The pair $\webleft (\mathcal{P}\webleft (X\webright ),\chi _{\webleft (-\webright )}\webright )$ consisting of

The powerset $\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )$ of $X$ of Definition 2.4.1.1.1;
The characteristic embedding $\chi _{\webleft (-\webright )}\colon X\hookrightarrow \mathcal{P}\webleft (X\webright )$ of $X$ into $\mathcal{P}\webleft (X\webright )$ of Definition 2.5.4.1.1;

satisfies the following universal property:

Given another pair $\webleft (Y,f\webright )$ consisting of
- A suplattice $\webleft (Y,\preceq \webright )$;
- A function $f\colon X\to Y$;
there exists a unique morphism of suplattices

\[ \webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )\overset {\exists !}{\to }\webleft (Y,\preceq \webright ) \]

making the diagram

commute.

Proof of Proposition 2.4.5.1.1.

This is a rephrasing ofProposition 2.4.5.1.2, which we prove below.¹

¹Here we only remark that the unique morphism of suplattices in the statement is given by the left Kan extension $\text{Lan}_{\chi _{X}}\webleft (f\webright )$ of $f$ along $\chi _{X}$.

Proposition 2.4.5.1.2 ▶ Powersets as Free Cocompletions: Adjointness

We have an adjunction

witnessed by a bijection

\[ \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \cong \mathsf{Sets}\webleft (X,Y\webright ), \]

natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $\webleft (Y,\preceq \webright )\in \text{Obj}\webleft (\mathsf{SupLat}\webright )$, where:

The category $\mathsf{SupLat}$ is the category of suplattices of .
The map

\[ \chi ^{*}_{X} \colon \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \to \mathsf{Sets}\webleft (X,Y\webright ) \]

witnessing the above bijection is defined by

\[ \chi ^{*}_{X}\webleft (f\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\circ \chi _{X}, \]

i.e. by sending a morphism of suplattices $f\colon \mathcal{P}\webleft (X\webright )\to Y$ to the composition

\[ X \overset {\chi _{X}}{\hookrightarrow } \mathcal{P}\webleft (X\webright ) \overset {f}{\to } Y. \]
The map

\[ \text{Lan}_{\chi _{X}} \colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \]

witnessing the above bijection is given by sending a function $f\colon X\to Y$ to its left Kan extension along $\chi _{X}$,
Moreover, invoking the bijection $\mathcal{P}\webleft (X\webright )\cong \mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright )$ of Item 2 of Proposition 2.5.1.1.4, $\text{Lan}_{\chi _{X}}\webleft (f\webright )$ can be explicitly computed by

\begin{align*} \webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright ) & = \int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )\\ & = \int ^{x\in X}\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )\\ & = \bigvee _{x\in X}\webleft (\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )\webright )\\ & = \webleft(\bigvee _{x\in U}\webleft (\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )\webright )\webright)\vee \webleft(\bigvee _{x\in U^{\textsf{c}}}\webleft (\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )\webright )\webright)\\ & = \webleft(\bigvee _{x\in U}f\webleft (x\webright )\webright)\vee \webleft(\bigvee _{x\in U^{\textsf{c}}}\varnothing _{Y}\webright)\\ & = \bigvee _{x\in U}f\webleft (x\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (X\webright )$, where:
- We have used for the first equality.
- We have used Proposition 2.5.5.1.1 for the second equality.
- We have used for the third equality.
- The symbol $\bigvee $ denotes the join in $\webleft (Y,\preceq \webright )$.
- The symbol $\odot $ denotes the tensor of an element of $Y$ by a truth value as in . In particular, we have
  
  \begin{align*} \mathsf{true}\odot f\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright ),\\ \mathsf{false}\odot f\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\varnothing _{Y}, \end{align*}
  
  where $\varnothing _{Y}$ is the bottom element of $\webleft (Y,\preceq \webright )$.
In particular, when $\webleft (Y,\preceq _{Y}\webright )=\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )$ for some set $B$, the Kan extension $\text{Lan}_{\chi _{X}}\webleft (f\webright )$ is given by

\begin{align*} \webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright ) & = \bigvee _{x\in U}f\webleft (x\webright )\\ & = \bigcup _{x\in U}f\webleft (x\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (X\webright )$.

Proof of Proposition 2.4.5.1.2.

Map I

We define a map

\[ \Phi _{X,Y}\colon \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \to \mathsf{Sets}\webleft (X,Y\webright ) \]

as in the statement, i.e. by

\[ \Phi _{X,Y}\webleft (f\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\circ \chi _{X} \]

for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$.

Map II

We define a map

\[ \Psi _{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright )\to \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \]

as in the statement, i.e. by

for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$.

Invertibility I

We claim that

\[ \Psi _{X,Y}\circ \Phi _{X,Y}=\text{id}_{\mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )}. \]

We have

\begin{align*} \webleft [\Psi _{X,Y}\circ \Phi _{X,Y}\webright ]\webleft (f\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (\Phi _{X,Y}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (f\circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Lan}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )\\ \end{align*}

for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$. We now claim that

\[ \text{Lan}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )=f \]

for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$. Indeed, we have

\begin{align*} \webleft[\text{Lan}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )\webright]\webleft (U\webright ) & = \bigvee _{x\in U} f\webleft (\chi _{X}\webleft (x\webright )\webright )\\ & = f\webleft(\bigvee _{x\in U}\chi _{X}\webleft (x\webright )\webright)\\ & = f\webleft(\bigcup _{x\in U}\webleft\{ x\webright\} \webright)\\ & = f\webleft (U\webright )\end{align*}

for each $U\in \mathcal{P}\webleft (X\webright )$, where we have used that $f$ is a morphism of suplattices and hence preserves joins for the second equality. This proves our claim. Since we have shown that

\[ \webleft [\Psi _{X,Y}\circ \Phi _{X,Y}\webright ]\webleft (f\webright )=f \]

for each $f\in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$, it follows that $\Psi _{X,Y}\circ \Phi _{X,Y}$ must be equal to the identity map $\text{id}_{\mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )}$ of $\mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$.

Invertibility II

We claim that

\[ \Phi _{X,Y}\circ \Psi _{X,Y}=\text{id}_{\mathsf{Sets}\webleft (X,Y\webright )}. \]

We have

\begin{align*} \webleft [\Phi _{X,Y}\circ \Psi _{X,Y}\webright ]\webleft (f\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\Psi _{X,Y}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Lan}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}\end{align*}

for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$. We now claim that

\[ \text{Lan}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}=f \]

for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$. Indeed, we have

\begin{align*} \webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}\webright ]\webleft (x\webright ) & = \bigvee _{y\in \webleft\{ x\webright\} }f\webleft (y\webright )\\ & = f\webleft (x\webright )\end{align*}

for each $x\in X$. This proves our claim. Since we have shown that

\[ \webleft [\Phi _{X,Y}\circ \Psi _{X,Y}\webright ]\webleft (f\webright )=f \]

for each $f\in \mathsf{Sets}\webleft (X,Y\webright )$, it follows that $\Phi _{X,Y}\circ \Psi _{X,Y}$ must be equal to the identity map $\text{id}_{\mathsf{Sets}\webleft (X,Y\webright )}$ of $\mathsf{Sets}\webleft (X,Y\webright )$.

Naturality for $\Phi $, Part I

We need to show that, given a function $f\colon X\to X'$, the diagram

commutes. Indeed, we have

\begin{align*} \webleft [\Phi _{X,Y}\circ \mathcal{P}_{*}\webleft (f\webright )^{*}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\mathcal{P}_{*}\webleft (f\webright )^{*}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y}\webleft (\xi \circ f_{*}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (\xi \circ f_{*}\webright )\circ \chi _{X}\\ & = \xi \circ \webleft (f_{*}\circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle (\dagger )}}{=}}}\xi \circ \webleft (\chi _{X'}\circ f\webright )\\ & = \webleft (\xi \circ \chi _{X'}\webright )\circ f\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X',Y}\webleft (\xi \webright )\circ f\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f^{*}\webleft (\Phi _{X',Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [f^{*}\circ \Phi _{X',Y}\webright ]\webleft (\xi \webright ), \end{align*}

for each $\xi \in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X'\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$, where we have used Item 1 of Proposition 2.5.4.1.3 for the fifth equality above.

Naturality for $\Phi $, Part II

We need to show that, given a morphism of suplattices

\[ g\colon \webleft (Y,\preceq _{Y}\webright )\to \webleft (Y',\preceq _{Y'}\webright ), \]

the diagram

commutes. Indeed, we have

\begin{align*} \webleft [\Phi _{X,Y'}\circ g_{*}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y'}\webleft (g_{*}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Phi _{X,Y'}\webleft (g\circ \xi \webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (g\circ \xi \webright )\circ \chi _{X}\\ & = g\circ \webleft (\xi \circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g\circ \webleft (\Phi _{X,Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g_{*}\webleft (\Phi _{X,Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [g_{*}\circ \Phi _{X,Y}\webright ]\webleft (\xi \webright ). \end{align*}

for each $\xi \in \mathsf{SupLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )$.

Naturality for $\Psi $

Since $\Phi $ is natural in each argument and $\Phi $ is a componentwise inverse to $\Psi $ in each argument, it follows from Chapter 9: Categories, Item 2 of Proposition 9.9.7.1.2 that $\Psi $ is also natural in each argument.

Warning 2.4.5.1.3 ▶ Free Cocompletion Is Not an Idempotent Operation

ゴ

Although the assignment $X\mapsto \mathcal{P}\webleft (X\webright )$ is called the free cocompletion of $X$, it is not an idempotent operation, i.e. we have $\mathcal{P}\webleft (\mathcal{P}\webleft (X\webright )\webright )\neq \mathcal{P}\webleft (X\webright )$.

ゴ

Noticed something off, or have any comments? Feel free to reach out!

You can also use the contact form below: