Stone duality

Stone-type dualities also provide the foundation for pointless topology and are exploited in theoretical computer science for the study of formal semantics.

This article gives pointers to special cases of Stone duality and explains a very general instance thereof in detail.

Now an obvious question is: To what extent is a topological space characterized by its locale of open sets?

Furthermore, it is easy to check that f −1 (like any inverse image map) preserves finite intersections and arbitrary unions and therefore is a morphism of frames.

However, there is still a reasonable technique for obtaining "points" from a locale, which indeed gives an example of a central construction for Stone-type duality theorems.

The open set lattice of the one-element topological space Ω(1) is just (isomorphic to) the two-element locale 2 = { 0, 1 } with 0 < 1.

Before defining the required topology on pt(X), it is worthwhile to clarify the concept of a point of a locale further.

From the properties of frame morphisms, one can derive that p −1(0) is a lower set (since p is monotone), which contains a greatest element ap = V p −1(0) (since p preserves arbitrary suprema).

This is done by defining the open sets of pt(L) as for every element a of L. Here we viewed the points of L as morphisms, but one can of course state a similar definition for all of the other equivalent characterizations.

At this point we already have more than enough data to obtain the desired result: the functors Ω and pt define an adjunction between the categories Top and Loc = Frmop, where pt is right adjoint to Ω and the natural transformations ψ and φop provide the required unit and counit, respectively.

Finally, one can verify that for every space X, Ω(X) is spatial and for every locale L, pt(L) is sober.

Hence, it follows that the above adjunction of Top and Loc restricts to an equivalence of the full subcategories Sob of sober spaces and SLoc of spatial locales.

The case of the functor Ω o pt is symmetric but a special name for this operation is not commonly used.