Relation Lifting

(draft)

Extending a functor from functions to relations is important to coalgebra for at least two reasons. Relation lifting can be used to define bisimulations and also to define Moss's coalgebraic logic. In the latter case, the idea is to apply the lifted functor to the satisfiability relation.

Relation lifting can be defined in at least two ways, via spans and via cospans. In both cases the idea is to first represent a relation by a pair of arrows, and then to apply the functor to these arrows.

In the following let

Rel be the category which has sets as objects and relations as arrows.

Span-Based Relation Lifting

The idea of the span-based relation lifting of a functor

T is to "tabulate" a relation
R
by a span
XpRqY
and then to apply the functor
T
to the projections, obtaining
TXTpTRTqTY
.

Definition: Let

T:SetSet and
XpRqY
be a relation. Then
T:RelRel

is the relation given by

TR={(a,b)TX×TYwTR.Tp(w)=a & Tq(w)=b}

Remark: This formulation is specific to set-functors, but can be generalised to other base categories.

Fact:

T preserves composition (and therefore is a functor on
Rel
) if
T
preserves weak-pullbacks.

Example/Exercise: Let

P be the powerset functor. It is an interesting exercise to check that
(a,b)PX
iff
xa.yb.xRyyb.xa.xRy

Fact:

P:RelRel is a functor. If
R
is a partial order then
PR
is a partial order.

Extending Set-Functors to Ordered Sets

The cospan-based relation lifting starts from the cotabulation (or collage) of a relation

R by a cospan
XjRkY
, where
R
is an order on the disjoint union
X+Y
given by
(u,v)R
iff
u=vX
or
(u,v)R
or
u=vY
.

Thus, in order to apply a set-functor

T to
j
and
k
, we need extend
T
from sets to orders. This follows the same idea as the relation lifting in the previous section, but now one closes under reflexivity and transitivity (and quotients by anti-symmetry in the case one works with posets).

Definition: Let

(X,) be a pre-order. Write
XpqX
for the two projections. Then
T~(X,)
has carrier
TX
and the order on
T~(X,)

is the smallest order containing

{(a,b)TX×TXwT().Tp(w)=a & Tq(w)=b}.

This defines a functor

T~:OrdOrd

where

Ord can be preorders or posets.

Remark: The surjection

 TXsT~(X,) has a universal property as the universal solution to the inequation to
sTpsTq
. Category theoretically, we can say that
s
is the coinserter of
(Tp,Tq)
and also that
T~
is the (order-enriched) left Kan extension of
DT
along
D
where
D
is the embedding of sets into (discrete) ordered sets.

The following fact allows us to use known results about the span-based relation lifting to compute the order-extension of a set-functor in many examples.

Fact: If

T preserves weak pullbacks, then applying
T~
to a preorder
(X,)
agrees with applying the relation lifting
T
to
.

Example: Let

(X,) be a preorder. For subsets
a,bX
we have
abP~(X,)
iff
xa.yb.xyyb.xa.xy

In domain theory, this is also known as the Egli-Milner order. When restricted to convex subsets (and modified wrt the empty subset)

P~ is known as the Plotkin powerdomain. See also my review of powerdomains.

Cospan-Based Relation Lifting

To cotabulate a relation

RX×Y by a cospan
XjRkY

we need to recall the collage

R of a relation
R
. This notion can also be defined in case
X
and
Y
are ordered sets and
R
is weakening-closed, that is,
xxRyyxRy.

We give the more general definition, because it shows that the cospan-based relation lifting cannot only be used to extend set-functors but also ordered functors.

If

RX×Y is a weakening relation, then the collage
R
is an order on the disjoint union
X+Y
such that
xRy
if (i)
xy
in
X
or (ii)
xRy
or (iii)
xy
in
Y
.

Given a functor

T:SetSet, [1] we can use the collage to give a cospan-based definition of relation lifting.

Definition: Let

RX×Y. Then
T^:RelRel

is defined

(a,b)T^R if
ab
in
T~R
.

Fact: If

T preserves weak pullbacks then
T=T^
.

Conclusion

The span-based relation lifting can be generalised to ordered sets an is well-behaved if the functor preserves weak pullbacks.

The cospan-based relation lifting is ineherently order enriched, but can be applied to the discrete case if we extend the functor to ordered sets.

One application of relation lifting is to define coalgebraic bisimulation. Here the span-based and the cospan-based definition agree if the functor preserves weak pullbacks, but in general it is only cospan bisimilarity that captures coalgebraic behavioural equivalence/preorder.

The cospan-based relation lifting generalises from ordered sets to Lawvere metric spaces and other categories enriched over a quantale.

References

References can be found in the survey article


  1. (or a functor on preorders or posets) ↩︎