 Frame-point adjunction

There is a natural bijection between continuous maps $X\to P(A)$ and frame homomorphisms $A\to O(X)$. It sends $f$ to $a\mapsto f^{-1}(U_a)$; the inverse sends $x$ to the point $a\mapsto 1_{\{x\in h(a)\}}$. Its adjunction unit sends a point of $X$ to its open-neighbourhood membership map. The counit is represented by $a\mapsto U_a$. Every open of $P(A)$ is such a $U_a$, and every point of a frame $O(P(A))$ is uniquely evaluation at a point of $A$. Consequently $P(A)\to P(O(P(A)))$ is a homeomorphism, and this is an idempotent adjunction.