nLab
bicategory 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 :X\to X\otimes X$ and codiagonal $\nabla :X\otimes X\to X$ satisfy the Frobenius condition:

$$\nabla \Delta =(1\otimes \Delta )(\nabla \otimes 1).$$\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$, ${\epsilon }_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\le {\Delta }_{X\otimes X}(R\otimes R),R{\epsilon }_Y\le {\epsilon }_X.$$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\le \Delta \nabla$ which is the unit of the adjunction $\Delta ⊣{\Delta }_{*}=\nabla$. In the other direction, there is an adjunction $\epsilon ⊣{\epsilon }_{*}$ between the counit and its dual, and the unit of this adjunction is a 2-cell $1\le \epsilon {\epsilon }_{*}$, from which we derive

$$\Delta \nabla =\Delta {\Delta }_{*}\le \Delta (1\times \epsilon )(1\times {\epsilon }_{*}){\Delta }_{*}=1$$\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 \epsilon )=1$ and its dual $(1\times {\epsilon }_{*}){\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 }_{XX}={\Delta }_X$$\Delta_X \sigma_{X X} = \Delta_X

Additionally, the right adjoint ${\sigma }_{XY*}$ is the inverse ${\sigma }_{XY}^{-1}={\sigma }_{YX}$. Hence the equation above is mated to ${\sigma }_{XX}{\nabla }_X={\nabla }_X$, and we calculate

$$\begin{array}{ccc}{\nabla }_X{\Delta }_X& =& {\sigma }_{XX}{\nabla }_X{\Delta }_X{\sigma }_{XX}\\ & =& {\sigma }_{XX}(1\times {\Delta }_X)({\nabla }_X\times 1){\sigma }_{XX}\\ & =& ({\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 }_{XX}\times 1)(1\times {\sigma }_{XX})(1\times {\nabla }_X)\\ & =& ({\Delta }_X\times 1_X)(1_X\times {\nabla }_X)\end{array}$$\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⊣X$ are given by equality predicates:

$${\eta }_X=(1\stackrel{{\epsilon }_{*}}{\to }X\stackrel{\Delta }{\to }X\times X){\theta }_X=(X\times X\stackrel{\nabla }{\to }X\stackrel{\epsilon }{\to }1)$$\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

$$\begin{array}{ccccc}X& \stackrel{1\times {\epsilon }_{*}}{\to }& X\times X& \stackrel{1\times \Delta }{\to }& X\times X\times X\\ & {}_1\searrow & \downarrow \nabla & & \downarrow \nabla \times 1\\ & & X& \stackrel{\Delta }{\to }& X\times X\\ & & & {}_1\searrow & \downarrow \epsilon \times 1\\ & & & & X\end{array}$$\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^{\mathrm{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)$$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 $\mathrm{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: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\le (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:X\to Y$ is a map, then $f^{\mathrm{op}}:Y\to X$ equals the right adjoint $f_{*}$.

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⊣f^{\mathrm{op}}$, and the second gives a unit. We have

$$\begin{array}{ccc}f{f}^{\mathrm{op}}& \stackrel{0}{=}& f\circ ({\epsilon }_Y\times 1)({\nabla }_Y\times 1)(1\times f\times 1)(1\times {\Delta }_X)(1\times {\epsilon }_X{}_{*})\\ & \stackrel{1}{=}& ({\epsilon }_Y\times 1)({\nabla }_Y\times 1)(1\times f\times f)(1\times {\Delta }_X)(1\times {\epsilon }_X{}_{*})\\ & \stackrel{2}{=}& ({\epsilon }_Y\times 1)({\nabla }_Y\times 1)(1\times {\Delta }_Y)(1\times f)(1\times {\epsilon }_X{}_{*})\\ & \stackrel{3}{\le }& ({\epsilon }_Y\times 1)({\nabla }_Y\times 1)(1\times {\Delta }_Y)(1\times {\epsilon }_Y{}_{*})\\ & \stackrel{4}{=}& ({\epsilon }_Y\times 1){\Delta }_Y{\nabla }_Y(1\times {\epsilon }_Y{}_{*})\\ & \stackrel{5}{=}& 1_Y\end{array}$$\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^{\mathrm{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:

$$\begin{array}{ccc}{1}_X& \stackrel{0}{=}& ({\epsilon }_X\times 1){\Delta }_X{\nabla }_X(1\times {\epsilon }_X{}_{*})\\ & \stackrel{1}{=}& ({\epsilon }_X\times 1)({\nabla }_X\times 1)(1\times {\Delta }_X)(1\times {\epsilon }_X{}_{*})\\ & \stackrel{2}{=}& ({\epsilon }_Y\times 1)(f\times 1)({\nabla }_X\times 1)(1\times {\Delta }_X)(1\times {\epsilon }_X{}_{*})\\ & \stackrel{3}{\le }& ({\epsilon }_Y\times 1)({\nabla }_Y\times 1)(f\times f\times 1)(1\times {\Delta }_X)(1\times {\epsilon }_X{}_{*})\\ & \stackrel{4}{=}& ({\epsilon }_Y\times 1)({\nabla }_Y\times 1)(1\times f\times 1)(1\times {\Delta }_X)(1\times {\epsilon }_X{}_{*})\circ f\\ & \stackrel{5}{=}& f^{\mathrm{op}}f\end{array}$$\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^{\mathrm{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⊣f^{\mathrm{op}}$.

Proposition

If $f,g:X\to Y$ are maps and $f\le 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\le g$ is mated to a inequality ${\alpha }_{*}:g_{*}\le 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 }^{\mathrm{op}}:f^{\mathrm{op}}\le g^{\mathrm{op}}$. Since $f^{\mathrm{op}}=f_{*}$ and $g^{\mathrm{op}}=g_{*}$, we obtain $f^{\mathrm{op}}=g^{\mathrm{op}}$, and because $f^{\mathrm{op}\mathrm{op}}=f$, we obtain $f=g$.

The Beck-Chevalley condition

Bicategories of relations $B$ satisfy a Beck-Chevalley condition, as follows. Let $\mathrm{Prod}(B_0)$ denote the free category with finite products generated by the set of objects of $B$. According to the results at free cartesian category, $\mathrm{Prod}(B_0)$ is finitely complete.

Since $\mathrm{Map}(B)$ has finite products, there is a product-preserving functor $\pi :\mathrm{Prod}(B_0)\to Map(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 $\mathrm{Prod}(B_0)$ is a pullback square, then application of $\pi$ to that diagram is a pullback square in $\mathrm{Map}(B)$.

Let us call pullback squares of this form in $\mathrm{Map}(B)$ product-based pullback squares.

Proposition

Given a product-based pullback square

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

in $\mathrm{Map}(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

$$\begin{array}{ccc}X& \stackrel{\Delta }{\to }& X\times X\\ \Delta \downarrow & & \downarrow \Delta \times 1\\ X\times X& \underset{1\times \Delta }{\to }& X\times X\times X\end{array}$$\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 $B$ as a hyperdoctrine or monoidal fibration over $\mathrm{Prod}(B_0)$, where the fiber over an object $B$ is the local hom-poset $\mathrm{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 $\mathrm{Map}(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 $\mathrm{Pos}$-enriched $†$-category whose local homs are meet-semilattices, satisfying Freyd’s modular law:

$$RS\cap T\le (R\cap T{S}^{\mathrm{op}})S$$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 ${\epsilon }_1={\mathrm{id}}_1:1\to 1$, and for any $R:1\to 1$ we have $R=R{\epsilon }_1\le {\epsilon }_1={\mathrm{id}}_1$.

• Any object $X$ is the source of a map ${\epsilon }_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 $\mathrm{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 $A$ is a unitary pretabular allegory. There is a faithful embedding, which preserves the unit, of $A$ into its coreflexive splitting, which is unitary and tabular, and hence equivalent to $\mathrm{Rel}$ of the regular category $\mathrm{Map}(A)$. By the proposition below, then, $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 $A$ is closed under products in its coreflexive splitting. The inclusion of $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^{XY},{\pi }_Y^{XY})$ of ${\top }_{XY}$ in $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 $\mathrm{Rel}C$ of relations in $C$ is a bicategory of relations.

Proof

By theorem 1.6 of Carboni–Walters, $A$ is a Cartesian bicategory if:

• $\mathrm{Map}(A)$ has finite products.

• $A$ has local finite products, and ${\mathrm{id}}_1$ is the top element of $A(1,1)$.

• The tensor product defined as

  $$R\otimes S=(pR{p}_{*})\cap (p\prime Sp{\prime }_{*})$$R \otimes S = (p R p_*) \cap (p' S p'_*)

  is functorial, where $p$ and $p\prime$ 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\prime =x\prime ]=1$$1 \otimes 1 = [x = x \wedge x' = x'] = 1

The formula whose meaning is by $RS\otimes R\prime S\prime$ is

$$(\exists y.Rxy\wedge Syz)\wedge (\exists y\prime .R\prime x\prime y\prime \wedge S\prime y\prime z\prime )$$(\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{array}{rl}& \exists y.(Rxy\wedge Syz\wedge y^{*}\exists y\prime .R\prime x\prime y\prime \wedge S\prime y\prime z\prime )\\ & \equiv \exists y.(Rxy\wedge Syz\wedge \exists y\prime .y^{*}(R\prime x\prime y\prime \wedge S\prime y\prime z\prime ))\\ & \equiv \exists y,y\prime .Rxy\wedge Syz\wedge R\prime x\prime y\prime \wedge S\prime y\prime z\prime \\ \end{array}$$\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\prime )(S\otimes S\prime )$. Finally, the Frobenius law is

$$[\exists x\prime .(x_1,x_2)=(x\prime ,x\prime )=(x_3,x_4)]=[\exists x\prime .(x_1,x\prime )=(x_3,x_3)\wedge (x_2,x_2)=(x_4,x\prime )]$$[\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.

See also

Other attempted axiomatizations of the same idea “something that acts like the category of relations in a regular category” include:

• allegories

• 1-category equipped with relations

References

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