Left Exact Functor

A functor $F:\mathcal{C}\to\mathcal{D}$ is left exact if it preserves all Finite Limits.

Properties

A functor $F:\mathcal{C}\to\mathcal{D}$ between Finitely Complete Categories is left exact if and only if the Comma Category $d\downarrow F$ is Cofiltered for all $d:\mathcal{D}$.

Explicitly, this means that for all $d:\mathcal{D}$:

• There merely exists a $c:\mathcal{C}$ and $\mathcal{D}(d,F(c))$.
• For any $(c_{1}:\mathcal{C},f:\mathcal{D}(d,F(c_{1})))$, $(c_{2},g:\mathcal{D}(d,F(c_{2})))$, there merely exists a $(c_{3},h:\mathcal{D}(d,F(c_{3})))$, $k_{1}:\mathcal{C}(c_{3},c_{1})$, $k_{2}:\mathcal{C}(c_{3},c_{2})$ with $f=F(k_{1})h$, $g=F(k_{2})h$.
• TODO: Fill in the equaliser condition.