What is a point-free space? Or a point-free bundle?

Steve Vickers

Point-free spaces have been defined in various technical ways, including as frames (locales), as formal topologies, and even - these are "generalized spaces" - as toposes. What they have in common is that by the time you have set up the technical framework, you have lost sight of what the point was.

This is often misunderstood as the essence of point-free topology, and the temptation is great to revert to point-set spaces and work with honest points.

The problem with that comes when you look at bundles, understood as families of spaces (the fibres) continuously indexed by base point. Pleasant results from topos theory show that these are equivalent to spaces internal in the topos of sheaves over the base space, but only if you work point-free. Simple topological examples show that a point-set approach cannot work in general. (Technically: some bundles cannot be satisfactorily approximated by local homeomorphisms.)

I shall explain how geometric logic restores the pointwise reasoning, but without the problems of assuming a set of points. The points of a point-free space are the models of a geometric theory; maps between spaces are defined using geometric constructions (colimits and finite limits) of points; and bundles are built by geometrically constructing theories out of points.

This underlies Grothendieck's idea of toposes as generalized spaces, and I shall say something about how it leads to my current work using arithmetic universes to get constructive results that are independent of any choice of base topos.

For more details -

My 5 TACL 2017 talks http://www.cs.bham.ac.uk/~sjv/talks.php
"Sketches for arithmetic universes" http://www.cs.bham.ac.uk/~sjv/papersfull.php#AUSk
"Arithmetic universes and classifying toposes" (in Cahiers de topologie et géométrie différentielle catégorique) http://www.cs.bham.ac.uk/~sjv/papersfull.php#AUClTop