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 the presence of classical logic, complete small categories reduce to complete lattices by the following theorem of Freyd.
If (in some universe $U$) a small category $D$ has products of families of objects whose size is at least that of its set of morphisms, then $D$ is a preorder. In particular, any complete small category is a preorder.
Let $x$, $y$ be any two objects, and suppose (contrary to $D$ being a preorder) that there are at least two different morphisms $x \,\underoverset{s}{r}{\rightrightarrows}\, y$. Then the set of morphisms
has cardinality at least $2^{|Mor(D)|} \gt {|Mor(D)|}$, which is a contradiction.
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 $Set$. A brief description of the argument can be found in the answer to this question.
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 $Set$ or in a Grothendieck topos must be a preorder.
Last revised on September 10, 2011 at 17:18:19. See the history of this page for a list of all contributions to it.