10 - Stone duality

Summary

We introduce a fundamental duality that arises in topology from the consideration of points versus open sets. A lot of work in topology can be done by working at the level of open sets only. This subject is called the pointless topology, and can be studied in [Joh82]. It leads generally to formulations and proofs of a more constructive nature than the ones ‘with points’. For the purpose of computer science, this duality is quite suggestive: points correspond to programs, and open sets to program properties. The investigation of Stone duality for domains has been pioneered by Martin-Löf [ML83] and by Smyth [Smy83b]. The work on intersection types, particularly in relation with the D^∞ models, as exposed in chapter 3, appears as an even earlier precursor. We also recommend [Vic89], which offers a computer science oriented introduction to Stone duality.

In section 10.1, we introduce locales, and Stone duality in its most abstract form. In sections 10.2 and 10.4, we specialize the construction to various categories of dcpo's and continuous functions, most notably those of Scott domains and of profinite dcpo's (cf. definition 5.2.2). On the way, in section 10.3, we prove Stone's theorem: every Boolean algebra is order-isomorphic to an algebra of subsets of some set X, closed under set theoretical intersection, union, and complementation. The proof of Stone's theorem involves a form of the axiom of choice (Zorn's lemma), used in the proof of an important technical lemma known as Scott open filter theorem.