nLab finitely complete category

Definition

A finitely complete category is a category $C$ which admits all finite limits, that is all limits for any diagrams $F: J \to C$ with $J$ 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.

Variants

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:

• It has a terminal object and admits all binary products and equalizers;
• It has a terminal object and admits all fibers and binary products;
• It has a terminal object and admits all binary pullbacks.

An appropriate notion of morphism between finitely complete categories $C$, $D$ 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: C \to D$ preserves terminal objects if $F(t_C)$ is terminal in $D$ whenever $t_C$ is terminal in $C$;

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

  $$F(c) \stackrel{F(\pi_1)}{\leftarrow} F(c \times d) \stackrel{F(\pi_2)}{\to} F(d)$$

  exhibits $F(c \times d)$ as a product of $F(c)$ and $F(d)$, where $\pi_1: c \times d \to c$ and $\pi_2: c \times d \to d$ are the product projections in $C$;

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

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

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

Properties

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

Related concepts

• locally cartesian category

• finitely complete (infinity,1)-category

category	functor	internal logic	theory	hyperdoctrine	subobject poset	coverage	classifying topos
finitely complete category	cartesian functor	cartesian logic	essentially algebraic theory
lextensive category		disjunctive logic
regular category	regular functor	regular logic	regular theory	regular hyperdoctrine	infimum-semilattice	regular coverage	regular topos
coherent category	coherent functor	coherent logic	coherent theory	coherent hyperdoctrine	distributive lattice	coherent coverage	coherent topos
geometric category	geometric functor	geometric logic	geometric theory	geometric hyperdoctrine	frame	geometric coverage	Grothendieck topos
Heyting category	Heyting functor	intuitionistic first-order logic	intuitionistic first-order theory	first-order hyperdoctrine	Heyting algebra
De Morgan Heyting category		intuitionistic first-order logic with weak excluded middle			De Morgan Heyting algebra
Boolean category		classical first-order logic	classical first-order theory	Boolean hyperdoctrine	Boolean algebra
star-autonomous category		multiplicative classical linear logic
symmetric monoidal closed category		multiplicative intuitionistic linear logic
cartesian monoidal category		fragment $\{\&, \top\}$ of linear logic
cocartesian monoidal category		fragment $\{\oplus, 0\}$ of linear logic
cartesian closed category		simply typed lambda calculus

References

Section A1.2 in

• Peter Johnstone, Sketches of an Elephant