# nLab coherent category

### Context

#### Regular and Exact categories

κ-ary regular and exact categories

regularity

exactness

category theory

# Contents

## Definition

A coherent category (also called a pre-logos) is a regular category in which the subobject posets $Sub(X)$ all have finite unions which are preserved by the base change functors $f^*:Sub(Y)\to Sub(X)$.

A coherent functor serves as a morphism between coherent categories.

The internal logic of a coherent category is coherent logic.

An infinitary coherent category is a well-powered regular category in which the subobject posets $Sub(X)$ have all small unions which are stable under pullback. Infinitary coherent categories are also called geometric categories.

Mike Shulman: I’m starting to feel that well-poweredness shouldn’t be included here. Any thoughts?

See familial regularity and exactness for a general description of the spectrum from regular categories through finitary and infinitary coherent categories.

## Properties

### Extensivity

Any coherent category automatically has a strict initial object. Moreover, if an object $X$ is the union of two subobjects $A\hookrightarrow X$ and $B\hookrightarrow X$ such that $A\cap B = 0$, then $X = A\amalg B$ is their coproduct. Thus, if every pair of objects can be embedded disjointly in some third object, then a coherent category has disjoint finite coproducts and is extensive (or “positive”).

Extensivity is the analogue for coherent categories of exactness for regular categories. A coherent category which is both extensive and exact is called a pretopos.

### The coherent topology

Any coherent category $C$ admits a subcanonical Grothendieck topology in which the covering families are generated by finite, jointly regular-epimorphic families: the coherent coverage. Equivalently, they are generated by single regular epimorphisms and by finite unions of subobjects. If $C$ is extensive, then its coherent topology is generated by the regular topology together with the extensive topology. (In fact, the coherent topology is superextensive.)

If $C$ is a pretopos, then its self-indexing is a stack for its coherent topology. Exactness and extensivity are stronger than necessary, however; a pair of necessary and sufficient conditions for this to hold are that 1. If $R\;\rightrightarrows\; A$ is a kernel pair, then for any $f\colon B\to A$, the pullback $f^*R \;\rightrightarrows\; B$ is also a kernel pair (this is equivalent to the codomain fibration being a stack for the regular topology). 1. If $A,B \rightarrowtail C$ are a pair of subobjects, then for any $f\colon X\to A$ and $g\colon Y\to B$ and any isomorphism $f^*(A\cap B) \cong g^*(A\cap B)$, the pushout

$\array{f^*(A\cap B) & \overset{}{\to} & X\\ \downarrow && \downarrow\\ Y& \underset{}{\to} & Z}$

exists and is also a pullback.

Topoi of sheaves for coherent topologies on coherent categories are called coherent topoi. (The terminology is slightly confusing, though, because every topos is a coherent category.)

### Making categories coherent

Just like the reg/lex completion, there is a “coh/lex completion” which makes an arbitrary finitely complete category into a coherent one in a universal way.

Similarly, there are “pretopos completions” analogous to the ex/reg completion and the ex/lex completion.

### Subobjects, slices and internal logic

For any object $X$ in a coherent category $\mathcal{C}$, the poset of subobjects $Sub_{\mathcal{C}}(X)$ is a distributive lattice. For $f : X \to Y$ any morphism, the base change $f^* : Sub(Y) \to Sub(X)$ has a left adjoint $\exists_f : Sub(X) \to Sub(Y)$: the dependent sum/existential quantifier along $f$.

The corresponding functor/indexed category

$Sub : \mathcal{C}^{op} \to DistLat$

to the category of distributive lattices is the coherent hyperdoctrine of the coherent category $\mathcal{C}$.

### Topos of types

See topos of types.

## References

Section A1.4 of

Revised on October 25, 2012 22:12:28 by Urs Schreiber (82.169.65.155)