nLab
point of a locale

A point of a locale $X$ is a continuous map (in the sense of locales) to $X$ from the abstract point (seen as a locale whose corresponding frame is the frame of truth values).

If $X^{*}$ is the frame that corresponds to $X$, then a point of $X$ is the same as a frame homomorphism from $X^{*}$ to the frame of truth values. This is the same as a completely prime filter in $X^{*}$.

A point of $X$ is the same as a point (in the usual sense) of the topological space $\mathrm{pt}(X)$; that is, the underlying set of $\mathrm{pt}(X)$ is the set of points (in the sense above) of $X$. (Thus, we call $\mathrm{pt}(X)$ the space of points of $X$.) Conversely, if $S$ is a topological space, then every point of $S$ determines a point of the locale $\mathrm{op}(S)$ of opens of $S$. This map $S\to \mathrm{pt}(\mathrm{op}(S))$ (which is a continuous map of topological spaces) is injective iff $S$ is $T_0$ (see separation axioms); it is a homeomorphism iff $S$ is sober.