STONE-•2ECH COMPACTIFICATION OF LOCALES I

This paper shows that the compact regular locales on the one hand, and the compact completely regular locales on the other, are reflective in the category of all locales by identifying these reflections for each locale L as a,xV-sublattice of the ideal lattice of L. The arguments involved in this are constructive, making them valid in any topos having a natural numbers object. Note that the consideration of locales rather than topological spaces is natural in a constructive context ' even the locale of real numbers may fail to be a topological space. In addition, a proof is included giving the characterization, implicit in Isbell [6], of the topologies of compact Hausdorff spaces as the compact regular locales, by which the reflections considered here are seen to extend the familiar Stone-•ech compactification f topological spaces. Thanks are due to Peter Johnstone for drawing our attention to Isbell [6] and for alerting us to the possibility of a difference between colnpact regular and compact completely regular locales. Also, financial assistance from the National Science and Engineering Research Council of Canada is gratefully acknowledged. Recall that a locale ( = complete Brouwerian lattice, local lattice, frame, complete Heyting algebra) is a complete lattice L satisfying the distribution law x ^VA = Vx ^ a (a G A) for any x G L and A C _ L, where ̂ andV have the usual meaning of meet and join. Of particular interest here will be the relation x <:I z (read ' x is rather below z) defined on any locale L, with zero 0andunite, tomeanthat x ^ y=0and z v y = e for some y G L or, equivalently, z v x * = e for the pseudocomplement x * = Vy(x ^ y = 0) of x. We call a locale L regular iff x =Vz(z <::1 x) for all x G L. A fi'lter F in a locale L is a subset of L such that]•E G F for all finite E C _ F (and hence F•O) and x> • z andz GF implies xG F. A prime filter Pisa filter such that, for any finite subset EC _ L,V E G P implies that x • P for some x G E, and a completely prime filter is a filter satisfying this condition for all subsets E C L