Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
Bicategories of 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 , the diagonal and codiagonal 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 , are left adjoint 1-morphisms, and for which every morphism 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 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 , 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) .
In one direction, we have the 2-cell which is the unit of the adjunction . In the other direction, there is an adjunction between the counit and its dual, and the unit of this adjunction is a 2-cell , from which we derive
where the last equation follows from the equation and its dual .
(Dual Frobenius condition) .
The locally full subcategory whose 1-cells are maps (= left adjoints) has finite products, in particular a symmetry involution for which
Additionally, the right adjoint is the inverse . Hence the equation above is mated to , 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 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 as the 1-morphism mate:
In this way, a bicategory of relations becomes a †-compact -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 is a map, then is a strict morphism of comonoids.
If is the right adjoint of , we have since , like any morphism, is a lax comonoid morphism. But this 2-cell is mated to a 2-cell , inverse to the 2-cell that comes for free. So preserves comultiplication strictly. A similar argument shows preserves the counit strictly.
If is a map, then equals the right adjoint .
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 , and the second gives a unit. We have
where (0) uses the definition of , (1) uses properties of monoidal categories, (2) uses the fact that strictly preserves comultiplication, (3) is mated to the fact that 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 preserves the counit, (3) is mated to the fact that laxly preserves comultiplication, (4) uses properties of monoidal categories, and (5) uses the definition of .
In fact, what this proof really proves is a converse of the earlier proposition:
If is a strict comonoid morphism, then has a right adjoint: .
If are maps and , then . Thus, the locally full subcategory whose morphisms are maps is locally discrete (the hom-posets are discrete).
A 2-cell inequality is mated to a inequality . On the other hand, whiskering with and , as in the construction of opposites above, gives . Since and , we obtain , and because , we obtain .
The Beck-Chevalley condition
Bicategories of relations satisfy a Beck-Chevalley condition, as follows. Let denote the free category with finite products generated by the set of objects of . According to the results at free cartesian category, is finitely complete.
Since has finite products, there is a product-preserving functor which is the identity on objects. Again, according to the results of free cartesian category, we have the following result.
If a diagram in is a pullback square, then application of to that diagram is a pullback square in .
Let us call pullback squares of this form in product-based pullback squares.
Given a product-based pullback square
in , the Beck-Chevalley condition holds: .
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 as a hyperdoctrine or monoidal fibration over , where the fiber over an object is the local hom-poset . Each in the base induces a pullback functor, by precomposing with in . Existential quantification is interpreted by precomposing with right adjoints . 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 -enriched -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 in the sense of allegories:
is a partial unit: we have , and for any we have .
Any object is the source of a map , which being a map is entire. Thus is a unit.
A bicategory of relations is also pretabular, for the maximal element in is tabulated as , where , are the product projections for .
In the other direction, suppose is a unitary pretabular allegory. There is a faithful embedding, which preserves the unit, of into its coreflexive splitting, which is unitary and tabular, and hence equivalent to of the regular category . By the proposition below, then, 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 is closed under products in its coreflexive splitting. The inclusion of 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 of in is a tabulation of in the coreflexive splitting, and hence .
By theorem 1.6 of Carboni–Walters, is a Cartesian bicategory if:
has finite products.
has local finite products, and is the top element of .
The tensor product defined as
is functorial, where and are the appropriate product projections.
The first two are obvious, and for the third we may reason in the internal language of . Clearly
The formula whose meaning is by is
and we may use Frobenius reciprocity to get
which is the meaning of . 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.