University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Oxford Quantum Talks Archive

Locales via bundles

Steve Vickers, Imperial College London
Categories, Logic and Foundations of Physics III, August 2008, University of Oxford

Locale theory, a "point-free" approach to topology, can be understood as viewing topological spaces as the spaces of models for logical theories of a particular kind. It has been found effective in a variety of fields, including pure mathematics (deriving from algebraic geometry) and computer science (notably in Abramsky's thesis). One of its most compelling virtues is that it interacts well with constructive mathematics, including the internal mathematics of toposes. In fact, it has a more satisfactory body of constructively valid results than does ordinary point-set topology. Locales have also appeared in the topos approaches to quantum mechanics of Isham and Doering at Imperial and (more explictly) of Heunen, Landsman and Spitters at Nijmegen. Locales have been motivated in a variety of ways, but the path to the constructive virtues can be long and stony. I shall outline a conceptual development in terms of bundles, and going back to a technical result described by Joyal and Tierney in 1984 and known even earlier. Essentially it says that bundles over a space X are equivalent to topological spaces in the internal mathematics of "bundles of sets" (local homeomorphisms) over X. This fits an intuition that "bundle" means a space (the fibre) parametrized by points of the base space. However, there are simple examples to show that this cannot work with a point-set approach to topology - essentially because arbitrary bundles cannot be approximated closely enough by local homeomorphisms. Instead, spaces must be replaced by locales. A key notion is that of "geometric" reasoning, preserved under pullback of bundles, that is more restricted than topos-valid reasoning. It is hoped that the topos-internal reasoning of the Imperial and Nijmegen groups, insofar as it is geometric, can be expressed more intuitively as fibrewise reasoning for bundles.

[video] [streaming video]