# nLab bicategory of relations

Bicategories of relations

## In higher category theory

#### 2-Category theory

2-category theory

Definitions

Transfors between 2-categories

Morphisms in 2-categories

Structures in 2-categories

Limits in 2-categories

Structures on 2-categories

# Bicategories of relations

## Idea

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.

## Definition

[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:

$\nabla\Delta = (1\otimes \Delta)(\nabla \otimes 1).$

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:

$R \Delta_Y \leq \Delta_{X \otimes X} (R \otimes R), \qquad R \varepsilon_Y \leq \varepsilon_X.$

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.

## Properties

We record a few consequences of this notion.

###### Proposition

(Separability condition) $\Delta\nabla = 1$.

###### Proof

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

$\Delta\nabla = \Delta\Delta_* \leq \Delta (1 \times \varepsilon)(1 \times \varepsilon_*)\Delta_* = 1$

where the last equation follows from the equation $\Delta(1 \times \varepsilon) = 1$ and its dual $(1 \times \varepsilon_*)\Delta_* = 1$.

###### Proposition

(Dual Frobenius condition) $\nabla \Delta = (\Delta \times 1)(1 \times \nabla)$.

###### Proof

The locally full subcategory whose 1-cells are maps (= left adjoints) has finite products, in particular a symmetry involution $\sigma$ for which

$\Delta_X \sigma_{X X} = \Delta_X$

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

$\array{ \nabla_X \Delta_X & = & \sigma_{X X}\nabla_X \Delta_X \sigma_{X X} \\ & = & \sigma_{X X} (1 \times \Delta_X)(\nabla_X \times 1) \sigma_{X X} \\ & = & (\Delta_X \times 1_X) \sigma_{X \times X, X} \sigma_{X \times X, X} (1_X \times \nabla_X) \\ & = & (\Delta_X \times 1_X) (\sigma_{X X} \times 1) (1 \times \sigma_{X X}) (1 \times \nabla_X) \\ & = & (\Delta_X \times 1_X)(1_X \times \nabla_X) }$

which gives the dual equation.

###### Theorem

In a bicategory of relations, each object is dual to itself, making the bicategory a compact closed bicategory.

###### Proof

Both the unit and counit of the desired adjunction $X \dashv X$ are given by equality predicates:

$\eta_X = (1 \stackrel{\varepsilon_*}{\to} X \stackrel{\Delta}{\to} X \times X) \qquad \theta_X = (X \times X \stackrel{\nabla}{\to} X \stackrel{\varepsilon}{\to} 1)$

One of the triangular equations follows from the commutative diagram

$\array{ X & \stackrel{1 \times \varepsilon_*}{\to} & X \times X & \stackrel{1 \times \Delta}{\to} & X \times X \times X \\ & {}_1\searrow & \downarrow \mathrlap{\nabla} & & \downarrow \mathrlap{\nabla \times 1} \\ & & X & \overset{\Delta}{\to} & X \times X \\ & & & {}_{1}\searrow & \downarrow \mathrlap{\varepsilon \times 1} \\ & & & & X }$

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:

$R^{op} = (Y \stackrel{1_Y \times \eta_X}{\to} Y \times X \times X \stackrel{1_Y \times R \times 1_X}{\to} Y \times Y \times X \stackrel{\theta_Y \times 1_X}{\to} X)$

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.

###### Proposition

If $f \colon X \to Y$ is a map, then $f$ is a strict morphism of comonoids.

###### Proof

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.

###### Proposition

If $f \colon X \to Y$ is a map, then $f^{op}: Y \to X$ equals the right adjoint $f_\ast$.

###### Proof

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

$\array{ f f^{op} & \stackrel{0}{=} & f \circ (\varepsilon_Y \times 1)(\nabla_Y\times 1)(1 \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{1}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times f \times f)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{2}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times \Delta_Y)(1 \times f)(1 \times \varepsilon_X_\ast)\\ & \stackrel{3}{\leq} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times \Delta_Y)(1 \times \varepsilon_Y_\ast) \\ & \stackrel{4}{=} & (\varepsilon_Y \times 1)\Delta_Y \nabla_Y(1 \times \varepsilon_Y_\ast) \\ & \stackrel{5}{=} & 1_Y }$

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:

$\array{ 1_X & \stackrel{0}{=} & (\varepsilon_X \times 1)\Delta_X \nabla_X(1 \times \varepsilon_X_\ast) \\ & \stackrel{1}{=} & (\varepsilon_X \times 1)(\nabla_X \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{2}{=} & (\varepsilon_Y \times 1)(f \times 1)(\nabla_X\times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{3}{\leq} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(f \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \\ & \stackrel{4}{=} & (\varepsilon_Y \times 1)(\nabla_Y \times 1)(1 \times f \times 1)(1 \times \Delta_X)(1 \times \varepsilon_X_\ast) \circ f \\ & \stackrel{5}{=} & f^{op} f }$

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:

###### Proposition

If $f$ is a strict comonoid morphism, then $f$ has a right adjoint: $f \dashv f^{op}$.

###### Proposition

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

###### Proof

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

## The Beck-Chevalley condition

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.

###### Lemma

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.

###### Proposition

Given a product-based pullback square

$\array{ W & \stackrel{h}{\to} & X \\ k \downarrow & & \downarrow f \\ Y & \underset{g}{\to} & Z }$

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

$\array{ X & \overset{\Delta}{\to} & X \times X \\ \mathllap{\Delta} \downarrow & & \downarrow \mathrlap{\Delta \times 1} \\ X \times X & \underset{1 \times \Delta}{\to} & X \times X \times X }$

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.

## Relation to allegories

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:

$R S \cap T \leq (R \cap T S^{op})S$

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:

###### Theorem

The notion of bicategory of relations is equivalent to the notion of unitary pretabular allegory.

###### Proof

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

###### Proposition

If $C$ is a regular category, then the bicategory $Rel C$ of relations in $C$ is a bicategory of relations.

###### Proof

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

$R \otimes S = (p R p_*) \cap (p' S p'_*)$

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

$1 \otimes 1 = [x = x \wedge x' = x'] = 1$

The formula whose meaning is by $R S \otimes R' S'$ is

$(\exists y. R x y \wedge S y z) \wedge (\exists y'. R' x' y' \wedge S' y' z')$

and we may use Frobenius reciprocity to get

\begin{aligned} & \exists y. (R x y \wedge S y z \wedge y^* \exists y'. R' x' y' \wedge S' y' z') \\ & \equiv \exists y. (R x y \wedge S y z \wedge \exists y'. y^* (R' x' y' \wedge S' y' z')) \\ & \equiv \exists y, y'. R x y \wedge S y z \wedge R' x' y' \wedge S' y' z' \\ \end{aligned}

which is the meaning of $(R \otimes R')(S \otimes S')$. Finally, the Frobenius law is

$[\exists x'. (x_1, x_2) = (x', x') = (x_3, x_4)] = [\exists x'. (x_1, x') = (x_3, x_3) \wedge (x_2, x_2) = (x_4, x')]$

which follows from transitivity and symmetry of equality.