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:ab, s:bc as sr:ac.

An allegory is a Pos-enriched -category A 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 ). Each of these forms can be derived from the other, using the -structure.

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

Lemma

For any r:ab, we have rrr or.

Proof

We have rr1 brr(1r or)rr or where the middle inequality uses the modular law.

Recall that a map in an allegory is a morphism f:ab such that ff o. A relation r:ab is well-defined if we merely have a counit inclusion rr o1 b, and is total if we merely have a unit inclusion 1 ar or. Clearly maps are closed under composition, as are total relations and well-defined relations.

Lemma

If f:ab is a map, then for any r,shom(b,c) we have (rs)f=rfsf.

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

Lemma

If f,g:ab are maps and fg, then f=g.

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

Domains and coreflexives

Definition

Let r:ab be a morphism. We define the domain dom(r) to be 1 ar or. A morphism e:aa is coreflexive if e1 a; in particular, domains are coreflexive. Cor(a) denotes the poset of coreflexives in hom(a,a).

Lemma

Coreflexives r:aa are symmetric and transitive. (Symmetric and transitive imply idempotent.)

Proof

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

Lemma

For r,shom(a,b), we have dom(rs)=1 ar os.

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:ab and coreflexives chom(a,a), we have dom(r)c if and only if rrc. In particular, rrdom(r).

Proof

If 1 ar orc, 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 rrc, 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:ab and s:bc, we have dom(sr)dom(r).

By lemma 6, it suffices that srsrdom(r). But this follows from the last sentence of lemma 6.

Units

Definition

An object t is a unit in an allegory if 1 t is maximal in hom(t,t) and if for every object a there is f:at such that 1 af of (i.e., f is total).

Of course by maximality we also have ff o1 t, so such f must also be a map.

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

Proposition

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

Proof

Order-preservation is clear. If r,s:at and dom(r)dom(s), then rs:

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 t (since 1 t is maximal in hom(t,t)). Therefore dom(r)=dom(s) implies r=s.

Corollary

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

Let ε a:at denote the maximal element of hom(a,t). For any r:ab, we then have rε b oε a since this is mated to the inequality ε brε a. Therefore ε b oε a is the maximal element of hom(a,b).

Tabulations in allegories

Recall from Categories, Allegories that a tabulation of r:ab is a pair of maps f:xa, g:xb such that r=gf o and f ofg og=1 x.

Preliminaries on tabulations

Lemma

For maps f:xa, g:xb, the condition f ofg og=1 x implies (f,g) is a jointly monic pair in Map(A).

Proof

Let h,h:yx be maps, and suppose fh=fh and gh=gh. If f ofg og=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:ab is tabulated by (f:xa,g:xb), and suppose h:ya, k:yb are maps. We have kh ogf o if and only if there exists a map j:yx such that h=fj and k=gj (this j is unique by lemma 7).

Proof

One direction is easy: if h=fj and k=gj for some map j, 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 o. Put j=f ohg ok. First we check that j is a map. We have 1 yj oj 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 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 j is a map.

Finally, we have fjf(f oh)h, which implies fj=h (lemma 3). Similarly gj=k.

Corollary

Tabulations are unique up to unique isomorphism.

Proposition

A diagram in 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 of.

Proof

An identity inclusion gk=fh is certainly mated to an inclusion kh og of. Conversely, an inclusion kh og of is mated to gkfh, and we can use lemma 3.

Corollary

Given f:ac and g:bc in Map(A), a tabulation (h:pa,k:pb) of r=g of provides a pullback of (f,g).

Proof

Indeed, by definition of tabulation we then have kh o=g of, so gk=fh. For the universality of (h,k): if gk=fh, then k(h) og of, and we can apply proposition 2 to finish.

Corollary

If i:ab is a monomorphism in Map(A) and i oi has a tabulation, then i oi=1 a.

Proof

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

Lemma

If r:aa is coreflexive, then for any tabulation (f,g) of r, we have f=g and f is monic.

Proof

The inclusion gf o=r1 a is mated to gf which must be an identity g=f. If (f,g)=(f,f) is jointly monic, then f is monic.

Pretabularity and tabularity

Definition

An allegory is tabular if every morphism r:ab admits a tabulation. A unital allegory is pretabular if for all a,b, the maximal morphism ε b oε ahom(a,b) (see the last sentence of the Units section) admits a tabulation.

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

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

Lemma

In a tabular allegory A, a map q:ae is a strong epi in Map(A) if qq o=1 e.

Proof

If qq o=1 e, then it is first of all clear that q is an epi in Map(A) because it retracts q o in A. We show q is orthogonal to monomorphisms in 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 i is monic. We wish to show there exists a filler map g:eb such that gq=f and ig=j. The uniqueness of a filler map is clear since i is monic.

Put g=fq o. We first check that g is a map. Notice that the identity inclusion if=jq is mated to an inclusion fq oi oj, so we have gi oj. 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 i is monic (corollary 5). This gives the counit for gdashvg 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 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=gq by lemma 3. This completes the proof.

Theorem

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

Proof

The equalizer of a pair of maps f,g:ab may be constructed as a tabulation of the coreflexive arrow dom(fg). By lemma 8, the tabulation is of the form (h,h) where h is monic, and by an application of proposition 2, one sees it is the universal map that equalizes f and g.

For any map f:ab, consider a tabulation of the coreflexive dom(f o)=ff o:bb by a pair of maps (i,i). Notice that i:eb is monic in Map(A), and ii o=ff o. By proposition 2, there exists a unique q:ae such that f=iq. Following the proof of proposition 2, the map q is constructed as i of. 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 (q o is total). By lemma 9, this means q is a strong epi in Map(A). Thus we have factored f into a strong epi followed by a mono.

Now suppose q:ae is any strong epi and g:de is a map, and that (g:pa,q:pd) is a pullback of (g,q). Then (g,q) is a tabulation of q og, so q og=g(q) o. Now the left side of this equation is total, and therefore so is the right: 1 edom(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 q is strong epi, and we are done.

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