Coherent category

Axiom

Let ${\displaystyle {\mathcal {C}}}$ be a category. We will say that ${\displaystyle {\mathcal {C}}}$ is coherent category if it satisfies the following axioms:^[4][5]

• The category ${\displaystyle {\mathcal {C}}}$ admits finite limits.
• Every morphism ${\displaystyle f:X\rightarrow Z}$ in ${\displaystyle {\mathcal {C}}}$ admits a factorization ${\displaystyle X\mathrel {\stackrel {g}{\longrightarrow }} Y\mathrel {\stackrel {h}{\longrightarrow }} Z}$ where g is an effective epimorphism^[6] and h is a monomorphism.
• For every object ${\displaystyle X\in {\mathcal {C}}}$, the poset ${\displaystyle \mathrm {Sub} (X)}$ have "finite" unions which are stable under pullback, then ${\displaystyle \mathrm {Sub} (X)}$ is an upper semilattice.
• The collection of effective epimorphisms in ${\displaystyle {\mathcal {C}}}$ is stable under pullback.
• For every morphism ${\displaystyle f:X\rightarrow Y}$ in ${\displaystyle {\mathcal {C}}}$, the map ${\displaystyle f^{-1}:\mathrm {Sub} (Y)\rightarrow \mathrm {Sub} (X)}$ is a homomorphism of upper semilattices.

Coherent functor

A functor ${\displaystyle f:{\mathcal {C}}\rightarrow {\mathcal {D}}}$ between coherent categories is called coherent functor if it is a regular functor which preserves finite unions.^[7]

Example

• Every coherent category admits an initial object ${\displaystyle 0}$ which is strict, that is every morphism ${\displaystyle X\rightarrow 0}$ is an isomorphism.^[8][9]
• For every object ${\displaystyle X}$ of a coherent category ${\displaystyle {\mathcal {C}}}$, the poset of subobjects ${\displaystyle \mathrm {Sub} (X)}$ is distributive lattice.^[10]
• If ${\displaystyle {\mathcal {C}}}$ is coherent, every functor category ${\displaystyle {\mathcal {C}}^{\mathcal {D}}}$ is again coherent.^[11]

Heyting functor

A Heyting functor between Heyting category is a coherent functor which commutes up to isomorphism with right adjoints ${\displaystyle \forall _{f}}$.^[14]

Joyal's completeness theorem

Let ${\displaystyle {\mathcal {A}}}$ be a coherent category and ${\displaystyle \mathrm {Mod} ({\mathcal {A}})}$ is the category of coherent functors from ${\displaystyle {\mathcal {A}}}$ to ${\displaystyle \mathrm {Sets} }$. Then the evaluation functor

${\displaystyle e_{\mathcal {A}}:{\mathcal {A}}\mathrel {\stackrel {ev}{\longrightarrow }} \mathrm {Sets} ^{\mathrm {Mod} ({\mathcal {A}})}}$

is conservative and preserves all finite limits, stable finite sups, stable images and stable ${\displaystyle \forall _{f}({\mathcal {A}})}$ existing in ${\displaystyle {\mathcal {A}}}$.^[15][16]

If ${\displaystyle {\mathcal {A}}}$ is a (small) Heyting category, then ${\displaystyle e_{\mathcal {A}}}$ is a conservative Heyting functor.^[17]