Why point-free topology is more general than standard topology: an
embedding of concrete spaces into positive topologies
Giovanni Sambin (Univ. of Padova)



The aim of this talk is to offer a panoramic view  on some recent developments in constructive topology, stressing in particular on those structures and insights which are new also for a classical mathematician.

One of the motivations for point-free topology is that many properties of topological spaces depend only on the algebraic structure of open subsets, called a locale. The fundamental link with standard topology (with points) is given by a categorical adjunction between topological spaces and locales.

We show that this adjunction can be refined into an embedding, provided that topological spaces are replaced with "concrete spaces" and locales with "positive topologies". We thus can give a mathematical expression to the original and  deeper motivation for point-free topology, namely the claim that it is is more general than topology with points.

The notion of a concrete space is reached from that of a topological space by always requiring to have a basis indexed by a set, called the set of observables. Then it is natural to pass from continuous functions to continuous relations (set-valued mappings) with a suitable equality. One thus obtains a structural characterization of continuity, namely as commutativity of a square of relations.

The link between points and observables shows that interior and closure of a subset are defined by logically dual formulas, which only classically reduce to complementation. Positive topologies are the abstraction of the structure induced by a concrete space on the set of observables. Contrary to locales, they include a primitive pointfree treatment of closed subsets.

All these technical novelties have been induced by the constructive approach. The systematic presence of bases is necessary in a predicative foundation  (no powerset axiom) and the distinction between closed and complement of open is due to intuitionistic logic (no law of excluded middle).  Constructively,  the point-free approach becomes necessary, rather than just more general, since in most examples of spaces the collection of points is not a set predicatively. Thus spaces are obtained constructively as the collection of ideal points, that is, suitable subsets of observables in a positive topology.