Subsubsection 8.3.5.3 (00KK): Horizontal Composition

8.3.5 The Double Category of Relations

8.3.5.1 The Double Category of Relations

Definition 8.3.5.1.1 ▶ The Double Category of Relations

The double category of relations is the locally posetal double category $\smash {\mathsf{Rel}^{\mathsf{dbl}}}$ where

•
Objects. The objects of $\mathsf{Rel}^{\mathsf{dbl}}$ are sets.
•
Vertical Morphisms. The vertical morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$ are maps of sets $f\colon A\to B$.
•
Horizontal Morphisms. The horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$ are relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X$.
•
2-Morphisms. A 2-cell
of $\mathsf{Rel}^{\mathsf{dbl}}$ is either non-existent or an inclusion of relations of the form
•
Horizontal Identities. The horizontal unit functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor of Definition 8.3.5.2.1.
•
Vertical Identities. For each $A\in \operatorname {\mathrm{Obj}}(\mathsf{Rel}^{\mathsf{dbl}})$, we have

\[ \operatorname {\mathrm{id}}^{\mathsf{Rel}^{\mathsf{dbl}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{id}}_{A}. \]
•
Identity 2-Morphisms. For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the identity 2-morphism
of $R$ is the identity inclusion
•
Horizontal Composition. The horizontal composition functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor of Definition 8.3.5.3.1.
•
Vertical Composition of $1$-Morphisms. For each composable pair $A\smash {\overset {F}{\to }}B\smash {\overset {G}{\to }}C$ of vertical morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. maps of sets, we have

\[ g\mathbin {{\circ }^{\mathsf{Rel}^{\mathsf{dbl}}}}f \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g\circ f. \]
•
Vertical Composition of 2-Morphisms. The vertical composition of 2-morphisms in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.4.1.
•
Associators. The associators of $\mathsf{Rel}^{\mathsf{dbl}}$ are defined as in Definition 8.3.5.5.1.
•
Left Unitors. The left unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ are defined as in Definition 8.3.5.6.1.
•
Right Unitors. The right unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ are defined as in Definition 8.3.5.7.1.

8.3.5.2 Horizontal Identities

Definition 8.3.5.2.1 ▶ The Horizontal Identities of $\mathsf{Rel}^{\mathsf{dbl}}$

The horizontal unit functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor

\[ \mathbb {1}^{\mathsf{Rel}^{\mathsf{dbl}}} \colon \mathsf{Rel}^{\mathsf{dbl}}_{0} \to \mathsf{Rel}^{\mathsf{dbl}}_{1} \]

of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor where

•
Action on Objects. For each $A\in \operatorname {\mathrm{Obj}}(\mathsf{Rel}^{\mathsf{dbl}}_{0})$, we have

\[ \mathbb {1}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\chi _{A}(-_{1},-_{2}). \]
•
Action on Morphisms. For each vertical morphism $f\colon A\to B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. each map of sets $f$ from $A$ to $B$, the identity 2-morphism
of $f$ is the inclusion
of Chapter 4: Constructions With Sets, Item 1 of Proposition 4.5.3.1.3.

8.3.5.3 Horizontal Composition

Definition 8.3.5.3.1 ▶ The Horizontal Composition of $\mathsf{Rel}^{\mathsf{dbl}}$

The horizontal composition functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor

\[ \mathbin {\odot }^{\mathsf{Rel}^{\mathsf{dbl}}} \colon \mathsf{Rel}^{\mathsf{dbl}}_{1}\operatorname*{\mathbin {\times }}_{\mathsf{Rel}^{\mathsf{dbl}}_{0}}\mathsf{Rel}^{\mathsf{dbl}}_{1} \to \mathsf{Rel}^{\mathsf{dbl}}_{1} \]

of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor where

•
Action on Objects. For each composable pair $\smash {A\mathbin {\overset {R}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}B\mathbin {\overset {S}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}C}$ of horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, we have

\[ S\mathbin {\odot }R\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S\mathbin {\diamond }R, \]

where $S\mathbin {\diamond }R$ is the composition of $R$ and $S$ of Definition 8.1.3.1.1.
•
Action on Morphisms. For each horizontally composable pair
of 2-morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. for each pair
of inclusions of relations, the horizontal composition
of $\alpha $ and $\beta $ is the inclusion of relations

Proof of the Inclusion in Definition 8.3.5.3.1.

The inclusion of relations

\[ (U\mathbin {\diamond }T)\circ (f\times h)\subset (S\mathbin {\diamond }R) \]

follows from the fact that the statement

•
We have $a\sim _{(U\mathbin {\diamond }T)\circ (f\times h)}c$, i.e. $f(a)\sim _{U\mathbin {\diamond }T}h(c)$, i.e. there exists some $y\in Y$ such that:
- •
  We have $f(a)\sim _{T}y$.
- •
  We have $y\sim _{U}h(c)$.

is implied by the statement

•
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$.

since:

•
If $a\sim _{R}b$, then $f(a)\sim _{T}g(b)$, as $T\circ (f\times g)\subset R$;
•
If $b\sim _{S}c$, then $g(b)\sim _{U}h(c)$, as $U\circ (g\times h)\subset S$.

This finishes the proof.

8.3.5.4 Vertical Composition of 2-Morphisms

Definition 8.3.5.4.1 ▶ The Vertical Composition of 2-Morphisms in $\mathsf{Rel}^{\mathsf{dbl}}$

The vertical composition in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as follows: for each vertically composable pair

of 2-morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. for each each pair

of inclusions of relations, we define the vertical composition

of $\alpha $ and $\beta $ as the inclusion of relations

given by the pasting of inclusions

Proof of the Inclusion in Definition 8.3.5.4.1.

The inclusion

\[ T\circ [(h\circ f)\times (k\circ g)]\subset R \]

follows from the fact that, given $(a,x)\in A\times X$, the statement

•
We have $h(f(a))\sim _{T}k(g(x))$;

is implied by the statement

•
We have $a\sim _{R}x$;

since

•
If $a\sim _{R}x$, then $f(a)\sim _{S}g(x)$, as $S\circ (f\times g)\subset R$;
•
If $b\sim _{S}y$, then $h(b)\sim _{T}k(y)$, as $T\circ (h\times k)\subset S$, and thus, in particular:
- •
  If $f(a)\sim _{S}g(x)$, then $h(f(a))\sim _{T}k(g(x))$.

This finishes the proof.

8.3.5.5 The Associators

Definition 8.3.5.5.1 ▶ The Associators of $\mathsf{Rel}^{\mathsf{dbl}}$

For each composable triple

\[ A\mathbin {\overset {R}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}B\mathbin {\overset {S}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}C\mathbin {\overset {T}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}D \]

of horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, the component

of the associator of $\mathsf{Rel}^{\mathsf{dbl}}$ at $(R,S,T)$ is the identity inclusion¹

¹As proved in Item 2 of Proposition 8.1.3.1.4.

8.3.5.6 The Left Unitors

Definition 8.3.5.6.1 ▶ The Left Unitors of $\mathsf{Rel}^{\mathsf{dbl}}$

For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the component

of the left unitor of $\mathsf{Rel}^{\mathsf{dbl}}$ at $R$ is the identity inclusion¹

¹As proved in Item 3 of Proposition 8.1.3.1.4.

8.3.5.7 The Right Unitors

Definition 8.3.5.7.1 ▶ The Right Unitors of $\mathsf{Rel}^{\mathsf{dbl}}$

For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the component

of the right unitor of $\mathsf{Rel}^{\mathsf{dbl}}$ at $R$ is the identity inclusion¹

¹As proved in Item 3 of Proposition 8.1.3.1.4.

Statistics Cite

Noticed something off, or have any comments? Feel free to reach out!

•Email
•Discord

You can also use the contact form below: