Locales as "topology-free spaces"

[categories <cat-dist@mta.ca>]

Date: Fri, 21 Feb 1997 11:34:36 +0000
From: Steve Vickers <sjv@doc.ic.ac.uk>

I am making two papers available as Departmental Research Reports:

   "Topical Categories of Domains"
   "Localic Completion of Quasimetric Spaces"

Both explore the idea of locales (and, indeed, toposes) as "topology-free
spaces". The technique is to work not with frames (point-free topologies)
but with presentations of them, understood as propositional geometric
theories whose models are the points. (But it is normally more convenient
to work with equivalent predicate theories.) Then -

*   the geometric theory already determines an implicit topology on its models;

*   any construction of models of one theory out of models of another
automatically determines a continuous map (or geometric morphism), just so
long as the construction is geometric.

In effect, a restriction to geometric mathematics removes the need to treat
topology explicitly, hence "topology-free spaces". Apparently, explicit
topology is needed to correct the over-credulousness of classical reasoning
principles, though in practice the geometric constraints often end up
forcing one to reintroduce the normal topological arguments in a different
guise.

The two papers test the applicability of the idea in the two areas of
domain theory and quasimetric spaces. Aside from the "topology-free space"
aspects, the papers develop some new results:

"Topical Categories of Domains" addresses categorical domain theory and
replaces the usual classes of objects and morphisms by toposes classifying
them. New general results concerning fixpoints of endo-geometric-morphisms
of toposes exploit their intrinsically topological nature to give a simple
approach to the solution of domain equations. The paper also gives a
summary of the constructive theory of Kuratowski finite sets and
establishes some limitations to the Cartesian closedness of Sets.

"Localic Completion of Quasimetric Spaces" proposes a construction of
locales in completion of quasimetric spaces (using ideas of flatness
deriving from Lawvere's enriched category account), studies the
powerlocales and shows that a limit map from a locale of Cauchy sequences
to the completion is triquotient in the sense of Plewe.

Paper copies are available from me; electronic copies are expected to be
available shortly in the Department of Computing's Research Report series
coordinated by Frank Kriwaczek (frk@doc.ic.ac.uk).

Steve Vickers.