Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
The concept of internal relation is an internalization of the concept of a relation from Set to more general categories and it is often called just a relation in the category $C$.
If $C$ is a regular category, then its category of internal binary relations is an allegory. The objects of an allegory may, but do not need to be, internal relations in some ambient category.
Let $C$ be a category. An internal binary relation from an object $X$ to an object $Y$ is an object $R$ and a pair of maps $d_0: R \to X$ and $d_1: R \to Y$ that are jointly monic, that is such that, given any object $G$ and morphism $e, e': G \to R$, if $d_0 \circ e = d_0 \circ e'$ and $d_1 \circ e = d_1 \circ e'$, then it must be that $e = e'$.
Now suppose that $C$ has binary products. Then we can simplify the definition; an internal binary relation from $X$ to $Y$ is simply a subobject $r: R\hookrightarrow X\times Y$. The $d_0$ and $d_1$ above may be recovered as the composites
called the projections of the relation $R$.
A relation from $X$ to $X$ is also said to be an internal binary relation on $X$, and an object $X$ with an internal binary relation is a loop digraph object.
As with relations in general, we can extend from binary to arbitrary internal relations by generalising from the pair $(X,Y)$ to an arbitrary family of objects. If this family has a product in $C$, then the internal relation is simply a subobject of that product; in general, the internal relation is given by a jointly monic family of morphisms.
The various kinds of relations described at relation can often be interpreted internally.
For example, an internal relation $R$ on $X$ is said to be reflexive if it contains the diagonal subobject $X\hookrightarrow X\times X$ of $X$; this can even be stated if $X \times X$ does not exist in the category.
An internal equivalence relation is often called a congruence.
Last revised on May 14, 2022 at 07:51:58. See the history of this page for a list of all contributions to it.