5.2.4 The Double Category of Relations

5.2.4.1 The Double Category of Relations

Definition 5.2.4.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 5.2.4.2.1.
  • Vertical Identities. For each $A\in \text{Obj}\webleft (\mathsf{Rel}^{\mathsf{dbl}}\webright )$, we have

    \[ \text{id}^{\mathsf{Rel}^{\mathsf{dbl}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{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 5.2.4.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 5.2.4.4.1.
  • Associators. The associators of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 5.2.4.5.1.
  • Left Unitors. The left unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 5.2.4.6.1.
  • Right Unitors. The right unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 5.2.4.7.1.

5.2.4.2 Horizontal Identities

Definition 5.2.4.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 \text{Obj}\webleft (\mathsf{Rel}^{\mathsf{dbl}}_{0}\webright )$, we have

    \[ \mathbb {1}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\chi _{A}\webleft (-_{1},-_{2}\webright ). \]

  • 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 2: Constructions With Sets, Item 1 of Proposition 2.4.1.1.3.

5.2.4.3 Horizontal Composition

Definition 5.2.4.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 Chapter 6: Constructions With Relations, Definition 6.3.12.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[1]

5.2.4.4 Vertical Composition of 2-Morphisms

Definition 5.2.4.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[2]

5.2.4.5 The Associators

Definition 5.2.4.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 $\webleft (R,S,T\webright )$ is the identity inclusion[3]

5.2.4.6 The Left Unitors

Definition 5.2.4.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[4]

5.2.4.7 The Right Unitors

Definition 5.2.4.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[5]

Footnotes

[1] This is justified by noting that, given $\webleft (a,c\webright )\in A\times C$, the statement
  • We have $a\sim _{\webleft (U\mathbin {\diamond }T\webright )\circ \webleft (f\times h\webright )}c$, i.e. $f\webleft (a\webright )\sim _{U\mathbin {\diamond }T}h\webleft (c\webright )$, i.e. there exists some $y\in Y$ such that:
    1. We have $f\webleft (a\webright )\sim _{T}y$;
    2. We have $y\sim _{U}h\webleft (c\webright )$;
is implied by the statement
  • We have $a\sim _{S\mathbin {\diamond }R}c$, i.e. there exists some $b\in B$ such that:
    1. We have $a\sim _{R}b$;
    2. We have $b\sim _{S}c$;
since:
  • If $a\sim _{R}b$, then $f\webleft (a\webright )\sim _{T}g\webleft (b\webright )$, as $T\circ \webleft (f\times g\webright )\subset R$;
  • If $b\sim _{S}c$, then $g\webleft (b\webright )\sim _{U}h\webleft (c\webright )$, as $U\circ \webleft (g\times h\webright )\subset S$.
[2] This is justified by noting that, given $\webleft (a,x\webright )\in A\times X$, the statement
  • We have $h\webleft (f\webleft (a\webright )\webright )\sim _{T}k\webleft (g\webleft (x\webright )\webright )$;
is implied by the statement
  • We have $a\sim _{R}x$;
since
  • If $a\sim _{R}x$, then $f\webleft (a\webright )\sim _{S}g\webleft (x\webright )$, as $S\circ \webleft (f\times g\webright )\subset R$;
  • If $b\sim _{S}y$, then $h\webleft (b\webright )\sim _{T}k\webleft (y\webright )$, as $T\circ \webleft (h\times k\webright )\subset S$, and thus, in particular:
    • If $f\webleft (a\webright )\sim _{S}g\webleft (x\webright )$, then $h\webleft (f\webleft (a\webright )\webright )\sim _{T}k\webleft (g\webleft (x\webright )\webright )$.
Previous

View Subsection 5.2.4 as PDF

Statistics Cite

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

You can also use the contact form below: