Subsection 7.3.9 (00Q7): Binary Products of Relations

Let $A$, $B$, $X$, and $Y$ be sets, let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation from $A$ to $B$, and let $S\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y$ be a relation from $X$ to $Y$.

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

The product of $R$ and $S$¹ is the relation $R\times S$ from $A\times X$ to $B\times Y$ defined as follows:

Viewing relations from $A\times X$ to $B\times Y$ as subsets of $\webleft (A\times X\webright )\times \webleft (B\times Y\webright )$, we define $R\times S$ as the Cartesian product of $R$ and $S$ as subsets of $A\times X$ and $B\times Y$;²
Viewing relations from $A\times X$ to $B\times Y$ as functions $A\times X\to \mathcal{P}\webleft (B\times Y\webright )$, we define $R\times S$ as the composition

\[ A\times X \overset {R\times S}{\to } \mathcal{P}\webleft (B\webright )\times \mathcal{P}\webleft (Y\webright ) \overset {\mathcal{P}^{\otimes }_{B,Y}}{\hookrightarrow } \mathcal{P}\webleft (B\times Y\webright ) \]

in $\mathsf{Sets}$, i.e. by

\[ \webleft [R\times S\webright ]\webleft (a,x\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R\webleft (a\webright )\times S\webleft (x\webright ) \]

for each $\webleft (a,x\webright )\in A\times X$.

¹Further Terminology: Also called the binary product of $R$ and $S$, for emphasis.

²That is, $R\times S$ is the relation given by declaring $\webleft (a,x\webright )\sim _{R\times S}\webleft (b,y\webright )$ iff $a\sim _{R}b$ and $x\sim _{S}y$.

Let $A$, $B$, $X$, and $Y$ be sets.

Interaction With Inverses. Let
\begin{align*} R & \colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A,\\ S & \colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X \end{align*}

We have

\[ \webleft (R\times S\webright )^{\dagger } = R^{\dagger }\times S^{\dagger }. \]
Interaction With Composition. Let
\begin{align*} R_{1} & \colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B,\\ S_{1} & \colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C,\\ R_{2} & \colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y,\\ S_{2} & \colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Z \end{align*}

be relations. We have

\[ \webleft (S_{1}\mathbin {\diamond }R_{1}\webright )\times \webleft (S_{2}\mathbin {\diamond }R_{2}\webright )=\webleft (S_{1}\times S_{2}\webright )\mathbin {\diamond }\webleft (R_{1}\times R_{2}\webright ). \]

Item 1: Interaction With Inverses

Unwinding the definitions, we see that:

We have $\webleft (a,x\webright )\sim _{\webleft (R\times S\webright )^{\dagger }}\webleft (b,y\webright )$ iff :
- We have $\webleft (b,y\webright )\sim _{R\times S}\webleft (a,x\webright )$, i.e. iff :
  - We have $b\sim _{R}a$;
  - We have $y\sim _{S}x$;
We have $\webleft (a,x\webright )\sim _{R^{\dagger }\times S^{\dagger }}\webleft (b,y\webright )$ iff :
- We have $a\sim _{R^{\dagger }}b$ and $x\sim _{S^{\dagger }}y$, i.e. iff :
  - We have $b\sim _{R}a$;
  - We have $y\sim _{S}x$.

These two conditions agree, and thus the two resulting relations on $A\times X$ are equal.

Item 2: Interaction With Composition

Unwinding the definitions, we see that:

We have $\webleft (a,x\webright )\sim _{\webleft (S_{1}\mathbin {\diamond }R_{1}\webright )\times \webleft (S_{2}\mathbin {\diamond }R_{2}\webright )}\webleft (c,z\webright )$ iff :
1. We have $a\sim _{S_{1}\mathbin {\diamond }R_{1}}c$ and $x\sim _{S_{2}\mathbin {\diamond }R_{2}}z$, i.e. iff :
  1. There exists some $b\in B$ such that $a\sim _{R_{1}}b$ and $b\sim _{S_{1}}c$;
  2. There exists some $y\in Y$ such that $x\sim _{R_{2}}y$ and $y\sim _{S_{2}}z$;
We have $\webleft (a,x\webright )\sim _{\webleft (S_{1}\times S_{2}\webright )\mathbin {\diamond }\webleft (R_{1}\times R_{2}\webright )}\webleft (c,z\webright )$ iff :
1. There exists some $\webleft (b,y\webright )\in B\times Y$ such that $\webleft (a,x\webright )\sim _{R_{1}\times R_{2}}\webleft (b,y\webright )$ and $\webleft (b,y\webright )\sim _{S_{1}\times S_{2}}\webleft (c,z\webright )$, i.e. such that:
  1. We have $a\sim _{R_{1}}b$ and $x\sim _{R_{2}}y$;
  2. We have $b\sim _{S_{1}}c$ and $y\sim _{S_{2}}z$.

These two conditions agree, and thus the two resulting relations from $A\times X$ to $C\times Z$ are equal.

The Clowder Project

7.3.9 Binary Products of Relations