nLab pretopos completion

Pretopos completion


Pretopos completion sends every coherent category into a pretopos, called its pretopos completion; the operation is idempotent. It is a “higher-ary” version of the exact completion of a regular category.

More generally, pretoposes form a full reflective sub-2-category of the 2-category of finitary sites, which in turn includes coherent categories (with their coherent topologies) as a full sub-2-category.

Relation to model theory

According to the observation of Mihály Makkai from around 1980, the pretopos completion of the syntactic category of a first-order theory corresponds to the operation TT eqT \mapsto T^{eq} invented by Saharon Shelah. T eqT^{eq} is a universal extension of TT which admits elimination of imaginaries.

Higher-ary versions

For any an arity class κ\kappa, there is a corresponding version of κ\kappa-pretopos completion; see (Shulman). The version for κ={1}\kappa = \{1\} is the exact completion, while classical pretopos completion is the version for κ=ω\kappa=\omega. The version for κ=\kappa= the size of the universe includes the topos of sheaves.


  • Panagis Karazeris, Notions of flatness relative to a Grothendieck topology,

  • Mike Shulman, “Exact completions and small sheaves”. Theory and Applications of Categories, Vol. 27, 2012, No. 7, pp 97-173. Free online

  • Mihály Makkai, G. E. Reyes, First order categorical logic, Lecture Notes in Math. 611, Springer 1977

  • David Ballard, William Boshuck, Definability and descent, The Journal of Symbolic Logic 63:2 (Jun., 1998), pp. 372-378, jstor

  • Victor Harnik, Model theory vs. categorical logic: two approaches to pretopos completion (a.k.a. T eqT^{eq}), in: Models, logics, and higher-dimensional categories, 79–106 (Makkai volume), CRM Proc. Lecture Notes 53, Amer. Math. Soc. 2011; gBooks

  • Saharon Shelah, Classification theory and the number of non-isomorphic models, Studies in Logic and the Foundations of Mathematics 92, North Holland, Amsterdam 1978

Last revised on September 6, 2012 at 20:06:11. See the history of this page for a list of all contributions to it.