nLab finitely complete category



Category theory

Limits and colimits



A finitely complete category is a category CC which admits all finite limits, that is all limits for any diagrams F:JCF: J \to C with JJ a finite category. Finitely complete categories are also called lex categories. They are also called (at least by Johnstone in the Elephant) cartesian categories, although this term more often means a cartesian monoidal category.

Small finitely complete categories form a 2-category, Lex.


There are several well known reductions of this concept to classes of special limits. For example, a category is finitely complete if and only if:

An appropriate notion of morphism between finitely complete categories CC, DD is a left exact functor, or a functor that preserves finite limits (also called a lex functor, a cartesian functor, or a finitely continuous functor). A functor preserves finite limits if and only if:

  • it preserves terminal objects, binary products, and equalizers;
  • it preserves terminal objects, fibers, and binary products;
  • it preserves terminal objects and binary pullbacks.

Since these conditions frequently come up individually, it may be worthwhile listing them separately:

  • F:CDF: C \to D preserves terminal objects if F(t C)F(t_C) is terminal in DD whenever t Ct_C is terminal in CC;

  • F:CDF: C \to D preserves binary products if the pair of maps

    F(c)F(π 1)F(c×d)F(π 2)F(d)F(c) \stackrel{F(\pi_1)}{\leftarrow} F(c \times d) \stackrel{F(\pi_2)}{\to} F(d)

    exhibits F(c×d)F(c \times d) as a product of F(c)F(c) and F(d)F(d), where π 1:c×dc\pi_1: c \times d \to c and π 2:c×dd\pi_2: c \times d \to d are the product projections in CC;

  • F:CDF: C \to D preserves equalizers if the map

    F(i):F(e)F(c)F(i): F(e) \to F(c)

    is the equalizer of F(f),F(g):F(c)F(d)F(f), F(g): F(c) \stackrel{\to}{\to} F(d), whenever i:eci: e \to c is the equalizer of f,g:cdf, g: c \stackrel{\to}{\to} d in CC.


In any finitely complete category, the kernel pair of the identity morphism idid on an object XX is the diagonal morphism (id,id)(id,id) of XX and has a coequalizer isomorphic to XX itself.

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus


Section A1.2 in

Last revised on November 16, 2022 at 06:08:06. See the history of this page for a list of all contributions to it.