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:a\to b$, $s:b\to c$ as $sr:a\to c$.
An allegory is a $\mathrm{Pos}$-enriched $\u2020$-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:
$rs\wedge t\le r(s\wedge {r}^{\u2020}t)$
$rs\wedge t\le (r\wedge t{s}^{\u2020})s$
(and of course there are variations, using commutativity of $\wedge $). Each of these forms can be derived from the other, using the $\u2020$-structure.
The $\u2020$-operation, which we henceforth denote by $(-{)}^{o}$, preserves meets since it preserves order and is an involution.)
For any $r:a\to b$, we have $r\le r{r}^{o}r$.
We have $r\le r{1}_{b}\wedge r\le r(1\wedge {r}^{o}r)\le r{r}^{o}r$ where the middle inequality uses the modular law.
Recall that a map in an allegory is a morphism $f:a\to b$ such that $f\u22a3{f}^{o}$. A relation $r:a\to b$ is well-defined if we merely have a counit inclusion $r{r}^{o}\le {1}_{b}$, and is total if we merely have a unit inclusion ${1}_{a}\le {r}^{o}r$. Clearly maps are closed under composition, as are total relations and well-defined relations.
If $f:a\to b$ is a map, then for any $r,s\in \mathrm{hom}(b,c)$ we have $(r\wedge s)f=rf\wedge sf$.
The non-trivial inclusion follows from
where the first inequality is an instance of the modular law, and the second holds for any well-defined relation $f$.
If $f,g:a\to b$ are maps and $f\le g$, then $f=g$.
Since the dagger operation $(-{)}^{o}:\mathrm{hom}(a,b)\to \mathrm{hom}(b,a)$ preserves order, we have ${f}^{o}\le {g}^{o}$. But also the inclusion $f\le g$ between left adjoints is mated to an inclusion ${g}^{o}\le {f}^{o}$ between right adjoints. Hence ${f}^{o}={g}^{o}$, and therefore $f=g$.
Let $r:a\to b$ be a morphism. We define the domain $dom(r)$ to be ${1}_{a}\wedge {r}^{o}r$. A morphism $e:a\to a$ is coreflexive if $e\le {1}_{a}$; in particular, domains are coreflexive. $\mathrm{Cor}(a)$ denotes the poset of coreflexives in $\mathrm{hom}(a,a)$.
Coreflexives $r:a\to a$ are symmetric and transitive. (Symmetric and transitive imply idempotent.)
We have $r\le r{r}^{o}r\le {1}_{a}{r}^{o}{1}_{a}\le {r}^{o}$ where the first inequality is lemma 1. Of course also $rr\le {1}_{a}r=r$. (If $r$ is symmetric and transitive, then $r\le r{r}^{o}r=rrr\le rr$ as well.)
For $r,s\in \mathrm{hom}(a,b)$, we have $dom(r\wedge s)={1}_{a}\wedge {r}^{o}s$.
One inclusion is trivial:
The other inclusion follows from fairly tricky applications of the modular law:
For $r:a\to b$ and coreflexives $c\in \mathrm{hom}(a,a)$, we have $dom(r)\le c$ if and only if $r\le rc$. In particular, $r\le r\circ dom(r)$.
If ${1}_{a}\wedge {r}^{o}r\le c$, then
If $r\le rc$, then
where the antepenultimate inequality uses the modular law, and the last uses lemma 4.
For $r:a\to b$ and $s:b\to c$, we have $dom(sr)\le dom(r)$.
By lemma 6, it suffices that $sr\le sr\circ dom(r)$. But this follows from the last sentence of lemma 6.
An object $t$ is a unit in an allegory if ${1}_{t}$ is maximal in $\mathrm{hom}(t,t)$ and if for every object $a$ there is $f:a\to t$ such that ${1}_{a}\le {f}^{o}f$ (i.e., $f$ is total).
Of course by maximality we also have $f{f}^{o}\le {1}_{t}$, so such $f$ must also be a map.
We say $A$ is unital (Freyd-Scedrov say unitary) if $A$ has a unit.
Let $t$ be a unit. Then $dom:\mathrm{hom}(a,t)\to \mathrm{Cor}(a)$ is an injective order-preserving function.
Order-preservation is clear. If $r,s:a\to t$ and $dom(r)\le dom(s)$, then $r\le s$:
where the first inequality uses lemma 6, and the last inequality follows from $r{s}^{o}\le {1}_{t}$ (since ${1}_{t}$ is maximal in $\mathrm{hom}(t,t)$). Therefore $dom(r)=dom(s)$ implies $r=s$.
For a unit $t$ and any $a$, there is at most one total relation = map $r:a\to t$ (because in that case $dom(r)={1}_{a}$, and we apply the previous proposition), and this is maximal in $\mathrm{hom}(a,t)$. Thus $t$ is terminal in $\mathrm{Map}(A)$.
Let ${\epsilon}_{a}:a\to t$ denote the maximal element of $\mathrm{hom}(a,t)$. For any $r:a\to b$, we then have $r\le {\epsilon}_{b}^{o}{\epsilon}_{a}$ since this is mated to the inequality ${\epsilon}_{b}r\le {\epsilon}_{a}$. Therefore ${\epsilon}_{b}^{o}{\epsilon}_{a}$ is the maximal element of $\mathrm{hom}(a,b)$.
Recall from Categories, Allegories that a tabulation of $r:a\to b$ is a pair of maps $f:x\to a$, $g:x\to b$ such that $r=g{f}^{o}$ and ${f}^{o}f\wedge {g}^{o}g={1}_{x}$.
For maps $f:x\to a$, $g:x\to b$, the condition ${f}^{o}f\wedge {g}^{o}g={1}_{x}$ implies $(f,g)$ is a jointly monic pair in $\mathrm{Map}(A)$.
Let $h,h\prime :y\to x$ be maps, and suppose $fh=fh\prime $ and $gh=gh\prime $. If ${f}^{o}f\wedge {g}^{o}g={1}_{x}$, then
where the second and fourth equations use lemma 2.
Suppose $r:a\to b$ is tabulated by $(f:x\to a,g:x\to b)$, and suppose $h:y\to a$, $k:y\to b$ are maps. We have $k{h}^{o}\le g{f}^{o}$ if and only if there exists a map $j:y\to x$ such that $h=fj$ and $k=gj$ (this $j$ is unique by lemma 7).
One direction is easy: if $h=fj$ and $k=gj$ for some map $j$, then
In the other direction: suppose $k{h}^{o}\le g{f}^{o}$. Put $j={f}^{o}h\wedge {g}^{o}k$. First we check that $j$ is a map. We have ${1}_{y}\le {j}^{o}j$ from
using lemma 5. We have $j{j}^{o}\le {1}_{x}$ from
where the last step uses one of the tabulation conditions. So $j$ is a map.
Finally, we have $fj\le f({f}^{o}h)\le h$, which implies $fj=h$ (lemma 3). Similarly $gj=k$.
Tabulations are unique up to unique isomorphism.
A diagram in $\mathrm{Map}(A)$
commutes if and only if $k{h}^{o}\le {g}^{o}f$.
An identity inclusion $gk=fh$ is certainly mated to an inclusion $k{h}^{o}\le {g}^{o}f$. Conversely, an inclusion $k{h}^{o}\le {g}^{o}f$ is mated to $gk\le fh$, and we can use lemma 3.
Given $f:a\to c$ and $g:b\to c$ in $\mathrm{Map}(A)$, a tabulation $(h:p\to a,k:p\to b)$ of $r={g}^{o}f$ provides a pullback of $(f,g)$.
Indeed, by definition of tabulation we then have $k{h}^{o}={g}^{o}f$, so $gk=fh$. For the universality of $(h,k)$: if $gk\prime =fh\prime $, then $k(h\prime {)}^{o}\le {g}^{o}f$, and we can apply proposition 2 to finish.
If $i:a\to b$ is a monomorphism in $\mathrm{Map}(A)$ and ${i}^{o}i$ has a tabulation, then ${i}^{o}i={1}_{a}$.
The tabulation of ${i}^{o}i$ gives a pullback of the pair $(i,i)$, but since this pullback is already $({1}_{a},{1}_{a})$, the conclusion is clear.
If $r:a\to a$ is coreflexive, then for any tabulation $(f,g)$ of $r$, we have $f=g$ and $f$ is monic.
The inclusion $g{f}^{o}=r\le {1}_{a}$ is mated to $g\le f$ which must be an identity $g=f$. If $(f,g)=(f,f)$ is jointly monic, then $f$ is monic.
An allegory is tabular if every morphism $r:a\to b$ admits a tabulation. A unital allegory is pretabular if for all $a,b$, the maximal morphism ${\epsilon}_{b}^{o}{\epsilon}_{a}\in \mathrm{hom}(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 $\mathrm{Map}(A)$ has pullbacks.
Likewise, it is immediate from the preceding corollary that if $A$ is unital and pretabular, then $\mathrm{Map}(A)$ has products, because we can form the pullback of the maps ${\epsilon}_{a}:a\to t$, ${\epsilon}_{b}:b\to t$ to the terminal object $t$.
In a tabular allegory $A$, a map $q:a\to e$ is a strong epi in $\mathrm{Map}(A)$ if $q{q}^{o}={1}_{e}$.
If $q{q}^{o}={1}_{e}$, then it is first of all clear that $q$ is an epi in $\mathrm{Map}(A)$ because it retracts ${q}^{o}$ in $A$. We show $q$ is orthogonal to monomorphisms in $\mathrm{Map}(A)$. That is, consider a commutative diagram
where $i$ is monic. We wish to show there exists a filler map $g:e\to b$ such that $gq=f$ and $ig=j$. The uniqueness of a filler map is clear since $i$ is monic.
Put $g=f{q}^{o}$. We first check that $g$ is a map. Notice that the identity inclusion $if=jq$ is mated to an inclusion $f{q}^{o}\le {i}^{o}j$, so we have $g\le {i}^{o}j$. In that case we have
where the last inclusion holds because $i$ is monic (corollary 5). This gives the counit for $gdashv{g}^{o}$. For the unit, use
So $g=f{q}^{o}$ is a map. We also have
and finally we have
so that $f=gq$ by lemma 3. This completes the proof.
If $A$ is tabular, then $\mathrm{Map}(A)$ has equalizers. Moreover, every map has a (strong epi)-mono factorization, and strong epis are preserved by pullbacks. In short, $\mathrm{Map}(A)$ is a locally regular category. If $A$ is moreover unital, then $\mathrm{Map}(A)$ is regular.
The equalizer of a pair of maps $f,g:a\to b$ may be constructed as a tabulation of the coreflexive arrow $dom(f\wedge g)$. 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:a\to b$, consider a tabulation of the coreflexive $dom({f}^{o})=f{f}^{o}:b\to b$ by a pair of maps $(i,i)$. Notice that $i:e\to b$ is monic in $\mathrm{Map}(A)$, and $i{i}^{o}=f{f}^{o}$. By proposition 2, there exists a unique $q:a\to e$ such that $f=iq$. Following the proof of proposition 2, the map $q$ is constructed as ${i}^{o}f$. We have
i.e., $dom({q}^{o})={1}_{e}$ (${q}^{o}$ is total). By lemma 9, this means $q$ is a strong epi in $\mathrm{Map}(A)$. Thus we have factored $f$ into a strong epi followed by a mono.
Now suppose $q:a\to e$ is any strong epi and $g:d\to e$ is a map, and that $(g\prime :p\to a,q\prime :p\to d)$ is a pullback of $(g,q)$. Then $(g\prime ,q\prime )$ is a tabulation of ${q}^{o}g$, so ${q}^{o}g=g\prime (q\prime {)}^{o}$. Now the left side of this equation is total, and therefore so is the right: ${1}_{e}\le dom(g\prime (q\prime {)}^{o})$. But then
where the second inequality uses corollary 1. This means $q\prime $ is strong epi, and we are done.