The Clowder Project

natural in $X\in \text{Obj}\webleft (\mathsf{Sets}\webright )$ and $\webleft (Y,\preceq \webright )\in \text{Obj}\webleft (\mathsf{Pos}^{\mathsf{cocomp.}}\webright )$.

• Map I. We define a map
  \[ \Phi _{X,Y}\colon \mathsf{Pos}^{\mathsf{cocomp.}}\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, by

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

  for each $f\in \mathsf{Pos}^{\mathsf{cocomp.}}\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{Pos}^{\mathsf{cocomp.}}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \]

  as in the statement, 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{Pos}^{\mathsf{cocomp.}}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright )}. \]

  Indeed, given a cocontinuous morphism of posets

  \[ \xi \colon \webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )\to \webleft (Y,\preceq \webright ), \]

  we have

  \begin{align*} \webleft [\Psi _{X,Y}\circ \Phi _{X,Y}\webright ]\webleft (\xi \webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (\Phi _{X,Y}\webleft (\xi \webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\Psi _{X,Y}\webleft (\xi \circ \chi _{X}\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{Lan}_{\chi _{X}}\webleft (\xi \circ \chi _{X}\webright )\\ & \cong \bigvee _{x\in X}\chi _{\webleft (-\webright )}\webleft (x\webright )\odot \xi \webleft (\chi _{X}\webleft (x\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{clm}}}{=}}}\xi ,\end{align*}

  where indeed

  \begin{align*} \webleft[\bigvee _{x\in X}\chi _{\webleft (-\webright )}\webleft (x\webright )\odot \xi \webleft (\chi _{X}\webleft (x\webright )\webright )\webright]\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigvee _{x\in X}\chi _{U}\webleft (x\webright )\odot \xi \webleft (\chi _{X}\webleft (x\webright )\webright )\\ & = \webleft (\bigvee _{x\in U}\chi _{U}\webleft (x\webright )\odot \xi \webleft (\chi _{X}\webleft (x\webright )\webright )\webright )\vee \webleft (\bigvee _{x\in X\setminus U}\chi _{U}\webleft (x\webright )\odot \xi \webleft (\chi _{X}\webleft (x\webright )\webright )\webright )\\ & = \webleft (\bigvee _{x\in U}\xi \webleft (\chi _{X}\webleft (x\webright )\webright )\webright )\vee \webleft (\bigvee _{x\in X\setminus U}\varnothing _{Y}\webright )\\ & = \bigvee _{x\in U}\xi \webleft (\chi _{X}\webleft (x\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle (\dagger )}}{=}}}\xi \webleft (\bigvee _{x\in U}\chi _{X}\webleft (x\webright )\webright )\\ & = \xi \webleft (U\webright )\end{align*}

  for each $U\in \mathcal{P}\webleft (X\webright )$, where we have used that $\xi $ is cocontinuous for the equality $\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle (\dagger )}}{=}}}$.
• Invertibility II. We claim that
  \[ \Phi _{X,Y}\circ \Psi _{X,Y}=\text{id}_{\mathsf{Sets}\webleft (X,Y\webright )}. \]

  Indeed, given a function $f\colon X\to Y$, 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}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{clm}}}{=}}}f,\end{align*}

  where indeed

  \begin{align*} \webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\circ \chi _{X}\webright ]\webleft (x\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigvee _{y\in X}\chi _{\webleft\{ x\webright\} }\webleft (y\webright )\odot f\webleft (y\webright )\\ & = \webleft (\chi _{\webleft\{ x\webright\} }\webleft (x\webright )\odot f\webleft (x\webright )\webright )\vee \webleft (\bigvee _{y\in X\setminus \webleft\{ x\webright\} }\chi _{\webleft\{ x\webright\} }\webleft (y\webright )\odot f\webleft (y\webright )\webright )\\ & = f\webleft (x\webright )\vee \webleft (\bigvee _{y\in X\setminus \webleft\{ x\webright\} }\varnothing _{Y}\webright )\\ & = f\webleft (x\webright )\vee \varnothing _{Y}\\ & = f\webleft (x\webright )\end{align*}

  for each $x\in X$.

• Naturality for $\Phi $, Part I. We need to show that, given a function $f\colon X\to X'$, the diagram
  

  commutes. Indeed, given a cocontinuous morphism of posets

  \[ \xi \colon \webleft (\mathcal{P}\webleft (X'\webright ),\subset \webright )\to \webleft (Y,\preceq \webright ), \]

  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*}

  where we have used Item 9 of Proposition 2.4.1.1.3 for the equality $\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle (\dagger )}}{=}}}$ 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, given a cocontinuous morphism of posets

  \[ \xi \colon \webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )\to \webleft (Y,\preceq \webright ), \]

  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*}

• 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 8: Categories, Item 2 of Proposition 8.8.6.1.2 that $\Psi $ is also natural in each argument.