nLab
allegory

Idea

In category theory, an allegory is a category with properties meant to reflect properties that hold in a category Rel of relations. The notion was first introduced (as far as we know) and certainly first made famous in the book Categories, Allegories (Freyd-Scedrov).

Freyd and Scedrov argue that a categorical calculus of relations is an alternative and often more amenable framework for developing concepts traditionally couched in “functional” language (i.e., concepts which apply to sets and functions); for instance, a principal raison d’etre for regular categories is precisely that one can do relational calculus in them (as had been long known, e.g., Saunders MacLane showed how to calculate with relations to do diagram chases in abelian categories). Allegories, and correlative notions such as bicategories of relations, also offer a smooth approach to regular and exact completions, as used for example in the construction of realizability toposes.

A signal feature of allegories is emphasis on the modular law (see def. 1 below), which generalizes the modular law in lattices to more general relations, and which generalizes also so-called Frobenius reciprocity in categorical logic.

Definition

Definition

An allegory is a (1,2)-category $A$ equipped with an involution $(-{)}^o:A^{\mathrm{op}}\to A$ which is the identity on objects, such that

1. each hom-poset $A(x,y)$ has binary intersections, and
2. the modular law holds: for $\varphi :x\to y$, $\psi :y\to z$, and $\chi :x\to z$, we have $\psi \varphi \cap \chi \le \psi (\varphi \cap {\psi }^o\chi )$.

Examples

• If $C$ is a regular category and $\mathrm{Rel}(C)$ is the locally posetal bicategory of relations, then $\mathrm{Rel}(C)$ is an allegory.

• Any first-order hyperdoctrine with equality similarly gives rise to an allegory, as does any abstract bicategory of relations in the sense of Carboni-Walters.

• Any modular lattice can be regarded as a one-object allegory if we take composition to be union and the involution to be the identity.

Maps, tabulations, and units

A map in an allegory is a morphism that has a right adjoint. If $r⊣s$, then $s=r^o$ (hint: use the modular law to show $r⊣s\cap r^o$ and $r\cap s^o⊣s$).

Any 2-category has a bicategory of maps. In an allegory, the ordering between maps is discrete, meaning that if $f\le g$ then $f=g$. Consequently, the bicategory of maps of an allegory is a category.

A tabulation of a morphism $\varphi$ is a pair of maps $f,g$ such that $\varphi =g^{o}f$ and $f^{o}f\cap g^{o}g=1$. An allegory is tabular if every morphism has a tabulation, and pretabular if every morphism is contained in one that has a tabulation.

Every regular category, and indeed every locally regular category, has a tabular allegory of internal binary relations. Conversely, by restricting to the morphisms with left adjoints (“maps”) in a tabular allegory, we obtain a locally regular category. These constructions are inverse, so tabular allegories are equivalent to locally regular categories.

A locally regular category has finite products if and only if its tabular allegory of relations has top elements in its hom-posets.

Finally, a unit in an allegory is an object $U$ such that $1_U$ is the greatest morphism $U\to U$, and every object $X$ admits a morphism $\varphi :X\to U$ such that $1_X\le {\varphi }^o\varphi$. A locally regular category has a terminal object (hence is regular) if and only if its tabular allegory of relations has a unit.

Thus, regular categories are equivalent to unital (or unitary) tabular allegories. For more details, see Categories, Allegories, the Elephant, or Theory of units and tabulations in allegories.

Division allegories and power allegories

A distributive allegory is an allegory whose hom-posets have finite joins that are preserved by composition. Thus a distributive allegory is locally a lattice. The category of maps in a unitary tabular distributive allegory is a pre-logos, and conversely the bicategory of relations in a pre-logos is a unitary tabular distributive allegory.

A division allegory is a distributive allegory in which composition on one (and therefore the other) side has a right adjoint (left or right division). That is: given $r:A\to B$ and $s:A\to C$, there exists $r/s:B\to C$ such that

$$t\le s/r\in \mathrm{hom}(B,C)\iff t\circ r\le s\in \mathrm{hom}(A,C)$$t \leq s/r \in \hom(B, C) \Leftrightarrow t \circ r \leq s \in \hom(A, C)

(so that $-\circ r$ has right adjoint $-/r$: an example of a right Kan extension). Composition on the other side, $r\circ -$, has a right adjoint (an example of a right Kan lift) given by

$$r\backslash u≔(u^o/r^o{)}^o.$$r\backslash u \coloneqq (u^o/r^o)^o.

In the bicategory of sets and relations, with notation as above, we have

$$(s/r)(b,c)⊣⊢{\forall }_{a:A}r(a,b)\Rightarrow s(a,c)$$(s/r)(b, c) \dashv \vdash \forall_{a \colon A} r(a, b) \Rightarrow s(a, c)

where $r(a,b)$ is shorthand for ”$(a,b)$ belongs to $r$”.

The category of maps (functional relations) of a unitary/unital tabular division allegory is a logos, and conversely the bicategory of relations in a logos is a unitary tabular division allegory. (Categories, Allegories, 2.32, page 227.)

A power allegory is an allegory $𝒜$ such that the inclusion functor $\mathrm{Map}(𝒜)\to 𝒜$ has a right adjoint $P$. The counit at an object $B$ may be written

$${\ni }_B:P(B)\to B$$\ni_B \colon P(B) \to B

and we have the comprehension axiom? that to each $r:A\to B$ there is a map ${\chi }_r:A\to P(B)$ such that $r={\ni }_B\circ {\chi }_r$.

Theorem

A power allegory is a division allegory.

Proof (sketch)

Let $r:A\to C$ and $s:B\to C$ be morphisms; we construct a right Kan lift $s\backslash r$ of $r$ through $s$. This means that for all $t:A\to B$ we have $s\circ t\le r$ if and only if $t\le s\backslash r$.

We construct $s\backslash r$ as ${\chi }_s^o[\ge ]{\chi }_r$ where $[\ge ]:P(C)\to P(C)$ is a relation opposite to the internalization $[\le ]$ of the external order. One way to define $[\le ]$ is

$$[\le ]=(P(C)\stackrel{{\ni }^o}{\to }PP(C)\stackrel{\bigcup }{\to }P(C)$$[\leq] = (P(C) \stackrel{\ni^o}{\to} P P(C) \stackrel{\bigcup}{\to} P(C)

where $\bigcup :PP(C)\to P(C)$ internalizes the union operation, and is defined to be the map that classifies the composite

$$PP(C)\stackrel{{\ni }_{P(C)}}{\to }P(C)\stackrel{{\ni }_C}{\to }C.$$P P(C) \stackrel{\ni_{P(C)}}{\to} P(C) \stackrel{\ni_C}{\to} C.

(Full details to appear.)

In other language, a power allegory is a division allegory which associates to each object $B$ a morphism ${\ni }_B:P(B)\to B$ such that for all $r:A\to B$

• $1_A\le (r\backslash {\ni }_B)\circ ({\ni }_B\backslash r)$

which expresses the truth of the formula ${\forall }_{a:A}{\exists }_{S:P(B)}{\forall }_{b:B}S{\ni }_{B}b\iff r(a,b)$, and

• $({\ni }_B\backslash {\ni }_B)\wedge ({\ni }_B\backslash {\ni }_B{)}^o\le 1_{P(B)}$

which internalizes an axiom of extensionality, which reads ${\forall }_{b:B}(S{\ni }_{B}b)\iff (T{\ni }_{B}b)⊢S=T$. Given those axioms, and given $r:A\to B$, one may define

$${\chi }_r≔({\ni }_B\backslash r)\wedge (r\backslash {\ni }_B{)}^o,$$\chi_r \coloneqq (\ni_B \backslash r) \wedge (r\backslash \ni_B)^o,

which internalizes the formula-definition ${\chi }_r(a,S)≔{\forall }_{b}S{\ni }_{B}b\iff r(a,b)$, and then show ${\chi }_r$ is a map. (See Categories, Allegories, pp. 235-236.)

The bicategory of relations in a topos is a power allegory; conversely, the category of maps in a unitary tabular power allegory is a topos.

Syntactic allegories

Let $T$ be a regular theory. There is then an allegory ${𝒜}_T$ given as follows:

• the objects are finite strings of sorts of $T$;
• a morphism $\stackrel{\rightharpoonup }{X}\to \stackrel{\rightharpoonup }{Y}$ is a predicate $P(\stackrel{\rightharpoonup }{x},\stackrel{\rightharpoonup }{y})$ of sort $\stackrel{\rightharpoonup }{X},\stackrel{\rightharpoonup }{Y}$ (or rather a provable-equivalence class of such predicates);
• the identity $\stackrel{\rightharpoonup }{X}\to \stackrel{\rightharpoonup }{X}$ is (named by) $x_1=x_1\wedge x_2=x_2\wedge \cdots \wedge x_n=x_n$;
• the composite of $R:\stackrel{\rightharpoonup }{X}\to \stackrel{\rightharpoonup }{Y}$ and $S:Y\to \stackrel{\rightharpoonup }{X}$ is named by $\exists \stackrel{\rightharpoonup }{y}.R(\stackrel{\rightharpoonup }{x},\stackrel{\rightharpoonup }{y})\wedge S(\stackrel{\rightharpoonup }{y},\stackrel{\rightharpoonup }{z})$.

That ${𝒜}_T$ is an allegory is B.311 in Freyd–Scedrov; that it is in fact unitary and pre-tabular is B.312.

Further structure on $T$ gives rise to further structure on ${𝒜}_T$ (B.313): if $T$ is a coherent, first-order or higher-order theory, then ${𝒜}_T$ will be a distributive, division or power allegory respectively.

Every pre-tabular allegory has a tabular completion, given by splitting its coreflexive morphisms (i.e. those endomorphisms $R$ such that $R\subset \mathrm{id}$). The category of maps in the coreflexive splitting of ${𝒜}_T$ is precisely the syntactic category of $T$.

The existential quantifier

There are two possible ways to interpret a regular formula of the form $\exists y.R(x,y)\wedge S(y,z)$ in a unitary pre-tabular allegory, if $R$ and $S$ are interpreted as $r:X\to Y$ and $s:Y\to Z$ respectively: as the composite $s\cdot r$, or more ‘literally’ by:

• pulling $r$ and $s^o$ back to the same hom set and taking their intersection: $(p_1^{o}r{p}_1)\cap (p_2^o{s}^o{p}_2):X\times Z\to Y\times Y$;
• then forcing the two $Y$s to be equal by post-composing with ${\Delta }_Y^o:Y\times Y\to Y$, applying the existential quantifier by post-composing with the unique map ${!}_Y$ to the unit, and post-composing with ${!}_Z^o$ to get a morphism into $Z$;
• then forcing the $Z$ in the domain to be equal to the $Z$ in the codomain by taking the meet with $p_2:X\times Z\to Z$;
• and finally pulling back along (precomposing with the right adjoint of) $p_1:X\times Z\to X$ to get a morphism $X\to Z$.

We would like to know that these morphisms are equal, so that an existential formula will have a unique interpretation:

Proposition

$$sr=(p_2\cap {!}_Z^o{!}_Y{\Delta }_Y^o((p_1^{o}r{p}_1)\cap (p_2^o{s}^o{p}_2)))p_1^o$$s r = (p_2 \cap !_Z^o !_Y \Delta_Y^o ((p_1^o r p_1) \cap (p_2^o s^o p_2))) p_1^o

Proof

We show inclusion in each direction.

Firstly, $sr=sr\cap p_2{p}_1^o$, because the product projections tabulate the top morphism. Notice also that the RHS above is equal to

$$({\top }_{YZ}(r{p}_1\cap s^o{p}_2)\cap p_2)p_1^o$$(\top_{Y Z} (r p_1 \cap s^o p_2) \cap p_2) p_1^o

where ${\top }_{YZ}$ is the top morphism $Y\to Z$.

Now we can calculate:

$$\begin{array}{rlr}sr\cap p_2{p}_1^o& =(sr{p}_1\cap p_2)p_1^o& \text{modular law}\\ & =(sr{p}_1\cap p_2\cap p_2)p_1^o\\ & \le (s(r{p}_1\cap s^o{p}_2)\cap p_2)p_1^o& \text{modular law}\\ & \le ({\top }_{YZ}(r{p}_1\cap s^o{p}_2)\cap p_2)p_1^o\end{array}$$\begin{aligned} s r \cap p_2 p_1^o & = (s r p_1 \cap p_2) p_1^o & \text{modular law} \\ & = (s r p_1 \cap p_2 \cap p_2) p_1^o \\ & \leq (s(r p_1 \cap s^o p_2) \cap p_2) p_1^o & \text{modular law} \\ & \leq (\top_{Y Z} (r p_1 \cap s^o p_2) \cap p_2) p_1^o \end{aligned}

In the other direction, we have

$$\begin{array}{rlr}({\top }_{YZ}(r{p}_1\cap s^o{p}_2)\cap p_2)p_1^o& \le ({\top }_{YZ}{s}^o(sr{p}_1\cap p_2)\cap p_2)p_1^o& \text{modular law}\\ & \le ({\top }_{YY}(sr{p}_1\cap p_2)\cap p_2)p_1^o& {\top }_{YZ}{s}^0\le {\top }_{YY}\\ & =(p_2(p_1^{o}sr{p}_1\cap p_1^o{p}_2)\cap p_2)p_1^o& \top YY=p_2{p}_1^o\\ & =p_2(p_1^{o}sr{p}_1\cap p_1^o{p}_2\cap p_2^o{p}_2)p_1^o& \text{modular law}\\ & =p_2(p_1^{o}sr{p}_1\cap (p_1^o\cap p_2^o)p_2)p_1^o& \text{maps distribute}\\ & =p_2(p_1^{o}sr{p}_1\cap \Delta p_2)p_1^o& \text{see below}\\ & =p_2\Delta ({\Delta }^o{p}_1^{o}sr{p}_1\cap p_2)p_1^o& \text{modular law}\\ & =(sr{p}_1\cap p_2)p_1^o& p_1\Delta =p_2\Delta =\mathrm{id}\\ & =sr\cap p_2{p}_1^o& \text{modular law}\end{array}$$\begin{aligned} (\top_{Y Z} (r p_1 \cap s^o p_2) \cap p_2) p_1^o & \leq (\top_{Y Z} s^o (s r p_1 \cap p_2) \cap p_2) p_1^o & \text{modular law} \\ & \leq (\top_{Y Y} (s r p_1 \cap p_2) \cap p_2) p_1^o & \top_{Y Z} s^0 \leq \top_{Y Y}\\ & = (p_2 (p_1^o s r p_1 \cap p_1^o p_2) \cap p_2) p_1^o & \top{Y Y} = p_2 p_1^o \\ & = p_2 (p_1^o s r p_1 \cap p_1^o p_2 \cap p_2^o p_2) p_1^o & \text{modular law} \\ & = p_2 (p_1^o s r p_1 \cap (p_1^o \cap p_2^o) p_2) p_1^o & \text{maps distribute} \\ & = p_2 (p_1^o s r p_1 \cap \Delta p_2) p_1^o & \text{see below} \\ & = p_2 \Delta (\Delta^o p_1^o s r p_1 \cap p_2) p_1^o & \text{modular law} \\ & = (s r p_1 \cap p_2) p_1^o & p_1 \Delta = p_2 \Delta = id \\ & = s r \cap p_2 p_1^o & \text{modular law} \end{aligned}

and we are back to where we started. In the fourth-last step we used the fact that if $p_1,p_2:Z\times Z\to Z$ are the projections, then $p_1\cap p_2={\Delta }^o$. But $\Delta =⟨\mathrm{id},\mathrm{id}⟩$, and from lemma 1 here we have that $⟨\mathrm{id},\mathrm{id}⟩=p_1^o\cap p_2^o$.

Related entries

Other attempted axiomatizations of the same idea “something that acts like the category of relations in a regular category” include:

• bicategory of relations (a special sort of cartesian bicategory)

• 1-category equipped with relations

Discussion of the relation between pretabular unitary allegories and bicategories of relations, and also between tabular unitary allegories and regular categories is in

• Theory of units and tabulations in allegories

References

The standard monograph is

• Peter Freyd and Andre Scedrov, Categories, Allegories, Mathematical Library Vol 39, North-Holland (1990). ISBN 978-0-444-70368-2.

The notion is discussed also in chapter A3 of

• Peter Johnstone, Sketches of an Elephant

In

• Bob Walters, Categorical algebras of relations (blog post )

it is shown that any bicategory of relations is an allegory.

See also

• Wikipedia, Allegory