nLab
coherent hyperdoctrine

Definition

Let $C$ be a category with finite limits. A coherent hyperdoctrine over $C$ is a functor

$$P:C^{\mathrm{op}}\to \mathrm{DistLattice}$$P : C^{op} \to DistLattice

from the opposite category of $C$ to the category of distributive lattices, such that for every morphism $f:A\to B$ in $C$, the functor $P(A)\to P(B)$ has a left adjoint ${\exists }_f$ satisfying

1. Frobenius reciprocity;

2. Beck-Chevalley condition.

Properties

The assignment (here) of a coherent hyperdoctrine $S(C)$ to a coherent category $C$ extends to a 2-adjunction

$$(A⊣S):\mathrm{CoherentCat}\stackrel{\stackrel{A}{\leftarrow }}{\underset{S}{\hookrightarrow }}\mathrm{CoherentHyperdoctrine}$$(A \dashv S) : CoherentCat \stackrel{\overset{A}{\leftarrow}}{\underset{S}{\hookrightarrow}} CoherentHyperdoctrine

with the right adjoint being a full and faithful 2-functor, hence exhibiting $\mathrm{CoherentCat}$ as a reflective sub-2-category of $\mathrm{CoherentHyperdoctrine}$.

(Here $\mathrm{CoherentCat}$ has as 2-morphisms those natural transformations that preserve finite products.)

This appears as (Coumans, prop. 8).

Coherent hyperdoctrines are closed under canonical extension $(-{)}^{\delta }:\mathrm{DistLattice}\to \mathrm{DistLattice}$, in that for $P:C^{\mathrm{op}}\to \mathrm{DistLattic}$ a coherent hyperdoctrine, so is $(-{)}^{\delta }\circ P$.

This appears as (Coumans, prop. 9).

Examples

Powersets

The powerset functor

$$P:=\{0,1{\}}^{(-)}:{\mathrm{Set}}^{\mathrm{op}}\to \mathrm{DistLattice}$$P := \{0,1\}^{(-)} : Set^{op} \to DistLattice

(sending a set to its power set and a function to the preimage-assignment) is a coherent hyperdoctrine.

Over a coherent category

Let $C$ be a coherent category. For every object $A\in C$ the poset of subobjects ${\mathrm{Sub}}_C(A)$ is a distributive lattice.

The corresponding functor

$$C^{\mathrm{op}}\to \mathrm{DistLattice}$$C^{op} \to DistLattice

from the opposite category of $C$ to the category of distributive lattices is called the coherent hyperdoctrine of $C$.

For a coherent theory

Accordingly, there is a coherent hyperdoctrine associated with any coherent theory, where the objects of $C$ are lists of free variables in the theory, and the lattice assigned to them is that of propositions of the theory in this context.

Related concepts

• first-order hyperdoctrine

• Boolean hyperdoctrine

References

• Dion Coumans, Generalizing canonical extensions to the categorical setting (Arxiv)