Todd Trimble Theory of units and tabulations in allegories




In this article we establish a connection between pretabular unitary allegories and bicategories of relations, and also between tabular unitary allegories and regular categories. The material is entirely adapted from Categories, Allegories?; we have merely changed some details of arrangement, notation, and terminology.


We write the composite of morphisms r:abr \colon a \to b, s:bcs \colon b \to c as sr:acs r \colon a \to c.

An allegory is a PosPos-enriched \dagger-category AA where each hom-poset has binary meets, and the modular law is satisfied. The modular law takes two forms, whenever the left sides of the inequalities make sense:

(and of course there are variations, using commutativity of \wedge). Each of these forms can be derived from the other, using the \dagger-structure.

The \dagger-operation, which we henceforth denote by () o(-)^o, preserves meets since it preserves order and is an involution.)


For any r:abr \colon a \to b, we have rrr orr \leq r r^o r.


We have rr1 brr(1r or)rr orr \leq r 1_b \wedge r \leq r(1 \wedge r^o r) \leq r r^o r where the middle inequality uses the modular law.

Recall that a map in an allegory is a morphism f:abf \colon a \to b such that ff of \dashv f^o. A relation r:abr \colon a \to b is well-defined if we merely have a counit inclusion rr o1 br r^o \leq 1_b, and is total if we merely have a unit inclusion 1 ar or1_a \leq r^o r. Clearly maps are closed under composition, as are total relations and well-defined relations.


If f:abf \colon a \to b is a map, then for any r,shom(b,c)r, s \in \hom(b, c) we have (rs)f=rfsf(r \wedge s)f = r f \wedge s f.


The non-trivial inclusion follows from

rfsf(rsff o)f(rs)fr f \wedge s f \leq (r \wedge s f f^o)f \leq (r \wedge s)f

where the first inequality is an instance of the modular law, and the second holds for any well-defined relation ff.


If f,g:abf, g \colon a \to b are maps and fgf \leq g, then f=gf = g.

Since the dagger operation () o:hom(a,b)hom(b,a)(-)^o \colon \hom(a, b) \to \hom(b, a) preserves order, we have f og of^o \leq g^o. But also the inclusion fgf \leq g between left adjoints is mated to an inclusion g of og^o \leq f^o between right adjoints. Hence f o=g of^o = g^o, and therefore f=gf = g.

Domains and coreflexives


Let r:abr \colon a \to b be a morphism. We define the domain dom(r)\dom(r) to be 1 ar or1_a \wedge r^o r. A morphism e:aae \colon a \to a is coreflexive if e1 ae \leq 1_a; in particular, domains are coreflexive. Cor(a)Cor(a) denotes the poset of coreflexives in hom(a,a)\hom(a, a).


Coreflexives r:aar \colon a \to a are symmetric and transitive. (Symmetric and transitive imply idempotent.)


We have rrr or1 ar o1 ar or \leq r r^o r \leq 1_a r^o 1_a \leq r^o where the first inequality is lemma . Of course also rr1 ar=rr r \leq 1_a r = r. (If rr is symmetric and transitive, then rrr or=rrrrrr \leq r r^o r = r r r \leq r r as well.)


For r,shom(a,b)r, s \in \hom(a, b), we have dom(rs)=1 ar os\dom(r \wedge s) = 1_a \wedge r^o s.


One inclusion is trivial:

dom(rs)=1 a(rs) o(rs)1 ar os.\dom(r \wedge s) = 1_a \wedge (r \wedge s)^o (r \wedge s) \leq 1_a \wedge r^o s.

The other inclusion follows from fairly tricky applications of the modular law:

1 as or 1 a(1 a(1 as or)) 1 a(1 as o(sr)) 1 a((sr) os o)(sr) 1 a(sr) o(sr) = dom(sr).\array{ 1_a \wedge s^o r & \leq & 1_a \wedge (1_a \wedge (1_a \wedge s^o r)) \\ & \leq & 1_a \wedge (1_a \wedge s^o(s \wedge r)) \\ & \leq & 1_a \wedge ((s \wedge r)^o \wedge s^o)(s \wedge r) \\ & \leq & 1_a \wedge (s \wedge r)^o (s \wedge r) \\ & = & \dom(s \wedge r). }

For r:abr \colon a \to b and coreflexives chom(a,a)c \in \hom(a, a), we have dom(r)c\dom(r) \leq c if and only if rrcr \leq r c. In particular, rrdom(r)r \leq r \circ \dom(r).


If 1 ar orc1_a \wedge r^o r \leq c, then

rr1 arr(1 ar or)rc.r \leq r 1_a \wedge r \leq r(1_a \wedge r^o r) \leq r c.

If rrcr \leq r c, then

1 ar or1 ar orc(c or or)cc occ1_a \wedge r^o r \leq 1_a \wedge r^o r c \leq (c^o \wedge r^o r)c \leq c^o c \leq c

where the antepenultimate inequality uses the modular law, and the last uses lemma .


For r:abr \colon a \to b and s:bcs \colon b \to c, we have dom(sr)dom(r)\dom(s r) \leq \dom(r).

By lemma , it suffices that srsrdom(r)s r \leq s r \circ \dom(r). But this follows from the last sentence of lemma .



An object tt is a unit in an allegory if 1 t1_t is maximal in hom(t,t)\hom(t, t) and if for every object aa there is f:atf \colon a \to t such that 1 af of1_a \leq f^o f (i.e., ff is total).

Of course by maximality we also have ff o1 tf f^o \leq 1_t, so such ff must also be a map.

We say AA is unital (Freyd-Scedrov say unitary) if AA has a unit.


Let tt be a unit. Then dom:hom(a,t)Cor(a)\dom \colon \hom(a, t) \to Cor(a) is an injective order-preserving function.


Order-preservation is clear. If r,s:atr, s \colon a \to t and dom(r)dom(s)\dom(r) \leq \dom(s), then rsr \leq s:

rrdom(r)rdom(s)rs ossr \leq r \circ \dom(r) \leq r \circ \dom(s) \leq r s^o s \leq s

where the first inequality uses lemma , and the last inequality follows from rs o1 tr s^o \leq 1_t (since 1 t1_t is maximal in hom(t,t)\hom(t, t)). Therefore dom(r)=dom(s)\dom(r) = \dom(s) implies r=sr = s.


For a unit tt and any aa, there is at most one total relation = map r:atr \colon a \to t (because in that case dom(r)=1 a\dom(r) = 1_a, and we apply the previous proposition), and this is maximal in hom(a,t)\hom(a, t). Thus tt is terminal in Map(A)Map(A).

Let ε a:at\varepsilon_a \colon a \to t denote the maximal element of hom(a,t)\hom(a, t). For any r:abr \colon a \to b, we then have rε b oε ar \leq \varepsilon_b^o \varepsilon_a since this is mated to the inequality ε brε a\varepsilon_b r \leq \varepsilon_a. Therefore ε b oε a\varepsilon_b^o \varepsilon_a is the maximal element of hom(a,b)\hom(a, b).

Tabulations in allegories

Recall from Categories, Allegories that a tabulation of r:abr \colon a \to b is a pair of maps f:xaf \colon x \to a, g:xbg \colon x \to b such that r=gf or = g f^o and f ofg og=1 xf^o f \wedge g^o g = 1_x.

Preliminaries on tabulations


For maps f:xaf \colon x \to a, g:xbg \colon x \to b, the condition f ofg og=1 xf^o f \wedge g^o g = 1_x implies (f,g)(f, g) is a jointly monic pair in Map(A)Map(A).


Let h,h:yxh, h' \colon y \to x be maps, and suppose fh=fhf h = f h' and gh=ghg h = g h'. If f ofg og=1 xf^o f \wedge g^o g = 1_x, then

h=(f ofg og)h=f ofhg ogh=f ofhg ogh=(f ofg ogg)h=hh = (f^o f \wedge g^o g)h = f^o f h \wedge g^o g h = f^o f h' \wedge g^o g h' = (f^o f \wedge g^o g g)h' = h'

where the second and fourth equations use lemma .


Suppose r:abr: a \to b is tabulated by (f:xa,g:xb)(f \colon x \to a, g \colon x \to b), and suppose h:yah \colon y \to a, k:ybk \colon y \to b are maps. We have kh ogf ok h^o \leq g f^o if and only if there exists a map j:yxj \colon y \to x such that h=fjh = f j and k=gjk = g j (this jj is unique by lemma ).


One direction is easy: if h=fjh = f j and k=gjk = g j for some map jj, then

kh o=gjj of ogf o.k h^o = g j j^o f^o \leq g f^o.

In the other direction: suppose kh ogf ok h^o \leq g f^o. Put j=f ohg okj = f^o h \wedge g^o k. First we check that jj is a map. We have 1 yj oj1_y \leq j^o j from

1 y1 y(k ok)(h oh)1 yk ogf ohdom(f ohg ok)=dom(j)1_y \leq 1_y \wedge (k^o k)(h^o h) \leq 1_y \wedge k^o g f^o h \leq \dom(f^o h \wedge g^o k) = \dom(j)

using lemma . We have jj o1 xj j^o \leq 1_x from

(f ohg ok)(h ofk og)(f ohh of)(g okk og)(f ofg og)1 x(f^o h \wedge g^o k)(h^o f \wedge k^o g) \leq (f^o h h^o f) \wedge (g^o k k^o g) \leq (f^o f \wedge g^o g) \leq 1_x

where the last step uses one of the tabulation conditions. So jj is a map.

Finally, we have fjf(f oh)hf j \leq f(f^o h) \leq h, which implies fj=hf j = h (lemma ). Similarly gj=kg j = k.


Tabulations are unique up to unique isomorphism.


A diagram in Map(A)Map(A)

p h a k f b g c\array{ p & \stackrel{h}{\to} & a \\ ^\mathllap{k} \downarrow & & \downarrow^\mathrlap{f} \\ b & \underset{g}{\to} & c }

commutes if and only if kh og ofk h^o \leq g^o f.


An identity inclusion gk=fhg k = f h is certainly mated to an inclusion kh og ofk h^o \leq g^o f. Conversely, an inclusion kh og ofk h^o \leq g^o f is mated to gkfhg k \leq f h, and we can use lemma .


Given f:acf \colon a \to c and g:bcg \colon b \to c in Map(A)Map(A), a tabulation (h:pa,k:pb)(h \colon p \to a, k \colon p \to b) of r=g ofr = g^o f provides a pullback of (f,g)(f, g).


Indeed, by definition of tabulation we then have kh o=g ofk h^o = g^o f, so gk=fhg k = f h. For the universality of (h,k)(h, k): if gk=fhg k' = f h', then k(h) og ofk (h')^o \leq g^o f, and we can apply proposition to finish.


If i:abi \colon a \to b is a monomorphism in Map(A)Map(A) and i oii^o i has a tabulation, then i oi=1 ai^o i = 1_a.


The tabulation of i oii^o i gives a pullback of the pair (i,i)(i, i), but since this pullback is already (1 a,1 a)(1_a, 1_a), the conclusion is clear.


If r:aar \colon a \to a is coreflexive, then for any tabulation (f,g)(f, g) of rr, we have f=gf = g and ff is monic.


The inclusion gf o=r1 ag f^o = r \leq 1_a is mated to gfg \leq f which must be an identity g=fg = f. If (f,g)=(f,f)(f, g) = (f, f) is jointly monic, then ff is monic.

Pretabularity and tabularity


An allegory is tabular if every morphism r:abr \colon a \to b admits a tabulation. A unital allegory is pretabular if for all a,ba, b, the maximal morphism ε b oε ahom(a,b)\varepsilon_b^o \varepsilon_a \in \hom(a, b) (see the last sentence of the Units section) admits a tabulation.

It is immediate from corollary that if AA is tabular, then Map(A)Map(A) has pullbacks.

Likewise, it is immediate from the preceding corollary that if AA is unital and pretabular, then Map(A)Map(A) has products, because we can form the pullback of the maps ε a:at\varepsilon_a \colon a \to t, ε b:bt\varepsilon_b \colon b \to t to the terminal object tt.


In a tabular allegory AA, a map q:aeq \colon a \to e is a strong epi in Map(A)Map(A) if qq o=1 eq q^o = 1_e.


If qq o=1 eq q^o = 1_e, then it is first of all clear that qq is an epi in Map(A)Map(A) because it retracts q oq^o in AA. We show qq is orthogonal to monomorphisms in Map(A)Map(A). That is, consider a commutative diagram

a q e f j b i x\array{ a & \stackrel{q}{\to} & e \\ ^\mathllap{f} \downarrow & & \downarrow^\mathrlap{j} \\ b & \underset{i}{\to} & x }

where ii is monic. We wish to show there exists a filler map g:ebg \colon e \to b such that gq=fg q = f and ig=ji g = j. The uniqueness of a filler map is clear since ii is monic.

Put g=fq og = f q^o. We first check that gg is a map. Notice that the identity inclusion if=jqi f = j q is mated to an inclusion fq oi ojf q^o \leq i^o j, so we have gi ojg \leq i^o j. In that case we have

gg oi ojj oii oi1 eg g^o \leq i^o j j^o i \leq i^o i \leq 1_e

where the last inclusion holds because ii is monic (corollary ). This gives the counit for gdashvg og \dash v g^o. For the unit, use

1 b=qq oqf ofq o=g og.1_b = q q^o \leq q f^o f q^o = g^o g.

So g=fq og = f q^o is a map. We also have

j=jqq o=ifq o=ig,j = j q q^o = i f q^o = i g,

and finally we have

ffq oq=gqf \leq f q^o q = g q

so that f=gqf = g q by lemma . This completes the proof.


If AA is tabular, then Map(A)Map(A) has equalizers. Moreover, every map has a (strong epi)-mono factorization, and strong epis are preserved by pullbacks. In short, Map(A)Map(A) is a locally regular category. If AA is moreover unital, then Map(A)Map(A) is regular.


The equalizer of a pair of maps f,g:abf, g \colon a \to b may be constructed as a tabulation of the coreflexive arrow dom(fg)\dom(f \wedge g). By lemma , the tabulation is of the form (h,h)(h, h) where hh is monic, and by an application of proposition , one sees it is the universal map that equalizes ff and gg.

For any map f:abf \colon a \to b, consider a tabulation of the coreflexive dom(f o)=ff o:bb\dom(f^o) = f f^o \colon b \to b by a pair of maps (i,i)(i, i). Notice that i:ebi \colon e \to b is monic in Map(A)Map(A), and ii o=ff oi i^o = f f^o. By proposition , there exists a unique q:aeq \colon a \to e such that f=iqf = i q. Following the proof of proposition , the map qq is constructed as i ofi^o f. We have

1 ei oii oi=i off oi=qq o1_e \leq i^o i i^o i = i^o f f^o i = q q^o

i.e., dom(q o)=1 e\dom(q^o) = 1_e (q oq^o is total). By lemma , this means qq is a strong epi in Map(A)Map(A). Thus we have factored ff into a strong epi followed by a mono.

Now suppose q:aeq \colon a \to e is any strong epi and g:deg \colon d \to e is a map, and that (g:pa,q:pd)(g' \colon p \to a, q' \colon p \to d) is a pullback of (g,q)(g, q). Then (g,q)(g', q') is a tabulation of q ogq^o g, so q og=g(q) oq^o g = g' (q')^o. Now the left side of this equation is total, and therefore so is the right: 1 edom(g(q) o)1_e \leq \dom(g' (q')^o). But then

1 edom(g(q) o)dom((q) o)1_e \leq \dom(g' (q')^o) \leq \dom((q')^o)

where the second inequality uses corollary . This means qq' is strong epi, and we are done.

Revised on August 27, 2012 at 20:46:33 by Todd Trimble