Draft:Coherent category

In category theory, a coherent category is a regular category in which the poset of subobjects $\mathrm{S}\mathrm{u}\mathrm{b}(X)$ has finte unions and each $f^{*}:\mathrm{S}\mathrm{u}\mathrm{b}(B)\to \mathrm{S}\mathrm{u}\mathrm{b}(A)$ perserves them.

Definition

Let $𝒞$ be a category. We will say that $𝒞$ is coherent category if it satisfies the following axioms:

• The category $𝒞$ admits finite limits.
• Every morphism $f:X\to Z$ in $𝒞$ admits a factorization $X\stackrel{g}{⟶}Y\stackrel{h}{⟶}Z$ where g is an effective epimorphism and h is a monomorphism.
• For every object $X\in 𝒞$, the poset $\mathrm{S}\mathrm{u}\mathrm{b}(X)$ have "finite" unions which are stable under pullback, then $\mathrm{S}\mathrm{u}\mathrm{b}(X)$ is an upper semilattice.
• The collection of effective epimorphisms in $𝒞$ is stable under pullback.
• For every morphism $f:X\to Y$ in $𝒞$, the map $f^{-1}:\mathrm{S}\mathrm{u}\mathrm{b}(Y)\to \mathrm{S}\mathrm{u}\mathrm{b}(X)$ is a homomorphism of upper semilattices.

Coherent functor

A functor $f:𝒞\to 𝒟$ between coherent categories is called coherent functor if it is a regular functor which preserves finite unions.

Heyting category

A Heyting category is a coherent category $𝒞$ in which $f^{*}:\mathrm{S}\mathrm{u}\mathrm{b}(B)\to \mathrm{S}\mathrm{u}\mathrm{b}(A)$ has a right adjoint ${\mathrm{\forall }}_f:\mathrm{S}\mathrm{u}\mathrm{b}(A)\to \mathrm{S}\mathrm{u}\mathrm{b}(B)$. The binary operation on subobjects thus defined is stable under pullback.

Joyal's completeness theorem

Let $𝒜$ be a coherent category. Then the evaluation functor

$𝒜\stackrel{ev}{⟶}{\mathrm{S}\mathrm{e}\mathrm{t}\mathrm{s}}^{\mathrm{M}\mathrm{o}\mathrm{d}(𝒜)}$

is faithful, coherent and conditionally Heyting.

Geometric category (a.k.a. Infinitary coherent category)

A geometric category is a regular category which is well-powered (every $\mathrm{S}\mathrm{u}\mathrm{b}(X)$ is small) and $\mathrm{S}\mathrm{u}\mathrm{b}(X)$ have all unions which are stable under pullback. A geometric category is Heyting category by the adjoint functor theorem for posets. Also, every Grothendieck topos is a geometric category.