Sketches for arithmetic universes

Add to your list(s) Download to your calendar using vCal

• Dr Steve Vickers (School of Computer Science, University of Birmingham)
• Wednesday 18 May 2016, 13:00-14:00
• CS 217.

If you have a question about this talk, please contact Uday Reddy.

Grothendieck says toposes are generalized topological spaces. Then any geometric theory T can be understood as a space, the points being the models of T, and then the topos is its classifying topos S[T]. A map from T_1 to T_2 is a geometric morphism from S[T_1] to S[T_2], and the universal property of classifying toposes says this is equivalent to a model of T_2 in S[T_1]. This means that, in the context of a generic model of T_1, and using the geometric maths of colimits and finite limits, we construct a model of T_2: hence to describe a map we use the points very explicitly, despite this being a point-free approach, and continuity relies on the geometricity of the construction.

In many ways that is a successful logical approach to topology, but it is hard to make a formal system for it because of the infinitary disjunctions and coproducts that are needed, for instance for real analysis. The available infinities are supplied externally as the objects of a chosen base topos S by which the whole programme is parameterized. Long ago I conjectured that Joyal’s Arithmetic Universes (AUs), pretoposes with parametrized list objects, might supply enough internal infinities (e.g. a natural numbers object) to be a finitary substitute, with no dependence on choice of base S, that is good enough in practice.

In this talk I outline a 2-category Con that is intended to be the category of generalized spaces in these AU terms. I have a first draft of a detailed paper that I am now polishing up for submission. Each object T describes a geometric theory, and presents by universal algebra an AU AU that stands in for S[T]. Con embeds fully and faithfully in the 2-category of AUs and strict AU-functors.

• I adapt the ideas of sketch theory to apply to AUs: principally, this introduces list objects. The category of sketches and sketch homomorphisms maps functorially to AUs, T |-> AU . This is not yet full or faithful – the homomorphisms are too syntax-bound.
• In general, sketches provide the ability to declare equality between objects in an undesirable way. I define “extensions” of sketches, in which limits, colimits and list objects are introduced fresh in a definitional way, and then “contexts”, extensions of the empty sketch. Any non-strict model of a context (these are needed for the semantics) has a unique isomorphism with a strict model (needed for the universal algebraic syntax).
• We now have a finitary category Con_hom of contexts and sketch homomorphisms.
• For a map from T_1 to T_2 we need to interpret T_2 in “stuff derived uniquely from T_1”. An “equivalence extension” of T_1 is an extension in which the new ingredients are already known to exist, and uniquely.
• “Object equalities” deal with the situation where the same construction is applied twice to the the same data, so the two copies are equal in any strict model.
• Con is a localization of (Con_hom)^op. It takes object equalities to actual equalities, and makes equivalence extensions invertible. It is entirely finitary.
• Con has finite pie-limits (product, inserter, equifier), and strict pullbacks of extension maps.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.