An exercise from Leinster:
Here is my attempt. Let $\hat f:\mathscr P(K)\to\mathscr P(L)$ be the function given by $\hat f(T)=\{y\in L:y=f(x)\text{ for some }x\in T\}$. Note that $\hat f$ is order preserving. We find left and right adjoints below.
(1.) Let's find a right adjoint. This must be an order preserving function $G:\mathscr P(K)\to \mathscr P(L)$ such that $$\mathscr P(K)(f^\ast(l),k)\cong\mathscr P(L)(l,G(k)).$$
This means the following:
$$f^\ast(l)\subseteq k \text{ iff } l\subseteq G(k)$$
or
$$\{x\in K: f(x)\in l\}\subseteq k \text{ iff } l\subseteq G(k)$$
If $G=\hat f$, then the above holds.
(2.) Let's find a left adjoint. This is an order preserving function $F:\mathscr P(K)\to\mathscr P(L)$ such that
$$\mathscr P(L)(F(k),l)\cong \mathscr P(K)(k, f^\ast(l))$$ i.e.
$$F(k)\subseteq l\text{ iff } k\subseteq \{x\in K: f(x)\in l\}$$
And again we can take $F=\hat f$.
Are the above arguments correct?
Do I also need to verify the naturality conditions below in each case? I'm asking because they state that two arrows are equal, but in a poset category any two arrows between same objects are automatically equal.


(2) holds: with $F=\hat f$, if $\hat f(k)\subseteq l$, then $$k\ \subseteq\ f^{-1}(\hat f(k))\ \subseteq\ f^{-1}(l)$$ and conversely, if $k\subseteq f^{-1}(l)$, then $\hat f(k)\ \subseteq\ \hat f(f^{-1}(l))\ \subseteq\ l$.
For (1), however, you need another functor. Define $$G(k):=\{y\in L: f^{-1}(y)\subseteq k\}$$ Note that if $f$ is not surjective, every $G(k)$ contains $L\setminus \hat f(K)$.
Note also that, we basically changed the quantifier inside the definition, so that now $y$ is required to satisfy that all of its preimages lie in $k$.
Try to prove the equivalences of the respective inclusions.
(3) For the naturality part, you're absolutely right: in a poset category every square commutes.