Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A bicategory of relations is a (1,2)-category which behaves like the 2-category of internal relations in a regular category. The notion is due to Carboni and Walters.
[Note: in this article, the direction of composition is diagrammatic (i.e., anti-Leibniz).]
A bicategory of relations is a cartesian bicategory which is locally posetal and moreover in which for every object $X$, the diagonal $\Delta\colon X\to X\otimes X$ and codiagonal $\nabla\colon X\otimes X\to X$ satisfy the Frobenius condition:
Of course, in the locally posetal case the definition of cartesian bicategory simplifies greatly: it amounts to a symmetric monoidal Pos-enriched category for which every object carries a commutative comonoid structure, for which the structure maps $\Delta_X: X \to X \otimes X$, $\varepsilon_X: X \to 1$ are left adjoint 1-morphisms, and for which every morphism $R: X \to Y$ is a colax morphism of comonoids in the sense that the following inequalities hold:
We remark that such structure is unique when it exists (being a cartesian bicategory is a property of, as opposed to structure on, a bicategory). The tensor product $\otimes$ behaves like the ordinary product of relations. Note this is not a cartesian product in the sense of the usual universal property; nevertheless, it is customary to write it as a product $\times$, and we follow this custom below. It does become a cartesian product if one restricts to the subcategory of left adjoints (called maps), which should be thought of as functional relations.
We record a few consequences of this notion.
(Separability condition) $\Delta\nabla = 1$.
In one direction, we have the 2-cell $1 \leq \Delta\nabla$ which is the unit of the adjunction $\Delta \dashv \Delta_* = \nabla$. In the other direction, there is an adjunction $\varepsilon \dashv \varepsilon_*$ between the counit and its dual, and the unit of this adjunction is a 2-cell $1 \leq \varepsilon\varepsilon_*$, from which we derive
where the last equation follows from the equation $\Delta(1 \times \varepsilon) = 1$ and its dual $(1 \times \varepsilon_*)\Delta_* = 1$.
(Dual Frobenius condition) $\nabla \Delta = (\Delta \times 1)(1 \times \nabla)$.
The locally full subcategory whose 1-cells are maps (= left adjoints) has finite products, in particular a symmetry involution $\sigma$ for which
Additionally, the right adjoint $\sigma_{X Y *}$ is the inverse $\sigma_{X Y}^{-1} = \sigma_{Y X}$. Hence the equation above is mated to $\sigma_{X X} \nabla_X = \nabla_X$, and we calculate
which gives the dual equation.
In a bicategory of relations, each object is dual to itself, making the bicategory a compact closed bicategory.
Both the unit and counit of the desired adjunction $X \dashv X$ are given by equality predicates:
One of the triangular equations follows from the commutative diagram
where the square expresses a Frobenius equation. The other triangular equation uses the dual Frobenius equation.
The compact closure allows us to define the opposite of a relation $R: X \to Y$ as the 1-morphism mate:
In this way, a bicategory of relations becomes a †-compact $Pos$-enriched category.
Recall (again) that a map in the bicategory of relations is the same as a 1-cell that has a right adjoint.
If $f \colon X \to Y$ is a map, then $f$ is a strict morphism of comonoids.
If $g$ is the right adjoint of $f$, we have $\Delta_X g \leq (g \times g)\Delta_Y$ since $g$, like any morphism, is a lax comonoid morphism. But this 2-cell is mated to a 2-cell $(f \times f)\Delta_X \to \Delta_Y f$, inverse to the 2-cell $\Delta_Y f \to (f \times f)\Delta_X$ that comes for free. So $f$ preserves comultiplication strictly. A similar argument shows $f$ preserves the counit strictly.
If $f \colon X \to Y$ is a map, then $f^{op}: Y \to X$ equals the right adjoint $f_\ast$.
The proof is much more perspicuous if we use string diagrams. But the key steps are given in two strings of equalities and inequalities. The first gives a counit for $f \dashv f^{op}$, and the second gives a unit. We have
where (0) uses the definition of $f^{op}$, (1) uses properties of monoidal categories, (2) uses the fact that $f$ strictly preserves comultiplication, (3) is mated to the fact that $f$ laxly preserves the counit, (4) is a Frobenius condition, and (5) uses comonoid and dual monoid laws. We can also “almost” run the same calculation backwards to get the unit:
where (0) uses comonoid and dual monoid laws, (1) uses a Frobenius condition, (2) uses the fact that $f$ preserves the counit, (3) is mated to the fact that $f$ laxly preserves comultiplication, (4) uses properties of monoidal categories, and (5) uses the definition of $f^{op}$.
In fact, what this proof really proves is a converse of the earlier proposition:
If $f$ is a strict comonoid morphism, then $f$ has a right adjoint: $f \dashv f^{op}$.
If $f, g: X \to Y$ are maps and $f \leq g$, then $f = g$. Thus, the locally full subcategory whose morphisms are maps is locally discrete (the hom-posets are discrete).
A 2-cell inequality $\alpha: f \leq g$ is mated to a inequality $\alpha_*: g_* \leq f_*$. On the other hand, whiskering $1_Y \times \alpha \times 1_X$ with $1_Y \times \eta_X$ and $\theta_Y \times 1_X$, as in the construction of opposites above, gives $\alpha^{op}: f^{op} \leq g^{op}$. Since $f^{op} = f_*$ and $g^{op} = g_*$, we obtain $f^{op} = g^{op}$, and because $f^{op op} = f$, we obtain $f = g$.
Bicategories of relations $\mathbf{B}$ satisfy a Beck-Chevalley condition, as follows. Let $Prod(B_0)$ denote the free category with finite products generated by the set of objects of $\mathbf{B}$. According to the results at free cartesian category, $Prod(B_0)$ is finitely complete.
Since $Map(\mathbf{B})$ has finite products, there is a product-preserving functor $\pi: Prod(B_0) \to \Map(\mathbf{B})$ which is the identity on objects. Again, according to the results of free cartesian category, we have the following result.
If a diagram in $Prod(B_0)$ is a pullback square, then application of $\pi$ to that diagram is a pullback square in $Map(\mathbf{B})$.
Let us call pullback squares of this form in $Map(\mathbf{B})$ product-based pullback squares.
Given a product-based pullback square
in $Map(\mathbf{B})$, the Beck-Chevalley condition holds: $h_* k = f g_*$.
See Brady-Trimble for further details. The critical case to consider is the pullback square
where the Beck-Chevalley condition is exactly the Frobenius condition.
One way of interpreting this result is by viewing $\mathbf{B}$ as a hyperdoctrine or monoidal fibration over $Prod(B_0)$, where the fiber over an object $B$ is the local hom-poset $\hom(B, 1)$. Each $f: A \to B$ in the base induces a pullback functor, by precomposing $R: B \to 1$ with $\pi(f): A \to B$ in $Map(\mathbf{B})$. Existential quantification is interpreted by precomposing with right adjoints $\pi(f)_*$. The Beck-Chevalley condition exerts compatibility between quantification and pullback/substitution functors.
Any bicategory of relations is an allegory. Recall that an allegory is a $Pos$-enriched $\dagger$-category whose local homs are meet-semilattices, satisfying Freyd’s modular law:
A proof of the modular law is given in the blog post by R.F.C. (“Bob”) Walters referenced below.
In fact, we may prove a little more:
The notion of bicategory of relations is equivalent to the notion of unitary pretabular allegory.
A bicategory of relations has a unit $1$ in the sense of allegories:
$1$ is a partial unit: we have $\varepsilon_1 = id_1: 1 \to 1$, and for any $R: 1 \to 1$ we have $R = R\varepsilon_1 \leq \varepsilon_1 = id_1$.
Any object $X$ is the source of a map $\varepsilon_X: X \to 1$, which being a map is entire. Thus $1$ is a unit.
A bicategory of relations is also pretabular, for the maximal element in $\hom(X, Y)$ is tabulated as $(\pi_X)_* \pi_Y$, where $\pi_X$, $\pi_Y$ are the product projections for $X \times Y$.
In the other direction, suppose $\mathbf{A}$ is a unitary pretabular allegory. There is a faithful embedding, which preserves the unit, of $\mathbf{A}$ into its coreflexive splitting, which is unitary and tabular, and hence equivalent to $Rel$ of the regular category $Map(\mathbf{A})$. By the proposition below, then, $\mathbf{A}$ is a full sub-2-category of a bicategory of relations. Because the product of two Frobenius objects is again Frobenius, it suffices to show that $\mathbf{A}$ is closed under products in its coreflexive splitting. The inclusion of $\mathbf{A}$ into the latter preserves the unit and the property of being a map, and hence preserves top elements of hom sets, while any allegory functor must preserve tabulations. So the tabulation $(\pi^{X Y}_X, \pi^{X Y}_Y)$ of $\top_{X Y}$ in $\mathbf{A}$ is a tabulation of $\top_{1_X 1_Y}$ in the coreflexive splitting, and hence $1_{X \times Y} \cong 1_X \times 1_Y$.
If $C$ is a regular category, then the bicategory $Rel C$ of relations in $C$ is a bicategory of relations.
By theorem 1.6 of Carboni–Walters, $\mathbf{A}$ is a Cartesian bicategory if:
$Map(\mathbf{A})$ has finite products.
$\mathbf{A}$ has local finite products, and $id_1$ is the top element of $\mathbf{A}(1,1)$.
The tensor product defined as
is functorial, where $p$ and $p'$ are the appropriate product projections.
The first two are obvious, and for the third we may reason in the internal language of $C$. Clearly
The formula whose meaning is by $R S \otimes R' S'$ is
and we may use Frobenius reciprocity to get
which is the meaning of $(R \otimes R')(S \otimes S')$. Finally, the Frobenius law is
which follows from transitivity and symmetry of equality.
Other attempted axiomatizations of the same idea “something that acts like the category of relations in a regular category” include:
Carboni and Walters, “Cartesian Bicategories, I”
blog post showing that any bicategory of relations is an allegory. Indeed, a bicategory of relations is equivalent to a unitary pretabular allegory.