Separating families of locale maps and localic embeddings (Q412005)

The aim of this nice short paper is to give a pointfree counterpart, in the category of locales and locale maps, of the topological concept of separating points from closed sets by continuous maps. For that, the authors establish the notion of a separating family of locale maps. Using this new localic concept, they provide the pointfree analogue of the general topological embedding (or diagonal) theorem. Three well-known embedding theorems (for arbitrary locales, zero-dimensional locales, and completely regular locales) are given as corollaries. Up to this point, all the proofs in the paper are constructively valid (in the usual sense of topos theory). Next, now making use of the axiom of choice, the authors show that their general embedding theorem allows to control the number of factors of the target localic products, which depends on the weight of the embeddable locale. In particular, they show that each completely regular locale \(L\) is embeddable into \(\omega(L)\) copies of the localic unit interval (where \(\omega(L)\) is the weight of \(L\)).