Todd Trimble
Theory of units and tabulations in allegories

Contents

Introduction

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.

Preliminaries

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

Lemma

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

Proof

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.

Lemma

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.

Proof

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.

Lemma

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

Definition

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

Lemma

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

Proof

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

Lemma

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.

Proof

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

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

Proof

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

Corollary

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 6, it suffices that srsrdom(r)s r \leq s r \circ \dom(r). But this follows from the last sentence of lemma 6.

Units

Definition

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.

Proposition

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.

Proof

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 6, 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.

Corollary

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

Lemma

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

Proof

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

Proposition

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

Proof

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 5. 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 3). Similarly gj=kg j = k.

Corollary

Tabulations are unique up to unique isomorphism.

Proposition

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.

Proof

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

Corollary

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

Proof

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 2 to finish.

Corollary

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.

Proof

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.

Lemma

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.

Proof

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

Definition

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

Lemma

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.

Proof

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 5). 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 3. This completes the proof.

Theorem

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.

Proof

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 8, the tabulation is of the form (h,h)(h, h) where hh is monic, and by an application of proposition 2, 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 2, there exists a unique q:aeq \colon a \to e such that f=iqf = i q. Following the proof of proposition 2, 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 9, 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 1. This means qq' is strong epi, and we are done.

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