Subsubsection 8.3.3.3 (00JY): The Associator

8.3.3 The Closed Symmetric Monoidal Category of Relations

8.3.3.1 The Monoidal Product

Definition 8.3.3.1.1 ▶ The Monoidal Product of $\mathsf{Rel}$

The monoidal product of $\mathsf{Rel}$ is the functor

\[ \times \colon \mathsf{Rel}\times \mathsf{Rel}\to \mathsf{Rel} \]

where

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

\[ \mathord {\times }(A,B)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A\times B, \]

where $A\times B$ is the Cartesian product of sets of Chapter 4: Constructions With Sets, Definition 4.1.3.1.1.
•
Action on Morphisms. For each $(A,C),(B,D)\in \operatorname {\mathrm{Obj}}(\mathsf{Rel}\times \mathsf{Rel})$, the action on morphisms

\[ \times _{(A,C),(B,D)}\colon \mathrm{Rel}(A,B)\times \mathrm{Rel}(C,D)\to \mathrm{Rel}(A\times C,B\times D) \]

of $\times $ is given by sending a pair of morphisms $(R,S)$ of the form

\begin{align*} R & \colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B,\\ S & \colon C\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}D \end{align*}

to the relation

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

of Chapter 9: Constructions With Relations, Definition 9.2.6.1.1.

8.3.3.2 The Monoidal Unit

Definition 8.3.3.2.1 ▶ The Monoidal Unit of $\mathsf{Rel}$

The monoidal unit of $\mathsf{Rel}$ is the functor

\[ \mathbb {1}^{\mathsf{Rel}}\colon \mathrm{pt}\to \mathsf{Rel} \]

picking the set

\[ \mathbb {1}_{\mathsf{Rel}}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{pt} \]

of $\mathsf{Rel}$.

8.3.3.3 The Associator

Definition 8.3.3.3.1 ▶ The Associator of $\mathsf{Rel}$

The associator of $\mathsf{Rel}$ is the natural isomorphism

\[ \alpha ^{\mathsf{Rel}}\colon {\times }\circ {({(\times )}\times {\mathsf{id}})}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}{\times }\circ {({\mathsf{id}}\times {(\times )})}\circ {\mathbf{\alpha }^{\mathsf{Cats}}_{\mathsf{Rel},\mathsf{Rel},\mathsf{Rel}}}\mathrlap {,} \]

as in the diagram

whose component

\[ \alpha ^{\mathsf{Rel}}_{A,B,C}\colon (A\times B)\times C\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A\times (B\times C) \]

at $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$ is the relation defined by declaring

\[ ((a,b),c) \sim _{\alpha ^{\mathsf{Rel}}_{A,B,C}} (a',(b',c')) \]

iff $a=a'$, $b=b'$, and $c=c'$.

8.3.3.4 The Left Unitor

Definition 8.3.3.4.1 ▶ The Left Unitor of $\mathsf{Rel}$

The left unitor of $\mathsf{Rel}$ is the natural isomorphism

whose component

\[ \lambda ^{\mathsf{Rel}}_{A} \colon \mathbb {1}_{\mathsf{Rel}}\times A \mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A \]

at $A$ is defined by declaring

\[ (\star ,a) \sim _{\lambda ^{\mathsf{Rel}}_{A}} b \]

iff $a=b$.

8.3.3.5 The Right Unitor

Definition 8.3.3.5.1 ▶ The Right Unitor of $\mathsf{Rel}$

The right unitor of $\mathsf{Rel}$ is the natural isomorphism

whose component

\[ \rho ^{\mathsf{Rel}}_{A} \colon A\times \mathbb {1}_{\mathsf{Rel}} \mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}A \]

at $A$ is defined by declaring

\[ (a,\star ) \sim _{\rho ^{\mathsf{Rel}}_{A}} b \]

iff $a=b$.

8.3.3.6 The Symmetry

Definition 8.3.3.6.1 ▶ The Symmetry of $\mathsf{Rel}$

The symmetry of $\mathsf{Rel}$ is the natural isomorphism

whose component

\[ \sigma ^{\mathsf{Rel}}_{A,B} \colon A\times B \to B\times A \]

at $(A,B)$ is defined by declaring

\[ (a,b) \sim _{\sigma ^{\mathsf{Rel}}_{A,B}} (b',a') \]

iff $a=a'$ and $b=b'$.

8.3.3.7 The Internal Hom

Definition 8.3.3.7.1 ▶ The Internal Hom of $\mathsf{Rel}$

The internal Hom of $\mathsf{Rel}$ is the functor

\[ \mathrm{Rel}\colon \mathsf{Rel}^{\mathsf{op}}\times \mathsf{Rel}\to \mathsf{Rel} \]

defined

•
On objects by sending $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$ to the set $\mathrm{Rel}(A,B)$ of of .
•
On morphisms by pre/post-composition defined as in Definition 8.1.3.1.1.

Proposition 8.3.3.7.2 ▶ Properties of the Internal Hom of $\mathsf{Rel}$

Let $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$.

1.
Adjointness. We have adjunctions
witnessed by bijections

\begin{align*} \mathrm{Rel}(A\times B,C) & \cong \mathrm{Rel}(A,\mathrm{Rel}(B,C)),\\ \mathrm{Rel}(A\times B,C) & \cong \mathrm{Rel}(B,\mathrm{Rel}(A,C)), \end{align*}

natural in $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Rel})$.

Proof of Proposition 8.3.3.7.2.

Item 1: Adjointness

Indeed, we have

\begin{align*} \mathrm{Rel}(A\times B,C) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{Sets}(A\times B\times C,\{ \mathsf{true},\mathsf{false}\} )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}(A,B\times C)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}(A,\mathrm{Rel}(B,C)), \end{align*}

and similarly for the bijection $\mathrm{Rel}(A\times B,C)\cong \mathrm{Rel}(B,\mathrm{Rel}(A,C))$.

8.3.3.8 The Closed Symmetric Monoidal Category of Relations

Proposition 8.3.3.8.1 ▶ The Closed Symmetric Monoidal Category of Relations

The category $\mathsf{Rel}$ admits a closed symmetric monoidal category structure consisting of¹

•
The Underlying Category. The category $\mathsf{Rel}$ of sets and relations of Definition 8.3.2.1.1.
•
The Monoidal Product. The functor

\[ \times \colon \mathrm{Rel}\times \mathrm{Rel}\to \mathrm{Rel} \]

of Definition 8.3.3.1.1.
•
The Internal Hom. The internal Hom functor

\[ \mathbf{Rel}\colon \mathrm{Rel}^{\mathsf{op}}\times \mathrm{Rel}\to \mathrm{Rel} \]

of Definition 8.3.3.7.1.
•
The Monoidal Unit. The functor

\[ \mathbb {1}^{\mathrm{Rel}} \colon \mathsf{pt}\to \mathrm{Rel} \]

of Definition 8.3.3.2.1.
•
The Associators. The natural isomorphism

\[ \alpha ^{\mathrm{Rel}} \colon {\times }\circ {({\times }\times \operatorname {\mathrm{id}}_{\mathrm{Rel}})} \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}{\times }\circ {(\operatorname {\mathrm{id}}_{\mathrm{Rel}}\times {\times })}\circ {\mathbf{\alpha }^{\mathsf{Cats}}_{\mathrm{Rel},\mathrm{Rel},\mathrm{Rel}}} \]

of Definition 8.3.3.3.1.
•
The Left Unitors. The natural isomorphism

\[ \lambda ^{\mathrm{Rel}}\colon {\times }\circ {(\mathbb {1}^{\mathrm{Rel}}\times \operatorname {\mathrm{id}}_{\mathrm{Rel}})} \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}\mathbf{\lambda }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathrm{Rel}} \]

of Definition 8.3.3.4.1.
•
The Right Unitors. The natural isomorphism

\[ \rho ^{\mathrm{Rel}}\colon {\times }\circ {({\mathsf{id}}\times {\mathbb {1}^{\mathrm{Rel}}})}\mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}\mathbf{\rho }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathrm{Rel}} \]

of Definition 8.3.3.5.1.
•
The Symmetry. The natural isomorphism

\[ \sigma ^{\mathrm{Rel}} \colon {\times } \mathbin {\overset {\mathord {\sim }}{\Longrightarrow }}{\times }\circ {\mathbf{\sigma }^{\mathsf{Cats}_{\mathsf{2}}}_{\mathrm{Rel},\mathrm{Rel}}} \]

of Definition 8.3.3.6.1.

¹Warning: This is not a Cartesian monoidal structure, as the product on $\mathsf{Rel}$ is in fact given by the disjoint union of sets; see Chapter 9: Constructions With Relations, .

Proof of Proposition 8.3.3.8.1.

Omitted.

Statistics Cite

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

•Email
•Discord

You can also use the contact form below: