nLab bicategory of relations

Bicategories of relations

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 XX, the diagonal Δ:XXX\Delta\colon X\to X\otimes X and codiagonal :XXX\nabla\colon X\otimes X\to X satisfy the Frobenius condition:

Δ=(1Δ)(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 Δ X:XXX\Delta_X: X \to X \otimes X, ε X:X1\varepsilon_X: X \to 1 are left adjoint 1-morphisms, and for which every morphism R:XYR: X \to Y is a colax morphism of comonoids in the sense that the following inequalities hold:

RΔ YΔ XX(RR),Rε Yε 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) Δ=1\Delta\nabla = 1.

Proof

In one direction, we have the 2-cell 1Δ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εε *1 \leq \varepsilon\varepsilon_*, from which we derive

Δ=ΔΔ *Δ(1×ε)(1×ε *)Δ *=1\Delta\nabla = \Delta\Delta_* \leq \Delta (1 \times \varepsilon)(1 \times \varepsilon_*)\Delta_* = 1

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

Proposition

(Dual Frobenius condition) Δ=(Δ×1)(1×)\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

Δ Xσ XX=Δ X\Delta_X \sigma_{X X} = \Delta_X

Additionally, the right adjoint σ XY*\sigma_{X Y *} is the inverse σ XY 1=σ YX\sigma_{X Y}^{-1} = \sigma_{Y X}. Hence the equation above is mated to σ XX X= X\sigma_{X X} \nabla_X = \nabla_X, and we calculate

XΔ X = σ XX XΔ Xσ XX = σ XX(1×Δ X)( X×1)σ XX = (Δ X×1 X)σ X×X,Xσ X×X,X(1 X× X) = (Δ X×1 X)(σ XX×1)(1×σ XX)(1× X) = (Δ X×1 X)(1 X× X)\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 XXX \dashv X are given by equality predicates:

η X=(1ε *XΔX×X)θ X=(X×XXε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

X 1×ε * X×X 1×Δ X×X×X 1 ×1 X Δ X×X 1 ε×1 X\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:XYR: X \to Y as the 1-morphism mate:

R op=(Y1 Y×η XY×X×X1 Y×R×1 XY×Y×Xθ Y×1 XX)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 PosPos-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:XYf \colon X \to Y is a map, then ff is a strict morphism of comonoids.

Proof

If gg is the right adjoint of ff, we have Δ Xg(g×g)Δ Y\Delta_X g \leq (g \times g)\Delta_Y since gg, like any morphism, is a lax comonoid morphism. But this 2-cell is mated to a 2-cell (f×f)Δ XΔ Yf(f \times f)\Delta_X \to \Delta_Y f, inverse to the 2-cell Δ Yf(f×f)Δ X\Delta_Y f \to (f \times f)\Delta_X that comes for free. So ff preserves comultiplication strictly. A similar argument shows ff preserves the counit strictly.

Proposition

If f:XYf \colon X \to Y is a map, then f op:YXf^{op}: Y \to X equals the right adjoint f *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 ff opf \dashv f^{op}, and the second gives a unit. We have

ff op =0 f(ε Y×1)( Y×1)(1×f×1)(1×Δ X)(1×ε X*) =1 (ε Y×1)( Y×1)(1×f×f)(1×Δ X)(1×ε X*) =2 (ε Y×1)( Y×1)(1×Δ Y)(1×f)(1×ε X*) 3 (ε Y×1)( Y×1)(1×Δ Y)(1×ε Y*) =4 (ε Y×1)Δ Y Y(1×ε Y*) =5 1 Y\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 opf^{op}, (1) uses properties of monoidal categories, (2) uses the fact that ff strictly preserves comultiplication, (3) is mated to the fact that ff 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:

1 X =0 (ε X×1)Δ X X(1×ε X*) =1 (ε X×1)( X×1)(1×Δ X)(1×ε X*) =2 (ε Y×1)(f×1)( X×1)(1×Δ X)(1×ε X*) 3 (ε Y×1)( Y×1)(f×f×1)(1×Δ X)(1×ε X*) =4 (ε Y×1)( Y×1)(1×f×1)(1×Δ X)(1×ε X*)f =5 f opf\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 ff preserves the counit, (3) is mated to the fact that ff laxly preserves comultiplication, (4) uses properties of monoidal categories, and (5) uses the definition of f opf^{op}.

In fact, what this proof really proves is a converse of the earlier proposition:

Proposition

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

Proposition

If f,g:XYf, g: X \to Y are maps and fgf \leq g, then f=gf = g. Thus, the locally full subcategory whose morphisms are maps is locally discrete (the hom-posets are discrete).

Proof

A 2-cell inequality α:fg\alpha: f \leq g is mated to a inequality α *:g *f *\alpha_*: g_* \leq f_*. On the other hand, whiskering 1 Y×α×1 X1_Y \times \alpha \times 1_X with 1 Y×η X1_Y \times \eta_X and θ Y×1 X\theta_Y \times 1_X, as in the construction of opposites above, gives α op:f opg op\alpha^{op}: f^{op} \leq g^{op}. Since f op=f *f^{op} = f_* and g op=g *g^{op} = g_*, we obtain f op=g opf^{op} = g^{op}, and because f opop=ff^{op op} = f, we obtain f=gf = g.

The Beck-Chevalley condition

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

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

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

Proposition

Given a product-based pullback square

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

in Map(B)Map(\mathbf{B}), the Beck-Chevalley condition holds: h *k=fg *h_* k = f g_*.

See Brady-Trimble for further details. The critical case to consider is the pullback square

X Δ X×X Δ Δ×1 X×X 1×Δ X×X×X\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\mathbf{B} as a hyperdoctrine or monoidal fibration over Prod(B 0)Prod(B_0), where the fiber over an object BB is the local hom-poset hom(B,1)\hom(B, 1). Each f:ABf: A \to B in the base induces a pullback functor, by precomposing R:B1R: B \to 1 with π(f):AB\pi(f): A \to B in Map(B)Map(\mathbf{B}). Existential quantification is interpreted by precomposing with right adjoints π(f) *\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 PosPos-enriched \dagger-category whose local homs are meet-semilattices, satisfying Freyd’s modular law:

RST(RTS op)SR 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 11 in the sense of allegories:

  • 11 is a partial unit: we have ε 1=id 1:11\varepsilon_1 = id_1: 1 \to 1, and for any R:11R: 1 \to 1 we have R=Rε 1ε 1=id 1R = R\varepsilon_1 \leq \varepsilon_1 = id_1.

  • Any object XX is the source of a map ε X:X1\varepsilon_X: X \to 1, which being a map is entire. Thus 11 is a unit.

A bicategory of relations is also pretabular, for the maximal element in hom(X,Y)\hom(X, Y) is tabulated as (π X) *π Y(\pi_X)_* \pi_Y, where π X\pi_X, π Y\pi_Y are the product projections for X×YX \times Y.

In the other direction, suppose A\mathbf{A} is a unitary pretabular allegory. There is a faithful embedding, which preserves the unit, of A\mathbf{A} into its coreflexive splitting, which is unitary and tabular, and hence equivalent to RelRel of the regular category Map(A)Map(\mathbf{A}). By the proposition below, then, A\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 A\mathbf{A} is closed under products in its coreflexive splitting. The inclusion of A\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 (π X XY,π Y XY)(\pi^{X Y}_X, \pi^{X Y}_Y) of XY\top_{X Y} in A\mathbf{A} is a tabulation of 1 X1 Y\top_{1_X 1_Y} in the coreflexive splitting, and hence 1 X×Y1 X×1 Y1_{X \times Y} \cong 1_X \times 1_Y.

Proposition

If CC is a regular category, then the bicategory RelCRel C of relations in CC is a bicategory of relations.

Proof

By theorem 1.6 of Carboni–Walters, A\mathbf{A} is a Cartesian bicategory if:

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

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

  • The tensor product defined as

    RS=(pRp *)(pSp *) R \otimes S = (p R p_*) \cap (p' S p'_*)

    is functorial, where pp and pp' are the appropriate product projections.

The first two are obvious, and for the third we may reason in the internal language of CC. Clearly

11=[x=xx=x]=1 1 \otimes 1 = [x = x \wedge x' = x'] = 1

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

(y.RxySyz)(y.RxySyz) (\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

y.(RxySyzy *y.RxySyz) y.(RxySyzy.y *(RxySyz)) y,y.RxySyzRxySyz \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 (RR)(SS)(R \otimes R')(S \otimes S'). Finally, the Frobenius law is

[x.(x 1,x 2)=(x,x)=(x 3,x 4)]=[x.(x 1,x)=(x 3,x 3)(x 2,x 2)=(x 4,x)] [\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:

References

This article 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 5, 2023 at 17:34:30. See the history of this page for a list of all contributions to it.