The over-topos at a model

TL;DR

This paper introduces the over-topos at a model, a new topos construction associated with a geometric theory in an arbitrary topos, generalizing colocalization and involving universal properties and bicategorical limits.

Contribution

It defines the over-topos at a model using a site with the antecedent topology, generalizes colocalization, and explores its geometric and 2-categorical properties.

Findings

Constructed the over-topos with a universal property.

Established the over-topos as a bilimit in the bicategory of toposes.

Provided a classification theory for models via the over-topos.

Abstract

With a model of a geometric theory in an arbitrary topos, we associate a site obtained by endowing a category of generalized elements of the model with a Grothendieck topology, which we call the antecedent topology. Then we show that the associated sheaf topos, which we call the over-topos at the given model, admits a canonical totally connected morphism to the given base topos and satisfies a universal property generalizing that of the colocalization of a topos at a point. We first treat the case of the base topos of sets, where global elements are sufficient to describe our site of definition; in this context, we also introduce a geometric theory classified by the over-topos, whose models can be identified with the model homomorphisms towards the (internalizations of the) model. Then we formulate and prove the general statement over an arbitrary topos, which involves the stack of generalized elements of the model. Lastly, we investigate the geometric and 2-categorical aspects of the over-topos construction, exhibiting it as a bilimit in the bicategory of Grothendieck toposes.