## Sketches for arithmetic universesAdd 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:Note that ex-directory lists are not shown. |
## Other listsBham Talks Nanoscale Physics Seminars Midlands Logic Seminar## Other talksRole of Mechanics and Geometry in Cellular Information Processing School Seminar Verification of Byzantine Fault Tolerant Systems How hard is LWE anyway? RSC S F Boys-A Rahman Award Lecture An attack on ECDSA using lattice techniques |