The composition of $R$ and $S$ is the relation $S\mathbin {\diamond }R$ defined in one of three equivalent ways:
-
1.
Viewing relations from $A$ to $C$ as subsets of $A\times C$, we define
\[ S\mathbin {\diamond }R \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,c)\in A\times C\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ such}\\ & \text{that $a\sim _{R}b$ and $b\sim _{S}c$}\end{aligned} \right\} . \] -
2.
Viewing relations as functions $A\times B\to \{ \mathsf{true},\mathsf{false}\} $, we define
\begin{align*} (S\mathbin {\diamond }R)^{-_{1}}_{-_{2}} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{b\in B}S^{-_{1}}_{b}\times R^{b}_{-_{2}}\\ & = \bigvee _{b\in B}S^{-_{1}}_{b}\times R^{b}_{-_{2}},\end{align*}where the join $\bigvee $ is taken in the poset $(\{ \mathsf{true},\mathsf{false}\} ,\preceq )$ of Chapter 3: Sets, Definition 3.2.2.1.3.
-
3.
Viewing relations as functions $A\to \mathcal{P}(B)$, we define
where $\operatorname {\mathrm{Lan}}_{\chi _{B}}(S)$ is computed by the formula
\begin{align*} [\operatorname {\mathrm{Lan}}_{\chi _{B}}(S)](V) & \cong \int ^{b\in B}\chi _{\mathcal{P}(B)}(\chi _{b},V)\odot S(b)\\ & \cong \int ^{b\in B}\chi _{V}(b)\odot S(b)\\ & \cong \bigcup _{b\in B}\chi _{V}(b)\odot S(b)\\ & \cong \bigcup _{b\in V}S(b) \end{align*}for each $V\in \mathcal{P}(B)$, so we have1
\begin{align*} [S\mathbin {\diamond }R](a) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S(R(a))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{b\in R(a)}S(b). \end{align*}for each $a\in A$.
- 1That is: the relation $R$ may send $a\in A$ to a number of elements $\left\{ b_{i}\right\} _{i\in I}$ in $B$, and then the relation $S$ may send the image of each of the $b_{i}$’s to a number of elements $\left\{ S(b_{i})\right\} _{i\in I}=\left\{ \left\{ c_{j_{i}}\right\} _{j_{i}\in J_{i}}\right\} _{i\in I}$ in $C$.
-
1If we replace $R(a)$ with $B\setminus R(a)$, defining \[ S\mathbin {\square }R\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcap _{b\in B\setminus R(a)}S(b), \]we instead obtain the apartness composition of relations; see Section 8.1.4.
-
1.
Composing Less/Greater Than Equal With Greater/Less Than Equal Signs. Let $A=B=C=\mathbb {R}$. We have
\begin{align*} \mathord {\leq }\mathbin {\diamond }\mathord {\geq } & = \sim _{\mathrm{triv}},\\ \mathord {\geq }\mathbin {\diamond }\mathord {\leq } & = \sim _{\mathrm{triv}}. \end{align*} -
2.
Composing Less/Greater Than Equal Signs With Less/Greater Than Equal Signs. Let $A=B=C=\mathbb {R}$. We have
\begin{align*} \mathord {\leq }\mathbin {\diamond }\mathord {\leq } & = \mathord {\leq },\\ \mathord {\geq }\mathbin {\diamond }\mathord {\geq } & = \mathord {\geq }. \end{align*} -
1.
Functoriality. The assignments $R,S,(R,S)\mapsto S\mathbin {\diamond }R$ define functors
\[ \begin{array}{ccc} S\mathbin {\diamond }-\colon \mkern -15mu & \mathbf{Rel}(A,B) \mkern -17.5mu& {}\mathbin {\to }\mathbf{Rel}(A,C),\\ -\mathbin {\diamond }R\colon \mkern -15mu & \mathbf{Rel}(B,C) \mkern -17.5mu& {}\mathbin {\to }\mathbf{Rel}(A,C),\\ -_{1}\mathbin {\diamond }-_{2}\colon \mkern -15mu & \mathbf{Rel}(B,C)\times \mathbf{Rel}(A,B) \mkern -17.5mu& {}\mathbin {\to }\mathbf{Rel}(A,C). \end{array} \]In particular, given relations
if $R_{1}\subset R_{2}$ and $S_{1}\subset S_{2}$, then $S_{1}\mathbin {\diamond }R_{1}\subset S_{2}\mathbin {\diamond }R_{2}$.
-
2.
Associativity. We have
\[ (T\mathbin {\diamond }S)\mathbin {\diamond }R = T\mathbin {\diamond }(S\mathbin {\diamond }R). \]That is, we have
\[ \bigcup _{b\in R(a)}\bigcup _{c\in S(b)}T(c)=\bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c) \]for each $a\in A$.
-
3.
Unitality. We have
\begin{align*} \Delta _{B}\mathbin {\diamond }R & = R,\\ R\mathbin {\diamond }\Delta _{A} & = R. \end{align*}That is, we have
\begin{align*} \bigcup _{b\in R(a)}\left\{ b\right\} & = R(a),\\ \bigcup _{a\in \left\{ a\right\} }R(a) & = R(a) \end{align*}for each $a\in A$.
-
4.
Relation to Apartness Composition of Relations. We have
\begin{align*} (S\mathbin {\diamond }R)^{\textsf{c}} & = S^{\textsf{c}}\mathbin {\square }R^{\textsf{c}},\\ (S\mathbin {\square }R)^{\textsf{c}} & = S^{\textsf{c}}\mathbin {\diamond }R^{\textsf{c}}, \end{align*}where $(-)^{\textsf{c}}$ is the complement functor of Chapter 4: Constructions With Sets, Section 4.3.11. In particular, $\mathord {\mathbin {\diamond }}$ is a special case of apartness composition of relations, as we have
\[ S\mathbin {\diamond }R=(S^{\textsf{c}}\mathbin {\square }R^{\textsf{c}})^{\textsf{c}}. \]This is also compatible with units, as we have $\Delta ^{\textsf{c}}_{A}=\nabla _{A}$.
-
5.
Linear Distributivity. We have inclusions of relations
\begin{align*} T\mathbin {\diamond }(S\mathbin {\square }R) & \subset (T\mathbin {\diamond }S)\mathbin {\square }R,\\ (T\mathbin {\square }S)\mathbin {\diamond }R & \subset T\mathbin {\square }(S\mathbin {\diamond }R). \end{align*}That is, we have
\begin{align*} T(\bigcap _{b\in B\setminus R(a)}S(b)) & \subset \bigcap _{b\in B\setminus R(a)}T(S(b))\\ \bigcup _{b\in R(a)}\bigcap _{c\in C\setminus S(b)}T(c) & \subset \bigcap _{c\in C\setminus S(R(a))}T(c) \end{align*}or, unwinding the expression for $S(R(a))$, we have
\begin{align*} \bigcup _{c\in \bigcap _{b\in B\setminus R(a)}S(b)}T(c) & \subset \bigcap _{b\in B\setminus R(a)}\bigcup _{c\in S(b)}T(c)\\ \bigcup _{b\in R(a)}\bigcap _{c\in C\setminus S(b)}T(c) & \subset \bigcap _{c\in C\setminus \bigcup _{b\in R(a)}S(b)}T(c) \end{align*}for each $a\in A$.
-
6.
Interaction With Converses. We have
\[ (S\mathbin {\diamond }R)^{\dagger } = R^{\dagger }\mathbin {\diamond }S^{\dagger }. \] -
7.
Interaction With Ranges and Domains. We have
\begin{align*} \operatorname {Dom}(S\mathbin {\diamond }R) & \subset \operatorname {Dom}(R),\\ \mathrm{Im}(S\mathbin {\diamond }R) & \subset \mathrm{Im}(S). \end{align*} -
1.
We have $a\sim _{(T\mathbin {\diamond }S)\mathbin {\diamond }R}d$, i.e. there exists some $b\in B$ such that:
-
•
We have $a\sim _{R}b$;
-
•
We have $b\sim _{T\mathbin {\diamond }S}d$, i.e. there exists some $c\in C$ such that:
-
•
We have $b\sim _{S}c$;
-
•
We have $c\sim _{T}d$;
-
•
-
•
-
2.
We have $a\sim _{T\mathbin {\diamond }(S\mathbin {\diamond }R)}d$, i.e. there exists some $c\in C$ such that:
-
•
We have $a\sim _{S\mathbin {\diamond }R}c$, i.e. there exists some $b\in B$ such that:
-
•
We have $a\sim _{R}b$;
-
•
We have $b\sim _{S}c$;
-
•
-
•
We have $c\sim _{T}d$;
-
•
- (★) There exist $b\in B$ and $c\in C$ such that $a\sim _{R}b\sim _{S}c\sim _{T}d$.
-
•
The equality
\[ \Delta _{B}\mathbin {\diamond }R=R \]witnesses the equivalence of the following two statements:
-
•
We have $a\sim _{b}B$.
-
•
There exists some $b'\in B$ such that:
-
•
We have $a\sim _{R}b'$
-
•
We have $b'\sim _{\Delta _{B}}b$, i.e. $b'=b$.
-
•
-
•
-
•
The equality
\[ R\mathbin {\diamond }\Delta _{A}=R \]witnesses the equivalence of the following two statements:
-
•
There exists some $a'\in A$ such that:
-
•
We have $a\sim _{\Delta _{B}}a'$, i.e. $a=a'$.
-
•
We have $a'\sim _{R}b$
-
•
-
•
We have $a\sim _{b}B$.
-
•
8.1.3 Composition of Relations
Let $A$, $B$, and $C$ be sets and let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ and $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$ be relations.
Proof of the Equivalences in Definition 8.1.3.1.1.
Omitted.
You might wonder what happens if we instead define an alternative composition of relations $\mathord {\mathbin {\diamond }'}$ via right Kan extensions. In this case, we would take the right Kan extension of $S$ along the dual characteristic embedding $B\hookrightarrow \mathcal{P}(B)^{\mathsf{op}}$:
\[ [S\mathbin {\mathord {\mathbin {\diamond }}'}R](a)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcap _{b\in R(a)}S(b). \]
This alternative composition turns out to actually be a different kind of structure: it’s an internal right Kan extension in $\boldsymbol {\mathsf{Rel}}$, namely $\operatorname {\mathrm{Ran}}_{R^{\dagger }}(S)$ — see Section 8.5.17.
Here are some examples of composition of relations.
Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$, $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$, and $T\colon C\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}D$ be relations.
Proof of Proposition 8.1.3.1.4.
Item 1: Functoriality
We have
\begin{align*} S_{1}\mathbin {\diamond }R_{1} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ (a,c)\in A\times C\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$, such}\\ & \text{that $a\sim _{R_{1}}b$ or $b\sim _{S_{1}}c$}\end{aligned} \right\} \\ & \subset \left\{ (a,c)\in A\times C\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$, such}\\ & \text{that $a\sim _{R_{2}}b$ or $b\sim _{S_{2}}c$}\end{aligned} \right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S_{2}\mathbin {\diamond }R_{2}. \end{align*}
This finishes the proof.
Item 2: Associativity, Proof I
Indeed, we have
\begin{align*} (T\mathbin {\diamond }S)\mathbin {\diamond }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\int ^{c\in C}T^{-_{1}}_{c}\times S^{c}_{-_{2}})\mathbin {\diamond }R\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{b\in B}(\int ^{c\in C}T^{-_{1}}_{c}\times S^{c}_{b})\times R^{b}_{-_{2}}\\ & = \int ^{b\in B}\int ^{c\in C}(T^{-_{1}}_{c}\times S^{c}_{b})\times R^{b}_{-_{2}}\\ & = \int ^{c\in C}\int ^{b\in B}(T^{-_{1}}_{c}\times S^{c}_{b})\times R^{b}_{-_{2}}\\ & = \int ^{c\in C}\int ^{b\in B}T^{-_{1}}_{c}\times (S^{c}_{b}\times R^{b}_{-_{2}})\\ & = \int ^{c\in C}T^{-_{1}}_{c}\times (\int ^{b\in B}S^{c}_{b}\times R^{b}_{-_{2}})\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{c\in C}T^{-_{1}}_{c}\times (S\mathbin {\diamond }R)^{c}_{-_{2}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}T\mathbin {\diamond }(S\mathbin {\diamond }R). \end{align*}
In the language of relations, given $a\in A$ and $d\in D$, the stated equality witnesses the equivalence of the following two statements:
both of which are equivalent to the statement
Item 2: Associativity, Proof II
Using Item 3 of Definition 8.1.3.1.1, we have
\begin{align*} [(T\mathbin {\diamond }S)\mathbin {\diamond }R](a) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{b\in R(a)}(T\mathbin {\diamond }S)(b)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{b\in R(a)}\bigcup _{c\in S(b)}T(c) \end{align*}
on the one hand and
\begin{align*} [T\mathbin {\diamond }(S\mathbin {\diamond }R)](a) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{c\in [S\mathbin {\diamond }R](a)}T(c)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c) \end{align*}
on the other, so we want to prove an equality of the form
\[ \bigcup _{b\in R(a)}\bigcup _{c\in S(b)}T(c)=\bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c). \]
This then follows from an application of Chapter 4: Constructions With Sets, Item 2 of Proposition 4.3.6.1.2 in which we consider $X=D$, consider $\mathcal{P}(\mathcal{P}(\mathcal{P}(D)))$, take $U=U_{c}=T(c)$, take $A$ to be
\[ A_{b}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ T(c)\in \mathcal{P}(D)\ \middle |\ c\in S(b)\right\} , \]
and then finally take
\begin{align*} \mathcal{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ A_{b}\in \mathcal{P}(\mathcal{P}(D))\ \middle |\ b\in R(a)\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ \left\{ T(c)\in \mathcal{P}(D)\ \middle |\ c\in S(b)\right\} \ \middle |\ b\in R(a)\right\} . \end{align*}
Indeed, we have
\begin{align*} \bigcup _{A\in \mathcal{A}}(\bigcup _{U\in A}U) & = \bigcup _{A_{b}\in \mathcal{A}}(\bigcup _{c\in S(b)}T(c))\\ & = \bigcup _{b\in R(a)}(\bigcup _{c\in S(b)}T(c)) \end{align*}
and
\begin{align*} \bigcup _{U\in \bigcup _{A\in \mathcal{A}}A}U & = \bigcup _{U_{c}\in \bigcup _{b\in R(a)}A_{b}}U_{c}\\ & = \bigcup _{T(c)\in \bigcup _{b\in R(a)}A_{b}}T(c)\\ & = \bigcup _{c\in \bigcup _{b\in R(a)}S(b)}T(c).\end{align*}
This finishes the proof.
Item 3: Unitality
Indeed, we have
\begin{align*} \Delta _{B}\mathbin {\diamond }R & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{b\in B}(\Delta _{B})^{-_{1}}_{b}\times R^{b}_{-_{2}}\\ & = \bigvee _{b\in B}(\Delta _{B})^{-_{1}}_{b}\times R^{b}_{-_{2}}\\ & = \bigvee _{\substack {b\in B\\ \begin{bgroup} b=-_{1}
\end{bgroup}}}R^{b}_{-_{2}}\\ & = R^{-_{1}}_{-_{2}}, \end{align*}
and
\begin{align*} R\mathbin {\diamond }\Delta _{A} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\int ^{a\in A}R^{-_{1}}_{a}\times (\Delta _{A})^{a}_{-_{2}}\\ & = \bigvee _{a\in B}R^{-_{1}}_{a}\times (\Delta _{A})^{a}_{-_{2}}\\ & = \bigvee _{\substack {a\in B\\ \begin{bgroup} a=-_{2}
\end{bgroup}}}R^{-_{1}}_{a}\\ & = R^{-_{1}}_{-_{2}}. \end{align*}
In the language of relations, given $a\in A$ and $b\in B$:
Item 4: Relation to Apartness Composition of Relations
This is a repetition of Item 4 of Proposition 8.1.4.1.3 and is proved there.
Item 5: Linear Distributivity
This is a repetition of Item 5 of Proposition 8.1.4.1.3 and is proved there.
Item 6: Interaction With Converses
This is a repetition of Item 3 of Proposition 8.1.5.1.3 and is proved there.
Item 7: Interaction With Ranges and Domains
We have
\begin{align*} \operatorname {Dom}(S\mathbin {\diamond }R) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ a\sim _{S\mathbin {\diamond }R}c\text{ for some $c\in C$}\right\} ,\\ & = \left\{ a\in A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$ and $c\in C$}\\ & \text{such that $a\sim _{R}b$ and $b\sim _{R}c$} \end{aligned} \right\} ,\\ & \subset \left\{ a\in A\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$}\\ & \text{such that $a\sim _{R}b$} \end{aligned} \right\} ,\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {Dom}(R) \end{align*}
and
\begin{align*} \mathrm{Im}(S\mathbin {\diamond }R) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ c\in C\ \middle |\ a\sim _{S\mathbin {\diamond }R}c\text{ for some $a\in A$}\right\} ,\\ & = \left\{ c\in C\ \middle |\ \begin{aligned} & \text{there exists some $a\in A$ and $b\in B$}\\ & \text{such that $a\sim _{R}b$ and $b\sim _{R}c$} \end{aligned} \right\} ,\\ & \subset \left\{ c\in C\ \middle |\ \begin{aligned} & \text{there exists some $b\in B$}\\ & \text{such that $b\sim _{S}c$} \end{aligned} \right\} ,\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Im}(S). \end{align*}
This finishes the proof.
