Why point-free topology is more general than standard topology: an
embedding of concrete spaces into positive topologies
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
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.