nLab
allegory

Contents

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 AA equipped with an involution () o:A opA(-)^o \colon A^{op} \to A which is the identity on objects, such that

  1. each hom-poset A(x,y)A(x,y) has binary intersections, and
  2. the modular law holds: for ϕ:xy\phi\colon x\to y, ψ:yz\psi\colon y\to z, and χ:xz\chi\colon x\to z, we have ψϕχψ(ϕψ oχ)\psi \phi \cap \chi \le \psi (\phi \cap \psi^o \chi).

Examples

Maps, tabulations, and units

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

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

A tabulation of a morphism ϕ\phi is a pair of maps f,gf,g such that ϕ=g of\phi = g^o f and f ofg og=1f^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 UU such that 1 U1_U is the greatest morphism UUU\to U, and every object XX admits a morphism ϕ:XU\phi\colon X\to U such that 1 Xϕ oϕ1_X\le \phi^o\phi. 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

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:ABr: A \to B and s:ACs \colon A \to C, there exists r/s:BCr/s: B \to C such that

ts/rhom(B,C)trshom(A,C)t \leq s/r \in \hom(B, C) \Leftrightarrow t \circ r \leq s \in \hom(A, C)

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

r\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) a:Ar(a,b)s(a,c)(s/r)(b, c) \dashv \vdash \forall_{a \colon A} r(a, b) \Rightarrow s(a, c)

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

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.)

Power allegories

A power allegory is, more or less, an allegory 𝒜\mathcal{A} such that the inclusion functor i:Map(𝒜)𝒜i: Map(\mathcal{A}) \to \mathcal{A} has a right adjoint PP. The idea is that PP assigns to an object AA a power object P(A)P(A), as in topos theory; if we summarize the notion of topos as a regular category E\mathbf{E} for which the inclusion i:ERel(E)i: \mathbf{E} \to Rel(\mathbf{E}) has a right adjoint PP, then it becomes apparent that the notion of power allegory is similar except that it takes the “relation side” as primary and derives the “function side” as Map(𝒜)Map(\mathcal{A}), whereas in topos theory it’s just the other way around. But in either case the adjunction iPi \dashv P is fundamental.

Since the inclusion ii is the identity on objects, the counit of the adjunction iPi \dashv P at an object BB may be written

B:P(B)B\ni_B: P(B) \to B

and we have a kind of comprehension scheme that to each r:ABr: A \to B there is a unique map χ r:AP(B)\chi_r: A \to P(B), the characteristic map of rr, such that r= Bχ rr = \ni_B \circ \chi_r. (If AA and BB are related by a property rr, then for each aa there is a subobject χ r(a)\chi_r(a) of BB consisting of elements bb so related to aa.) In the case r=1 A:AAr = 1_A: A \to A, the characteristic map χ 1 A:AP(A)\chi_{1_A}: A \to P(A) is called the singleton map of AA, and more general χ r\chi_r may be defined as P(r)σ AP(r) \sigma_A.

Freyd-Scedrov definition

The exact definition of power allegory is a matter for consideration. One can get a certain distance just by adopting the naive definition suggested above, that a power allegory is nothing more than an allegory for which the inclusion Map(𝒜)𝒜Map(\mathcal{A}) \to \mathcal{A} has a right adjoint PP. (Below we introduce a similar notion that we call a PP-allegory.) But it seems hard to develop a theory from the naive notion that rises to a level comparable to topos theory.

Freyd and Scedrov start with a structure of division allegory (thus packing in a good amount of internal logic from the start) and introduce the fundamental adjunction iPi \dashv P in terms of that structure. For them, a power allegory is defined to be a division allegory which associates to each object BB a morphism B:P(B)B\ni_B \colon P(B) \to B such that for all r:ABr \colon A \to B

  • 1 A(r\ B)( B\r)1_A \leq (r \backslash \ni_B) \circ (\ni_B \backslash r)

which expresses the truth of the formula a:A S:P(B) b:BS Bbr(a,b)\forall_{a \colon A} \exists_{S: P(B)} \forall_{b \colon B} S \ni_B b \Leftrightarrow r(a, b), and

  • ( B\ B)( B\ B) o1 P(B)(\ni_B \backslash \ni_B) \wedge (\ni_B \backslash \ni_B)^o \leq 1_{P(B)}

which internalizes an axiom of extensionality, which reads b:B(S Bb)(T Bb)S=T\forall_{b \colon B} (S \ni_B b) \Leftrightarrow (T \ni_B b) \vdash S = T. Given those axioms, and given r:ABr: A \to B, one may define

χ r( B\r)(r\ B) o,\chi_r \coloneqq (\ni_B \backslash r) \wedge (r\backslash \ni_B)^o,

which internalizes the formula-definition χ r(a,S) bS Bbr(a,b)\chi_r(a, S) \coloneqq \forall_b S \ni_B b \Leftrightarrow r(a, b), and then show χ r\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.

Variant notion

Nevertheless, the spare elegance of the naive definition gives one something to shoot for. It appears that quite a decent theory can be developed just by adding the assumption of coproducts in an allegory: a reasonable and fairly mild assumption. (Most allegories don’t admit many colimits; for example having coequalizers is pretty rare. But the standard examples do have finite coproducts, coinciding with coproducts on the maps/functional side.)

Definition

A PP-allegory is an allegory 𝒜\mathcal{A} with finite coproducts1 for which the inclusion i:Map(𝒜)𝒜i: Map(\mathcal{A}) \to \mathcal{A} has a right adjoint PP.

As before, the counit is denoted :iP1 𝒜\ni: i P \to 1_{\mathcal{A}}. It is perhaps surprising that the notion of PP-allegory is at least as strong as power allegory in the Freyd-Scedrov sense:

Theorem

Any PP-allegory is a division allegory in which the Freyd-Scedrov conditions on \ni are satisfied.

Proof (sketch)

For now we content ourselves with a description of the division structure. Let r:ACr: A \to C and s:BCs: B \to C be morphisms; we construct a right Kan lift s\rs \backslash r of rr through ss. This means that for all t:ABt: A \to B we have strs \circ t \leq r if and only if ts\rt \leq s \backslash r. We begin by constructing the right Kan lift for the case r=s= C:PCCr = s = \ni_C: P C \to C.

Define the internal union C\bigcup_C by C=P( C):PPCPC\bigcup_C = P(\ni_C): P P C \to P C, and define an internal order relation [] C:PCPC[\Rightarrow]_C: P C \to P C by PC PCPPC CPCP C \stackrel{\in_{P C}}{\to} P P C \stackrel{\bigcup_C}{\to} P C. (Here o\in \coloneqq \ni^o.) Define [] C[] C o[\Leftarrow]_C \coloneqq [\Rightarrow]_C^o.

We now show [] C= C\ C[\Leftarrow]_C = \ni_C \backslash \ni_C. That is, for R:PCPCR: P C \to P C, we show CR C\ni_C R \leq \ni_C is equivalent to R[]R \leq [\Leftarrow]. The backward implication is easy; for the forward implication, one may prove it first for reflexive RR where we have an actual equation CR= C\ni_C R = \ni_C. It follows that P( C)P(R)=P( C)P(\ni_C) P(R) = P(\ni_C), whence P(R) C o CP(R) \leq \bigcup_C^o \bigcup_C. A short calculation then yields R= CP(R)σ PC= C C o Cσ PC= C C o=[]R = \ni_C P(R) \sigma_{P C} = \ni_C \bigcup_C^o \bigcup_C \sigma_{P C} = \ni_C \bigcup_C^o = [\Leftarrow]. The case for general RR reduces to the reflexive case: form the reflexive completion 1R1 \vee R as the composite

C1 PC,RC+CCC \stackrel{\langle 1_{P C}, R \rangle}{\to} C + C \stackrel{\nabla}{\to} C

which is where coproducts come in; here \nabla is the codiagonal and we use the fact that C+CC + C in an allegory is a biproduct to form the pairing for the first arrow. It is easy to show that C(1R)= C CR= C\ni_C(1 \vee R) = \ni_C \vee \ni_C R = \ni_C, and then we derive R1R[]R \leq 1 \vee R \leq [\Leftarrow] from before. Thus we have shown [] C= C\ C[\Leftarrow]_C = \ni_C \backslash \ni_C.

For general r:AC,s:BCr: A \to C, s: B \to C, we claim the right Kan lift s\r:ABs \backslash r: A \to B is given by χ s o( C\ C)χ r\chi_s^o (\ni_C \backslash \ni_C) \chi_r. For, we have r= Cχ rr = \ni_C \chi_r, whence

str iff Cχ st Cχ r iff Cχ stχ r o C iff χ stχ r o C\ C iff tχ s o( C\ C)χ r\array{ s t \leq r & iff & \ni_C \chi_s t \leq \ni_C \chi_r \\ & iff & \ni_C \chi_s t \chi_r^o \leq \ni_C \\ & iff & \chi_s t \chi_r^o \leq \ni_C \backslash \ni_C \\ & iff & t \leq \chi_s^o (\ni_C \backslash \ni_C) \chi_r }

thus proving the claim.

Further details may be found here.

Thus the notion of PP-category is just as strong as the Freyd-Scedrov notion of power allegory, and one can then piggy-back on their further developments.

Syntactic allegories

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

  • the objects are finite strings of sorts of TT;

  • a morphism XY\vec X \to \vec Y is a predicate P(x,y)P(\vec x, \vec y) of sort X,Y\vec X, \vec Y (or rather a provable-equivalence class of such predicates);

  • the identity XX\vec X \to \vec X is (named by) x 1=x 1x 2=x 2x n=x nx_1 = x_1 \wedge x_2 = x_2 \wedge \cdots \wedge x_n = x_n;

  • the composite of R:XYR \colon \vec X \to \vec Y and S:YXS \colon Y \to \vec X is named by y.R(x,y)S(y,z)\exists \vec y. R(\vec x, \vec y) \wedge S(\vec y, \vec z).

That 𝒜 T\mathcal{A}_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 TT gives rise to further structure on 𝒜 T\mathcal{A}_T (B.313): if TT is a coherent, first-order or higher-order theory, then 𝒜 T\mathcal{A}_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 RR such that RidR \subset id). The category of maps in the coreflexive splitting of 𝒜 T\mathcal{A}_T is precisely the syntactic category of TT.

The existential quantifier

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

  • pulling rr and s os^o back to the same hom set and taking their intersection: (p 1 orp 1)(p 2 os op 2):X×ZY×Y(p_1^o r p_1) \cap (p_2^o s^o p_2) \colon X \times Z \to Y \times Y;

  • then forcing the two YYs to be equal by post-composing with Δ Y o:Y×YY\Delta_Y^o \colon Y \times Y \to Y, applying the existential quantifier by post-composing with the unique map ! Y!_Y to the unit, and post-composing with ! Z o!_Z^o to get a morphism into ZZ;

  • then forcing the ZZ in the domain to be equal to the ZZ in the codomain by taking the meet with p 2:X×ZZp_2 \colon X \times Z \to Z;

  • and finally pulling back along (precomposing with the right adjoint of) p 1:X×ZXp_1 \colon X \times Z \to X to get a morphism XZX \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! Z o! YΔ Y o((p 1 orp 1)(p 2 os op 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=srp 2p 1 os r = s r \cap p_2 p_1^o, because the product projections tabulate the top morphism. Notice also that the RHS above is equal to

( YZ(rp 1s op 2)p 2)p 1 o (\top_{Y Z} (r p_1 \cap s^o p_2) \cap p_2) p_1^o

where YZ\top_{Y Z} is the top morphism YZY \to Z.

Now we can calculate:

srp 2p 1 o =(srp 1p 2)p 1 o modular law =(srp 1p 2p 2)p 1 o (s(rp 1s op 2)p 2)p 1 o modular law ( YZ(rp 1s op 2)p 2)p 1 o \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

( YZ(rp 1s op 2)p 2)p 1 o ( YZs o(srp 1p 2)p 2)p 1 o modular law ( YY(srp 1p 2)p 2)p 1 o YZs 0 YY =(p 2(p 1 osrp 1p 1 op 2)p 2)p 1 o YY=p 2p 1 o =p 2(p 1 osrp 1p 1 op 2p 2 op 2)p 1 o modular law =p 2(p 1 osrp 1(p 1 op 2 o)p 2)p 1 o maps distribute =p 2(p 1 osrp 1Δp 2)p 1 o see below =p 2Δ(Δ op 1 osrp 1p 2)p 1 o modular law =(srp 1p 2)p 1 o p 1Δ=p 2Δ=id =srp 2p 1 o modular law \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×ZZp_1, p_2 \colon Z \times Z \to Z are the projections, then p 1p 2=Δ op_1 \cap p_2 = \Delta^o. But Δ=id,id\Delta = \langle id, id \rangle, and from lemma 1 here we have that id,id=p 1 op 2 o\langle id, id \rangle = p_1^o \cap p_2^o.

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

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

References

The standard monograph is

The notion is discussed also in chapter A3 of

In

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

See also


  1. We mean coproducts as certain conical colimits qua PosPos-enriched categories.

Revised on October 28, 2016 10:05:46 by Todd Trimble (67.81.95.215)