The Clowder Project

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

1. Functoriality. The assignment $U\mapsto R_{*}\webleft (U\webright )$ defines a functor
   \[ R_{*}\colon \webleft (\mathcal{P}\webleft (A\webright ),\subset \webright )\to \webleft (\mathcal{P}\webleft (B\webright ),\subset \webright ) \]

   where

   • Action on Objects. For each $U\in \mathcal{P}\webleft (A\webright )$, we have
     \[ \webleft [R_{*}\webright ]\webleft (U\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R_{*}\webleft (U\webright ); \]

   • Action on Morphisms. For each $U,V\in \mathcal{P}\webleft (A\webright )$:
     • If $U\subset V$, then $R_{*}\webleft (U\webright )\subset R_{*}\webleft (V\webright )$.

2. Adjointness. We have an adjunction
   
   witnessed by a bijections of sets
   \[ \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (R_{*}\webleft (U\webright ),V\webright )\cong \textup{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. Preservation of Colimits. We have an equality of sets
   \[ R_{*}\webleft (\bigcup _{i\in I}U_{i}\webright )=\bigcup _{i\in I}R_{*}\webleft (U_{i}\webright ), \]

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

   \[ \begin{gathered} R_{*}\webleft (U\webright )\cup R_{*}\webleft (V\webright ) = R_{*}\webleft (U\cup V\webright ),\\ R_{*}\webleft (\text{Ø}\webright ) = \text{Ø}, \end{gathered} \]

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

4. Oplax Preservation of Limits. We have an inclusion of sets
   \[ R_{*}\webleft (\bigcap _{i\in I}U_{i}\webright )\subset \bigcap _{i\in I}R_{*}\webleft (U_{i}\webright ), \]

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

   \[ \begin{gathered} R_{*}\webleft (U\cap V\webright ) \subset R_{*}\webleft (U\webright )\cap R_{*}\webleft (V\webright ),\\ R_{*}\webleft (A\webright ) \subset B, \end{gathered} \]

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

5. Symmetric Strict Monoidality With Respect to Unions. The direct image function of Item 1 has a symmetric strict monoidal structure
   \[ \webleft (R_{*},R^{\otimes }_{*},R^{\otimes }_{*|\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 equalities

   \[ \begin{gathered} R^{\otimes }_{*|U,V} \colon R_{*}\webleft (U\webright )\cup R_{*}\webleft (V\webright ) \mathbin {\overset {=}{\rightarrow }}R_{*}\webleft (U\cup V\webright ),\\ R^{\otimes }_{*|\mathbb {1}} \colon \text{Ø}\mathbin {\overset {=}{\rightarrow }}\text{Ø}, \end{gathered} \]

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

6. Symmetric Oplax Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric oplax monoidal structure
   \[ \webleft (R_{*},R^{\otimes }_{*},R^{\otimes }_{*|\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 inclusions

   \[ \begin{gathered} R^{\otimes }_{*|U,V} \colon R_{*}\webleft (U\cap V\webright ) \subset R_{*}\webleft (U\webright )\cap R_{*}\webleft (V\webright ),\\ R^{\otimes }_{*|\mathbb {1}} \colon R_{*}\webleft (A\webright ) \subset B, \end{gathered} \]

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

7. Relation to Direct Images With Compact Support. We have
   \[ R_{*}\webleft (U\webright )=B\setminus R_{!}\webleft (A\setminus U\webright ) \]

   for each $U\in \mathcal{P}\webleft (A\webright )$.

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

1. Functionality I. The assignment $R\mapsto R_{*}$ defines a function
   \[ \webleft (-\webright )_{*}\colon \mathrm{Rel}\webleft (A,B\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (A\webright ),\mathcal{P}\webleft (B\webright )\webright ). \]
2. Functionality II. The assignment $R\mapsto R_{*}$ defines a function
   \[ \webleft (-\webright )_{*}\colon \mathrm{Rel}\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. Interaction With Identities. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have¹
   \[ \webleft (\chi _{A}\webright )_{*}=\text{id}_{\mathcal{P}\webleft (A\webright )}; \]
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²
   

---

¹That is, the postcomposition function

\[ \webleft (\chi _{A}\webright )_{*}\colon \mathrm{Rel}\webleft (\text{pt},A\webright )\to \mathrm{Rel}\webleft (\text{pt},A\webright ) \]

is equal to $\text{id}_{\mathrm{Rel}\webleft (\text{pt},A\webright )}$.

²That is, we have