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 )$, where the maps witnessing this bijection are given by

• The map
  \[ \chi ^{*}_{X} \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 ) \]

  defined by

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

  i.e. by sending a cocontinuous morphism of posets $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{Pos}^{\mathsf{cocomp.}}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (Y,\preceq \webright )\webright ) \]

  is given by sending a function $f\colon X\to Y$ to its left Kan extension along $\chi _{X}$,

  
  Moreover, $\text{Lan}_{\chi _{X}}\webleft (f\webright )$ can be explicitly computed by

  $\displaystyle \webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright ) \cong \int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )$

  $\displaystyle \phantom{\webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright )} \cong \rlap {\int ^{x\in X}\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )}\phantom{\int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )}$

  (by Proposition 2.4.2.1.1)

  $\displaystyle \phantom{\webleft [\text{Lan}_{\chi _{X}}\webleft (f\webright )\webright ]\webleft (U\webright )} \cong \rlap {\bigvee _{x\in X}\webleft (\chi _{U}\webleft (x\webright )\odot f\webleft (x\webright )\webright )}\phantom{\int ^{x\in X}\chi _{\mathcal{P}\webleft (X\webright )}\webleft (\chi _{x},U\webright )\odot f\webleft (x\webright )}$

  for each $U\in \mathcal{P}\webleft (X\webright )$, where:

  • $\bigvee $ is the join in $\webleft (Y,\preceq \webright )$.
  • 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 minimal element of $\webleft (Y,\preceq \webright )$.