∞-ary regular and exact categories
arity class: unary, finitary, infinitary
regularity
regular category = unary regular
coherent category = finitary regular
geometric category = infinitary regular
exactness
exact category = unary exact
An infinitary coherent category or geometric category is a regular category in which the subobject posets have all small unions which are stable under pullback.
More generally, for a regular cardinal, a -geometric category, or -coherent category, is a regular category with unions for -small families of subobjects, stable under pullback. (For this reduces to the notion of coherent category, called a pre-logos by Freyd–Scedrov.)
Makkai-Reyes call this a -logical category, while Shulman calls it a -ary regular category. See also (Butz-Johnstone, p. 12).
See familial regularity and exactness for a general description of the spectrum from regular categories through finitary and infinitary coherent categories.
Frequently, geometric categories are additionally required to be well-powered. If a geometric category is well-powered, then its subobject posets are complete lattices, hence also have all intersections. Moreover, by the adjoint functor theorem for posets, it is a Heyting category.
However, since geometric logic does not include implication or infinite conjunction, this categorical structure should not necessarily be expected to exist in a category called “geometric” (and when they do exist, they are not preserved by geometric functors). A requirement of well-poweredness is also inconsistent with the spectrum of familial regularity and exactness.
Note, however, that if a geometric category has a small generating set, then it is necessarily well-powered. In particular, this applies to the syntactic category of any (small) geometric theory, and also to any Grothendieck topos.
Around lemma A1.4.18 in
Michael Makkai, Gonzalo Reyes, First Order Categorical Logic, Lecture Notes in Math. 611 (Springer-Verlag, 1977).
Last revised on November 16, 2022 at 05:59:31. See the history of this page for a list of all contributions to it.