Item 3 (00RN) — The Clowder Project

8.5.1 Direct Images

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

The direct image function associated to $R$ is the function

\[ R_{!}\colon \mathcal{P}\webleft (A\webright )\to \mathcal{P}\webleft (B\webright ) \]

defined by^1,2,3

\begin{align*} R_{!}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}R\webleft (a\webright )\\ & = \left\{ b\in B\ \middle |\ \begin{aligned} & \text{there exists some $a\in U$}\\ & \text{such that $b\in R\webleft (a\webright )$} \end{aligned} \right\} \end{align*}

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

¹Further Notation: The set $R_{!}\webleft (U\webright )$ is also denoted $R\webleft (U\webright )$.
²Further Terminology: The set $R\webleft (U\webright )$ is called the direct image of $U$ by $R$.
³We also have
\[ R_{!}\webleft (U\webright )=B\setminus R_{*}\webleft (A\setminus U\webright ); \]
see Item 7 of Proposition 8.5.1.1.3.

Remark 8.5.1.1.2 ▶ Unwinding Definition 8.5.1.1.1

Identifying subsets of $A$ with relations from $\mathrm{pt}$ to $A$ via Chapter 4: Constructions With Sets, of , we see that the direct image function associated to $R$ is equivalently the function

\[ R_{!}\colon \underbrace{\mathcal{P}\webleft (A\webright )}_{\cong \mathrm{Rel}\webleft (\mathrm{pt},A\webright )} \to \underbrace{\mathcal{P}\webleft (B\webright )}_{\cong \mathrm{Rel}\webleft (\mathrm{pt},B\webright )} \]

defined by

\[ R_{!}\webleft (U\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R\mathbin {\diamond }U \]

for each $U\in \mathcal{P}\webleft (A\webright )$, where $R\mathbin {\diamond }U$ is the composition

\[ \mathrm{pt}\mathbin {\overset {U}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}A\mathbin {\overset {R}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}B. \]

Proposition 8.5.1.1.3 ▶ Properties of Direct Image Functions

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

\[ \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:
- (★)
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 $\left\{ U_{i}\right\} _{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 $\left\{ U_{i}\right\} _{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 Codirect Images. We have

\[ R_{!}\webleft (U\webright )=B\setminus R_{*}\webleft (A\setminus U\webright ) \]

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

Proof of Proposition 8.5.1.1.3.

Item 1: Functoriality

Clear.

Item 2: Adjointness

This follows from

Item 3: Preservation of Colimits

This follows from Item 2 and

Item 4: Oplax Preservation of Limits

Omitted.

Item 5: Symmetric Strict Monoidality With Respect to Unions

This follows from Item 3.

Item 6: Symmetric Oplax Monoidality With Respect to Intersections

This follows from Item 4.

Item 7: 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 7 of Proposition 8.5.4.1.3 to $A\setminus U$, we have

\begin{align*} R_{*}\webleft (A\setminus U\webright ) & = B\setminus R_{!}\webleft (A\setminus \webleft (A\setminus U\webright )\webright )\\ & = B\setminus R_{!}\webleft (U\webright ). \end{align*}

Taking complements, we then obtain

\begin{align*} R_{!}\webleft (U\webright ) & = B\setminus \webleft (B\setminus R_{!}\webleft (U\webright )\webright ),\\ & = B\setminus R_{*}\webleft (A\setminus U\webright ), \end{align*}

which finishes the proof.

Proposition 8.5.1.1.4 ▶ Properties of the Direct Image Function Operation

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 \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, we have¹

\[ \webleft (\chi _{A}\webright )_{!}=\operatorname {\mathrm{id}}_{\mathcal{P}\webleft (A\webright )}. \]

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 (\mathrm{pt},A\webright )\to \mathrm{Rel}\webleft (\mathrm{pt},A\webright ) \]
is equal to $\operatorname {\mathrm{id}}_{\mathrm{Rel}\webleft (\mathrm{pt},A\webright )}$.
²That is, we have

Proof of Proposition 8.5.1.1.4.

Item 1: Functionality I

Clear.

Item 2: Functionality II

Clear.

Item 3: Interaction With Identities

Indeed, we have

\begin{align*} \webleft (\chi _{A}\webright )_{!}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}\chi _{A}\webleft (a\webright )\\ & \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}\webleft (A\webright )}\webleft (U\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (A\webright )$. Thus $\webleft (\chi _{A}\webright )_{!}=\operatorname {\mathrm{id}}_{\mathcal{P}\webleft (A\webright )}$.

Item 4: Interaction With Composition

Indeed, we have

\begin{align*} \webleft (S\mathbin {\diamond }R\webright )_{!}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}\webleft [S\mathbin {\diamond }R\webright ]\webleft (a\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}S\webleft (R\webleft (a\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\bigcup _{a\in U}S_{!}\webleft (R\webleft (a\webright )\webright )\\ & = S_{!}\webleft (\bigcup _{a\in U}R\webleft (a\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S_{!}\webleft (R_{!}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [S_{!}\circ R_{!}\webright ]\webleft (U\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (A\webright )$, where we used Item 3 of Proposition 8.5.1.1.3. Thus $\webleft (S\mathbin {\diamond }R\webright )_{!}=S_{!}\circ R_{!}$.

Statistics Cite

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

•Email
•Discord

You can also use the contact form below: