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 , as .
An allegory is a -enriched -category 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 , preserves meets since it preserves order and is an involution.)
For any , we have .
We have where the middle inequality uses the modular law.
Recall that a map in an allegory is a morphism such that . A relation is well-defined if we merely have a counit inclusion , and is total if we merely have a unit inclusion . Clearly maps are closed under composition, as are total relations and well-defined relations.
If is a map, then for any we have .
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 .
If are maps and , then .
Since the dagger operation preserves order, we have . But also the inclusion between left adjoints is mated to an inclusion between right adjoints. Hence , and therefore .
Domains and coreflexives
Let be a morphism. We define the domain to be . A morphism is coreflexive if ; in particular, domains are coreflexive. denotes the poset of coreflexives in .
Coreflexives are symmetric and transitive. (Symmetric and transitive imply idempotent.)
We have where the first inequality is lemma 1. Of course also . (If is symmetric and transitive, then as well.)
For , we have .
One inclusion is trivial:
The other inclusion follows from fairly tricky applications of the modular law:
For and coreflexives , we have if and only if . In particular, .
If , then
If , then
where the antepenultimate inequality uses the modular law, and the last uses lemma 4.
For and , we have .
By lemma 6, it suffices that . But this follows from the last sentence of lemma 6.
An object is a unit in an allegory if is maximal in and if for every object there is such that (i.e., is total).
Of course by maximality we also have , so such must also be a map.
We say is unital (Freyd-Scedrov say unitary) if has a unit.
Let be a unit. Then is an injective order-preserving function.
Order-preservation is clear. If and , then :
where the first inequality uses lemma 6, and the last inequality follows from (since is maximal in ). Therefore implies .
For a unit and any , there is at most one total relation = map (because in that case , and we apply the previous proposition), and this is maximal in . Thus is terminal in .
Let denote the maximal element of . For any , we then have since this is mated to the inequality . Therefore is the maximal element of .
Tabulations in allegories
Recall from Categories, Allegories that a tabulation of is a pair of maps , such that and .
Preliminaries on tabulations
For maps , , the condition implies is a jointly monic pair in .
Let be maps, and suppose and . If , then
where the second and fourth equations use lemma 2.
Suppose is tabulated by , and suppose , are maps. We have if and only if there exists a map such that and (this is unique by lemma 7).
One direction is easy: if and for some map , then
In the other direction: suppose . Put . First we check that is a map. We have from
If is tabular, then has equalizers. Moreover, every map has a (strong epi)-mono factorization, and strong epis are preserved by pullbacks. In short, is a locally regular category. If is moreover unital, then is regular.
The equalizer of a pair of maps may be constructed as a tabulation of the coreflexive arrow . By lemma 8, the tabulation is of the form where is monic, and by an application of proposition 2, one sees it is the universal map that equalizes and .
For any map , consider a tabulation of the coreflexive by a pair of maps . Notice that is monic in , and . By proposition 2, there exists a unique such that . Following the proof of proposition 2, the map is constructed as . We have
i.e., ( is total). By lemma 9, this means is a strong epi in . Thus we have factored into a strong epi followed by a mono.
Now suppose is any strong epi and is a map, and that is a pullback of . Then is a tabulation of , so . Now the left side of this equation is total, and therefore so is the right: . But then
where the second inequality uses corollary 1. This means is strong epi, and we are done.