Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y$ be a relation.
The direct image function associated to $R$ is the function
\[ R_{!}\colon \mathcal{P}(X)\to \mathcal{P}(Y) \]
defined by
\begin{align*} R_{!}(U) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ b\in Y\ \middle |\ R^{-1}(b)\cap U\neq \text{Ø}\right\} \\ & = \left\{ b\in Y\ \middle |\ \begin{aligned} & \text{there exists some $a\in U$}\\ & \text{such that $b\in R(a)$} \end{aligned} \right\} \\ & = \bigcup _{a\in U}R(a) \end{align*}
for each $U\in \mathcal{P}(X)$.
Omitted.
This follows from Remark 8.7.1.1.3, Remark 8.7.2.1.2 and 
, of .
Item 3: Interaction With Unions of Families of Subsets
We have
\begin{align*} \bigcup _{V\in R_{!}(\mathcal{U})}V & = \bigcup _{V\in \left\{ R_{!}(U)\in \mathcal{P}(X)\ \middle |\ U\in \mathcal{U}\right\} }V\\ & = \bigcup _{U\in \mathcal{U}}R_{!}(U).\end{align*}
This finishes the proof.
Item 4: Interaction With Intersections of Families of Subsets
We have
\begin{align*} \bigcap _{V\in R_{!}(\mathcal{U})}V & = \bigcap _{V\in \left\{ R_{!}(U)\in \mathcal{P}(X)\ \middle |\ U\in \mathcal{U}\right\} }V\\ & = \bigcap _{U\in \mathcal{U}}R_{!}(U).\end{align*}
This finishes the proof.
Item 5: Interaction With Binary Unions
We have
\begin{align*} R_{!}(U\cup V) & = \bigcup _{a\in U\cup V}R(a)\\ & = \left(\bigcup _{a\in U}R(a)\right)\cup \left(\bigcup _{a\in V}R(a)\right)\\ & = R_{!}(U)\cup R_{!}(V). \end{align*}
This finishes the proof.
Item 6: Interaction With Binary Intersections
We have
\begin{align*} R_{!}(U\cap V) & = \bigcup _{a\in U\cap V}R(a)\\ & \subset \left(\bigcup _{a\in U}R(a)\right)\cap \left(\bigcup _{a\in V}R(a)\right)\\ & = R_{!}(U)\cap R_{!}(V), \end{align*}
where we have used Chapter 4: Constructions With Sets, Item 7 of Proposition 4.3.6.1.2 by taking
\begin{align*} \mathcal{U} & = \left\{ R(a)\in \mathcal{P}(Y)\ \middle |\ a\in U\right\} ,\\ \mathcal{V} & = \left\{ R(a)\in \mathcal{P}(Y)\ \middle |\ a\in V\right\} . \end{align*}
Since $\mathcal{P}(Y)$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2).
Item 7: Interaction With Differences
See [[Unknown Reference: proof-wiki:image-of-set-difference-under-relation]].
Item 8: Interaction With Complements
Applying Item 17 to $X\setminus U$, we have
\begin{align*} R_{!}(U^{\textsf{c}}) & = R_{!}(X\setminus U)\\ & = Y\setminus R_{*}(X\setminus (X\setminus U))\\ & = Y\setminus R_{*}(U)\\ & = R_{*}(U)^{\textsf{c}}. \end{align*}
This finishes the proof.
Item 9: Interaction With Binary Symmetric Differences
We have
\begin{align*} R_{!}(U)\mathbin {\triangle }R_{!}(V) & = (R_{!}(U)\cup R_{!}(V))\setminus (R_{!}(U)\cap R_{!}(V))\\ & \subset (R_{!}(U)\cup R_{!}(V))\setminus (R_{!}(U\cap V))\\ & = (R_{!}(U\cup V))\setminus (R_{!}(U\cap V))\\ & \subset R_{!}((U\cup V)\setminus (U\cap V))\\ & = R_{!}(U\mathbin {\triangle }V), \end{align*}
where we have used:
Since $\mathcal{P}(Y)$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2). This finishes the proof.
Item 10: Interaction With Internal Homs of Powersets
We have
\begin{align*} R_{!}([U,V]_{X}) & = R_{!}(U^{\textsf{c}}\cup V)\\ & = R_{!}(U^{\textsf{c}})\cup R_{!}(V)\\ & = R_{*}(U)^{\textsf{c}}\cup R_{!}(V)\\ & = [R_{*}(U),R_{!}(V)]_{Y},\end{align*}
where we have used:
-
•
Item 5 for the second equality.
-
•
Item 17 for the third equality.
Since $\mathcal{P}(Y)$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2). This finishes the proof.
This follows from Item 2 and , of .
Item 12: Oplax Preservation of Limits
Omitted.
Item 13: Symmetric Strict Monoidality With Respect to Unions
This follows from Item 11.
Item 14: Symmetric Oplax Monoidality With Respect to Intersections
This follows from Item 12.
Item 15: Interaction With Coproducts
Omitted.
Omitted.
Item 17: Relation to Codirect Images
The proof proceeds in the same way as in the case of functions (Chapter 4: Constructions With Sets, Item 17 of Proposition 4.6.1.1.5): applying Item 17 of Proposition 8.7.4.1.4 to $A\setminus U$, we have
\begin{align*} R_{*}(X\setminus U) & = Y\setminus R_{!}(X\setminus (X\setminus U))\\ & = Y\setminus R_{!}(U). \end{align*}
Taking complements, we then obtain
\begin{align*} R_{!}(U) & = Y\setminus (Y\setminus R_{!}(U)),\\ & = Y\setminus R_{*}(X\setminus U), \end{align*}
which finishes the proof.
There is nothing to prove.
This follows from Item 1 of Proposition 8.7.1.1.4.
Item 3: Interaction With Identities
Indeed, we have
\begin{align*} (\chi _{X})_{!}(U) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}\chi _{X}(a)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}\left\{ a\right\} \\ & = U\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{id}}_{\mathcal{P}(X)}(U) \end{align*}
for each $U\in \mathcal{P}(X)$. Thus $(\chi _{X})_{!}=\operatorname {\mathrm{id}}_{\mathcal{P}(X)}$.
Item 4: Interaction With Composition
Indeed, we have
\begin{align*} (S\mathbin {\diamond }R)_{!}(U) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}[S\mathbin {\diamond }R](a)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}S(R(a))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}S_{!}(R(a))\\ & = S_{!}\left(\bigcup _{a\in U}R(a)\right)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S_{!}(R_{!}(U))\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}[S_{!}\circ R_{!}](U) \end{align*}
for each $U\in \mathcal{P}(X)$, where we used Item 11 of Proposition 8.7.1.1.4. Thus $(S\mathbin {\diamond }R)_{!}=S_{!}\circ R_{!}$.
Item 5: Interaction With Converses
Omitted.
