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.
2017 article on Knowledge Representation in Bicategories of Relations by Evan Patterson, shows how one can model RDF (Resource Description Framework) and parts of OWL (Ontology Web Language) in bicategories of relations, whose internal logic is regular logic. He ends by showing how one can extend these to distributive bicategories of relations? whose internal logic is coherent logic, which is equivalent in expressivity to first order logic.
Last revised on January 22, 2020 at 11:41:41. See the history of this page for a list of all contributions to it.