Traditionally, a topological space consists of a set of points together with a topology, a system of subsets called open sets that with the operations of intersection and union forms a lattice with certain properties. Point-free topology is based on the concept of a "realistic spot" instead of a point without extent. Spots can be joined and if a spot meets a join of others it has to meet some of the constituents, which, roughly speaking, leads to the distributive law
Formally
The basic concept is that of a frame, a complete lattice satisfying the distributive law above; frame homomorphisms respect all joins and finite meets. Frames, together with frame homomorphisms, form a category.
In classical topology, represented on a set by the system of open sets, is a frame, and if is a continuous map, defined by is a frame homomorphism. For sober spaces such are precisely the frame homomorphisms. Hence is a full embedding of the category of sober spaces into the dual of the category of frames. This justifies thinking of frames as of generalized topological spaces. A frame is spatial if it is isomorphic to a. There are plenty of non-spatial ones and this fact turned out to be helpful in several problems.
The theory of frames and locales in the contemporary sense was initiated in the late 1950s and developed through the following decades into a lively branch of topology, with application in various fields, in particular also in theoretical computer science. For more on the history of locale theory see. It is possible to translate most concepts of point-set topology into the context of locales, and prove analogous theorems. Regarding the advantages of the point-free approach let uspoint out, for example, the fact that some important facts of classical topology depending on choice principles become choice-free. Thus for instance, products of compact locales are compact constructively, or completions of uniform locales are constructive. This can be useful if one works in a topos that does not have the axiom of choice. Other advantages include the much better behaviour of paracompactness, or the fact that subgroups of localic groups are always closed. Another point where locale theory and topology diverge strongly is the concepts of subspaces versus sublocales: by Isbell's density theorem, every locale has a smallest dense sublocale. This has absolutely no equivalent in the realm of topological spaces.
