Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.
-
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 )$.
- Action on Objects. For each $U\in \mathcal{P}\webleft (A\webright )$, we have
-
Adjointness. We have an adjunction witnessed by a bijections of sets
\[ \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (R^{-1}\webleft (U\webright ),V\webright )\cong \textup{Hom}_{\mathcal{P}\webleft (A\webright )}\webleft (U,R_{!}\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^{-1}\webleft (U\webright )\subset V$;
- We have $U\subset R_{!}\webleft (V\webright )$.
- The following conditions are equivalent:
-
Lax Preservation of Colimits. We have an inclusion of sets
\[ \bigcup _{i\in I}R_{!}\webleft (U_{i}\webright )\subset R_{!}\webleft (\bigcup _{i\in I}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\webright )\cup R_{!}\webleft (V\webright ) \subset R_{!}\webleft (U\cup V\webright ),\\ \text{Ø}\subset R_{!}\webleft (\text{Ø}\webright ), \end{gathered} \]natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
-
Preservation of Limits. We have an equality of sets
\[ R_{!}\webleft (\bigcap _{i\in I}U_{i}\webright )=\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 equalities
\[ \begin{gathered} R_{!}\webleft (U\cap V\webright ) = R_{!}\webleft (U\webright )\cap R_{!}\webleft (V\webright ),\\ R_{!}\webleft (A\webright ) = B, \end{gathered} \]natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
-
Symmetric Lax Monoidality With Respect to Unions. The direct image with compact support function of Item 1 has a symmetric lax 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 inclusions
\[ \begin{gathered} R^{\otimes }_{!|U,V} \colon R_{!}\webleft (U\webright )\cup R_{!}\webleft (V\webright ) \subset R_{!}\webleft (U\cup V\webright ),\\ R^{\otimes }_{!|\mathbb {1}} \colon \text{Ø}\subset R_{!}\webleft (\text{Ø}\webright ), \end{gathered} \]natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
-
Symmetric Strict Monoidality With Respect to Intersections. 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 ),\cap ,A\webright ) \to \webleft (\mathcal{P}\webleft (B\webright ),\cap ,B\webright ), \]
being equipped with equalities
\[ \begin{gathered} R^{\otimes }_{!|U,V} \colon R_{!}\webleft (U\cap V\webright ) \mathbin {\overset {=}{\rightarrow }}R_{!}\webleft (U\webright )\cap R_{!}\webleft (V\webright ),\\ R^{\otimes }_{!|\mathbb {1}} \colon R_{!}\webleft (A\webright ) \mathbin {\overset {=}{\rightarrow }}B, \end{gathered} \]natural in $U,V\in \mathcal{P}\webleft (A\webright )$.
-
Relation to Direct Images. We have
\[ R_{!}\webleft (U\webright )=B\setminus R_{*}\webleft (A\setminus U\webright ) \]
for each $U\in \mathcal{P}\webleft (A\webright )$.