"new foundations must give new math"

from "The Basic Picture. Structures for constructive topology"

by Giovanni Sambin, Oxford University Press, forthcoming

Registration

To register send an e-mail to maietti @ math.unipd.it

Registration fee: 40 euros
(to be paid at arrival).

Under the patronage of

Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Italy

University of Padova, Italy

AILA (Italian Association of Logic and Applications), whose first president was Giovanni Sambin (from 1987 to 1994).

Abstracts » Vickers

Steve Vickers
Birmingham

On the trail of the Formal Topos

Grothendieck said the topos was more important than the site, and in a sense this encapsulates the difference between impredicative locales and predicative formal topology.

In the "propositional" case where the site is on a poset rather than a more general category, it is unnecessary to work with the full topos (of sheaves) because the frame (of opens) already contains enough information.

The locale theorist follows the Grothendieck view by favouring the frame, but the predicative mathematician is reluctant to do this - the frame is impredicative - and so in effect stays with the site as the formal topology.

But what about the general site? It might seem natural to study this in predicative mathematics as a "Formal Topos".

I shall describe some sightings of this elusive creature (for example: spaces of algebras and the symmetric topos) and some clues to its whereabouts and habits.

The impredicative treatment, using toposes and frames, is naturally easier and now comprises a large body of established results.
The predicative need always to work concretely with generators and relations (which is what the site in effect provides) is an extra layer of difficulty.

I shall survey some experiences of extracting predicative content from the impredicative results, in particular through the notions of bundle and geometricity. (By "bundle" I just mean continuous map, but with the suggestion that the dependence of fibre on base point gives the map a flavour of "variable space". By a key result that goes back to Joyal/Tierney and earlier, localic bundles correspond to conducting frame theory internally in a topos.)

I shall also suggest how abstract categorical accounts of "categories of spaces" (e.g. Townsend, Taylor) provide signposts.