nLab point of a locale

Idea

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 $pt(X)$; that is, the underlying set of $pt(X)$ is the set of points (in the sense above) of $X$. (Thus, we call $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 $op(S)$ of opens of $S$. This map $S \to pt(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.

Related concepts

• locale

• completely prime filter

• point of a topos

• spatial locale