point of a locale

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

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

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

Revised on April 14, 2017 10:07:19 by Toby Bartels (