A finitely complete category (which the Elephant calls a cartesian 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.
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 $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:
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
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
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$.
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.
cartesian category, cartesian functor, cartesian logic, cartesian theory
regular category, regular functor, regular logic, regular theory, regular coverage, regular topos
coherent category, coherent functor, coherent logic, coherent theory, coherent coverage, coherent topos
geometric category, geometric functor, geometric logic, geometric theory
Section A1.2 in
Last revised on June 12, 2021 at 16:20:59. See the history of this page for a list of all contributions to it.