Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A binary relation from a set to a set is called functional if every element of is related to at most one element of . Notice that this is the same thing as a partial function, seen from a different point of view. A (total) function is precisely a relation that is both functional and entire.
Like any relation, a functional relation can be viewed as a span
Such a span is a relation iff the pairing map from the domain to is an injection, and such a relation is functional iff the inclusion map is also an injection. Such a relation is entire iff the inclusion map is a surjection.
(Total) functions are precisely left adjoints in the bicategory of relations, in other words relations in for which there exists satisfying
For if a relation is a function, then
: this just says that if and , then . Equivalently, if and then : this holds precisely because is functional or well-defined.
: this says that if in , then there exists in such that and , i.e., there exists such that and . This holds precisely because a function is an entire relation.
On the other hand, suppose is a left adjoint.
From we deduce that if in , then there exists in such that and ; in particular is entire.
Suppose . From there exists such that and . Thus and ; from we infer . We conclude at most one satisfies , making functional.
Since is a function, it has a right adjoint , and by uniqueness of right adjoints, we may conclude . The monad has a unit ( is reflexive) and a multiplication ( is transitive), and also ( is symmetric). So the monad is an equivalence relation. The above reasoning may be internalized to apply to the bicategory of relations internal to a regular category, in which case this equivalence relation is exactly the kernel pair of the map . The comonad has a counit ( is coreflexive), and such coreflective relations in correspond to subsets of . More generally, in a regular category, the subobject of named by is the image of (the coequalizer of the kernel pair).
Further remarks: surjectivity of a function can be expressed as the condition , and injectivity as .
Peter Freyd and André Scedrov, Categories, Allegories, Mathematical Library Vol. 39, North-Holland (1990).
Robin Houston, Fun with Rel, blog post at Bosker Blog (June 14, 2006). (link)
Last revised on November 21, 2017 at 07:34:19. See the history of this page for a list of all contributions to it.