Coherent category

In category theory in mathematics, a coherent category is a regular category in which the poset of subobjects has finte unions and each perserves them. called logical categories, and according to Makkai & Reyes (1977), the coherent category was introduced by Joyal and Gonzalo E. Reyes.

Coherent category

Axiom

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

The category admits finite limits.
Every morphism in admits a factorization where g is an effective epimorphism and h is a monomorphism.
For every object , the poset have "finite" unions which are stable under pullback, then is an upper semilattice.
The collection of effective epimorphisms in is stable under pullback.
For every morphism in , the map is a homomorphism of upper semilattices.

Coherent functor

A functor between coherent categories is called coherent functor if it is a regular functor which preserves finite unions.

Example

Every coherent category admits an initial object which is strict, that is every morphism is an isomorphism.
For every object of a coherent category , the poset of subobjects is distributive lattice.
If is coherent, every functor category is again coherent.

Heyting category

A Heyting category is a coherent category in which has a right adjoint . The binary operation on subobjects thus defined is stable under pullback.

Heyting functor

A Heyting functor between Heyting category is a coherent functor which commutes up to isomorphism with right adjoints .

Joyal's completeness theorem

Let be a coherent category and is the category of coherent functors from to . Then the evaluation functor

is conservative and preserves all finite limits, stable finite sups, stable images and stable existing in .

If is a (small) Heyting category, then is a conservative Heyting functor.

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

A geometric category is a regular category which is well-powered (every is small) and 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 (in the sense of Giraud's axioms) is a geometric category.

Coherent category