Topological Representation of Geometric Theories

TL;DR

This paper develops a topological groupoid-based duality framework for geometric theories, linking syntax and semantics through a topological representation of models and classifying toposes.

Contribution

It introduces a new duality between geometric theories with enough models and topological groupoids, extending previous syntax-semantics dualities to arbitrary geometric theories.

Findings

Constructs a topological groupoid representation of models and isomorphisms.

Establishes a contravariant adjunction and equivalence between theories and groupoids.

Simplifies the construction of the duality using slice constructions and intrinsic characterizations.

Abstract

Using Butz and Moerdijk's topological groupoid representation of a topos with enough points, a `syntax-semantics' duality for geometric theories is constructed. The emphasis is on a logical presentation, starting with a description of the semantical topological groupoid of models and isomorphisms of a theory and a direct proof that this groupoid represents its classifying topos. Using this representation, a contravariant adjunction is constructed between theories and topological groupoids. The restriction of this adjunction yields a contravariant equivalence between theories with enough models and semantical groupoids. Technically a variant of the syntax-semantics duality constructed in [Awodey and Forssell, arXiv:1008.3145v1] for first-order logic, the construction here works for arbitrary geometric theories and uses a slice construction on the side of groupoids---reflecting the use of `indexed' models in the representation theorem---which in several respects simplifies the construction and allows for an intrinsic characterization of the semantic side.