= Frame-point adjunction
{title2=$O:\mathbf{Top}\rightleftarrows\mathbf{Frm}^{\mathrm{op}}:P,\quad O\dashv P$}
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\mapsto1_{\{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>.
Back to article page
