Localic Priestley duality Original Research Article

Given the category of ordered Stone spaces (as introduced by Priestley, 1970) and the category of coherent spaces (= spectral spaces) we can construct a pair of functors CohSp image OStoneSp between the categories. Priestley (1970) has shown, assuming the prime ideal theorem, that these define an equivalence. In this paper, we define ordered Stone locales. These are classically just the ordered Stone spaces. It is well known that the localic analogue of the coherent spaces is the category of coherent locales. We prove, entirely constructively, that the category of coherent locales is equivalent to the category of ordered Stone locales.