8.3.3.7 The Internal Hom

    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}}\webleft (\mathsf{Rel}\webright )$ to the set $\mathrm{Rel}\webleft (A,B\webright )$ of Unresolved reference of Unresolved reference.

    • On morphisms by pre/post-composition defined as in Chapter 9: Constructions With Relations, Unresolved reference.

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

  • 1.

    Adjointness. We have adjunctions

    witnessed by bijections

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

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

  • Item 1: Adjointness
    Indeed, we have

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

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


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


You can also use the contact form below: