Proposition 2.4.6.1.2 ▶ Powersets as Free Completions: Adjointness

We have an adjunction

witnessed by a bijection

\[ \mathsf{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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{InfLat}\webright )$, where:

  • The category $\mathsf{InfLat}$ is the category of inflattices of .
  • The map

    \[ \chi ^{*}_{X} \colon \mathsf{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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 inflattices $f\colon \mathcal{P}\webleft (X\webright )^{\mathsf{op}}\to Y$ to the composition

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

  • The map

    \[ \text{Ran}_{\chi _{X}} \colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \webright ),\webleft (Y,\preceq \webright )\webright ) \]

    witnessing the above bijection is given by sending a function $f\colon X\to Y$ to its right 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{Ran}_{\chi _{X}}\webleft (f\webright )$ can be explicitly computed by

    \begin{align*} \webleft [\text{Ran}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright ) & = \int _{x\in X}\chi _{\mathcal{P}\webleft (X\webright )^{\mathsf{op}}}\webleft (\chi _{x},U\webright )\pitchfork f\webleft (x\webright )\\ & = \int _{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (U,\chi _{x}\webright )\pitchfork f\webleft (x\webright )\\ & = \int _{x\in X}\chi _{U}\webleft (x\webright )\pitchfork f\webleft (x\webright )\\ & = \bigwedge _{x\in X}\chi _{U}\webleft (x\webright )\pitchfork f\webleft (x\webright )\\ & = \webleft(\bigwedge _{x\in U}\chi _{U}\webleft (x\webright )\pitchfork f\webleft (x\webright )\webright)\wedge \webleft(\bigwedge _{x\in U^{\textsf{c}}}\chi _{U}\webleft (x\webright )\pitchfork f\webleft (x\webright )\webright)\\ & = \webleft(\bigwedge _{x\in U}f\webleft (x\webright )\webright)\wedge \webleft(\bigwedge _{x\in U^{\textsf{c}}}\infty _{Y}\webright)\\ & = \webleft(\bigwedge _{x\in U}f\webleft (x\webright )\webright)\wedge \infty _{Y}\\ & = \bigwedge _{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 $\bigwedge $ denotes the meet in $\webleft (Y,\preceq \webright )$.
    • The symbol $\pitchfork $ denotes the cotensor of an element of $Y$ by a truth value as in . In particular, we have

      \begin{align*} \mathsf{true}\pitchfork f\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (x\webright ),\\ \mathsf{false}\pitchfork f\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\infty _{Y}, \end{align*}

      where $\infty _{Y}$ is the top 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{Ran}_{\chi _{X}}\webleft (f\webright )$ is given by

    \begin{align*} \webleft [\text{Ran}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright ) & = \bigwedge _{x\in U}f\webleft (x\webright )\\ & = \bigcap _{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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \webright ),\webleft (Y,\preceq \webright )\webright )$.

Map II
We define a map

\[ \Psi _{X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright )\to \mathsf{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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{Ran}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )\\ \end{align*}

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

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

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

\begin{align*} \webleft[\text{Ran}_{\chi _{X}}\webleft (f\circ \chi _{X}\webright )\webright]\webleft (U\webright ) & = \bigwedge _{x\in U}f\webleft (\chi _{X}\webleft (x\webright )\webright )\\ & = f\webleft(\bigwedge _{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 inflattices and hence preserves meets in $\webleft (\mathcal{P}\webleft (X\webright ),\supset \webright )$ (i.e. joins in $\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )$) 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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \webright ),\webleft (Y,\preceq \webright )\webright )}$ of $\mathsf{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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{Ran}_{\chi _{X}}\webleft (f\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Ran}_{\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{Ran}_{\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{Ran}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}\webright ]\webleft (x\webright ) & = \bigwedge _{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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X'\webright ),\supset \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 cocontinuous morphism of posets

\[ 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{InfLat}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\supset \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: Preorders, Item 2 of Proposition 9.9.7.1.2 that $\Psi $ is also natural in each argument.

Previous
Next

View Proposition 2.4.6.1.2 as PDF

Statistics Cite
1 tag refers to this tag

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

You can also use the contact form below: