Exact completions and small sheaves
arXiv:1203.4318
Abstract
We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal k. A k-ary exact category is an exact category with disjoint and universal k-small coproducts, and a k-ary site is a site whose covering sieves are generated by k-small families and which satisfies a weak size condition. For different values of k, this includes the exact completions of a regular category or a category with (weak) finite limits; the pretopos completion of a coherent category; and the category of sheaves on a small site. For a large site with k the size of the universe, it gives a well-behaved "category of small sheaves". Along the way, we define a slightly generalized notion of "morphism of sites", and show that k-ary sites are equivalent to a type of "enhanced allegory".
v2: 77 pages; added discussion of postulated and lex colimits; final version, has appeared in TAC
References in corpus (7)
- Higher Topos Theory
- Limits of small functors
- Higher gauge theory I: 2-Bundles
- Derived Algebraic Geometry V: Structured Spaces
- Enhanced 2-categories and limits for lax morphisms
- Internal categories, anafunctors and localisations
- Idempotent splittings, colimit completion, and weak aspects of the theory of monads
Cited by in corpus (13)
- Enriched indexed categories
- A fibrational study of realizability toposes
- Temporal Type Theory: A topos-theoretic approach to systems and behavior
- (Almost) C*-algebras as sheaves with self-action
- Enriched categories as a free cocompletion
- Denseness conditions, morphisms and equivalences of toposes
- Topos and Stacks of Deep Neural Networks
- Fibrations of predicates and bicategories of relations
- Scheme representation for first-order logic
- Borel and analytic sets in locales
- Relative monadicity
- Gabriel-Ulmer duality for topoi and its relation with site presentations
- Formulating Categorical Concepts using Classes