nLab
complete small category

Context

Category theory

Limits and colimits

Complete small categories

Definition

A complete small category (or small complete category) is a category which is both small (has only a set of objects and morphisms) and complete (has a limit of every small diagram).

(Note that the phrase “small-complete category” is sometimes used to mean merely a complete category, i.e. one which is “complete relative to small diagrams”. Therefore, “complete small category” is a safer term for our concept.)

In classical logic

In the presence of classical logic, complete small categories reduce to complete lattices by the following theorem of Freyd.

Theorem

If (in some universe UU) a small category DD has products of families of objects whose size is at least that of its set of morphisms, then DD is a preorder. In particular, any complete small category is a preorder.

Proof

Let xx, yy be any two objects, and suppose (contrary to DD being a preorder) that there are at least two different morphisms xsryx \,\underoverset{s}{r}{\rightrightarrows}\, y. Then the set of morphisms

x fMor(D)yx \to \prod_{f \in Mor(D)} y

has cardinality at least 2 Mor(D)>Mor(D)2^{|Mor(D)|} \gt {|Mor(D)|}, which is a contradiction.

In Grothendieck toposes

The internal logic of a topos is not, in general, classical, so the above proof does not apply when considering internal categories in a topos. However, in a Grothendieck topos, one can show that the conclusion still holds by essentially reducing the question to the analogous one in SetSet. A brief description of the argument can be found in the answer to this question.

In more general toposes and constructive mathematics

However, it is possible to have non-preorder complete small categories in non-Grothendieck topoi. In particular, the effective topos, along with most other realizability toposes, does contain such internal categories. These categories have applications to the modeling of impredicative type theory.

It follows that, in constructive mathematics, it is impossible to prove even that every complete small category in SetSet or in a Grothendieck topos must be a preorder.

Revised on September 10, 2011 17:18:19 by Mike Shulman (71.136.248.27)