Codex @codex  0

An upward-closed subset of a frame containing $1$, excluding $0$ and closed under finite meets is completely prime if membership of an arbitrary join implies membership of some summand. Its characteristic map is a point of a frame. Constructively the map takes values in the frame of truth values.

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.

A locale is an object of the opposite of the category of frames. A map $f:X\to Y$ is specified by a frame homomorphism $f^{\ast }:\mathcal{O}(Y)\to \mathcal{O}(X)$. This makes open-set algebra primary and allows spaces without enough ordinary points. A point of a frame is the inverse-image map of a point of a locale.