The Clowder Project

Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.

1. 1.

   Functoriality. The assignment $V\mapsto R_{-1}\webleft (V\webright )$ defines a functor

   \[ R_{-1}\colon \webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )\to \webleft (\mathcal{P}\webleft (A\webright ),\subset \webright ) \]

   where

   • •

     Action on Objects. For each $V\in \mathcal{P}\webleft (B\webright )$, we have

     \[ \webleft [R_{-1}\webright ]\webleft (V\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R_{-1}\webleft (V\webright ). \]
   • •

     Action on Morphisms. For each $U,V\in \mathcal{P}\webleft (B\webright )$:

     • •

       If $U\subset V$, then $R_{-1}\webleft (U\webright )\subset R_{-1}\webleft (V\webright )$.

2. 2.

   Adjointness. We have an adjunction

   
   witnessed by a bijections of sets
   \[ \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (A\webright )}\webleft (R_{!}\webleft (U\webright ),V\webright )\cong \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (A\webright )}\webleft (U,R_{-1}\webleft (V\webright )\webright ), \]

   natural in $U\in \mathcal{P}\webleft (A\webright )$ and $V\in \mathcal{P}\webleft (B\webright )$, i.e. such that:

   • (★)
   The following conditions are equivalent:
   • •

     We have $R_{!}\webleft (U\webright )\subset V$.

   • •

     We have $U\subset R_{-1}\webleft (V\webright )$.

3. 3.

   Lax Preservation of Colimits. We have an inclusion of sets

   \[ \bigcup _{i\in I}R_{-1}\webleft (U_{i}\webright )\subset R_{-1}\webleft (\bigcup _{i\in I}U_{i}\webright ), \]

   natural in $\left\{ U_{i}\right\} _{i\in I}\in \mathcal{P}\webleft (B\webright )^{\times I}$. In particular, we have inclusions

   \[ \begin{gathered} R_{-1}\webleft (U\webright )\cup R_{-1}\webleft (V\webright ) \subset R_{-1}\webleft (U\cup V\webright ),\\ \text{Ø}\subset R_{-1}\webleft (\text{Ø}\webright ), \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

4. 4.

   Preservation of Limits. We have an equality of sets

   \[ R_{-1}\webleft (\bigcap _{i\in I}U_{i}\webright )=\bigcap _{i\in I}R_{-1}\webleft (U_{i}\webright ), \]

   natural in $\left\{ U_{i}\right\} _{i\in I}\in \mathcal{P}\webleft (B\webright )^{\times I}$. In particular, we have equalities

   \[ \begin{gathered} R_{-1}\webleft (U\cap V\webright ) = R_{-1}\webleft (U\webright )\cap R_{-1}\webleft (V\webright ),\\ R_{-1}\webleft (B\webright ) = B, \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

5. 5.

   Symmetric Lax Monoidality With Respect to Unions. The codirect image function of Item 1 has a symmetric lax monoidal structure

   \[ \webleft (R_{-1},R^{\otimes }_{-1},R^{\otimes }_{-1|\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (A\webright ),\cup ,\text{Ø}\webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cup ,\text{Ø}\webright ), \]

   being equipped with inclusions

   \[ \begin{gathered} R^{\otimes }_{-1|U,V} \colon R_{-1}\webleft (U\webright )\cup R_{-1}\webleft (V\webright ) \subset R_{-1}\webleft (U\cup V\webright ),\\ R^{\otimes }_{-1|\mathbb {1}} \colon \text{Ø}\subset R_{-1}\webleft (\text{Ø}\webright ), \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

6. 6.

   Symmetric Strict Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric strict monoidal structure

   \[ \webleft (R_{-1},R^{\otimes }_{-1},R^{\otimes }_{-1|\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (A\webright ),\cap ,A\webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cap ,B\webright ), \]

   being equipped with equalities

   \[ \begin{gathered} R^{\otimes }_{-1|U,V} \colon R_{-1}\webleft (U\cap V\webright ) \mathbin {\overset {=}{\rightarrow }}R_{-1}\webleft (U\webright )\cap R_{-1}\webleft (V\webright ),\\ R^{\otimes }_{-1|\mathbb {1}} \colon R_{-1}\webleft (A\webright ) \mathbin {\overset {=}{\rightarrow }}B, \end{gathered} \]

   natural in $U,V\in \mathcal{P}\webleft (B\webright )$.

7. 7.

   Interaction With Weak Inverse Images I. We have

   \[ R_{-1}\webleft (V\webright )=A\setminus R^{-1}\webleft (B\setminus V\webright ) \]

   for each $V\in \mathcal{P}\webleft (B\webright )$.

8. 8.

   Interaction With Weak Inverse Images II. Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation from $A$ to $B$.

   1. (a)

      If $R$ is a total relation, then we have an inclusion of sets

      \[ R_{-1}\webleft (V\webright ) \subset R^{-1}\webleft (V\webright ) \]

      natural in $V\in \mathcal{P}\webleft (B\webright )$.

   2. (b)

      If $R$ is total and functional, then the above inclusion is in fact an equality.

Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.

1. 1.

   Functionality I. The assignment $R\mapsto R_{-1}$ defines a function

   \[ \webleft (-\webright )_{-1}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ). \]
2. 2.

   Functionality II. The assignment $R\mapsto R_{-1}$ defines a function

   \[ \webleft (-\webright )_{-1}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )\webright ). \]
3. 3.

   Interaction With Identities. For each $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, we have

   \[ \webleft (\operatorname {\mathrm{id}}_{A}\webright )_{-1}=\operatorname {\mathrm{id}}_{\mathcal{P}\webleft (A\webright )}. \]
4. 4.

   Interaction With Composition. For each pair of composable relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ and $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$, we have