Item 2 (00T9) — The Clowder Project

8.5.4 Codirect 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 codirect 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

\begin{align*} R_{*}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ b\in B\ \middle |\ \begin{aligned} & \text{for each $a\in A$, if we have}\\ & \text{$b\in R\webleft (a\webright )$, then $a\in U$}\end{aligned} \right\} \\ & = \left\{ b\in B\ \middle |\ R^{-1}\webleft (b\webright )\subset U\right\} \end{align*}

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

¹Further Terminology: The set $R_{*}\webleft (U\webright )$ is called the codirect 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.4.1.3.

Remark 8.5.4.1.2 ▶ Unwinding Definition 8.5.4.1.1

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

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

defined by

being explicitly computed by

\begin{align*} R^{*}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{Ran}}_{R}\webleft (U\webright )\\ & \cong \int _{a\in A}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{-_{2}}_{a},U^{-_{1}}_{a}\webright ), \end{align*}

where we have used .

Proof of Remark 8.5.4.1.2.

We have

\begin{align*} \operatorname {\mathrm{Ran}}_{R}\webleft (V\webright )& \cong \int _{a\in A}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{-_{2}}_{a},U^{-_{1}}_{a}\webright )\\ & =\left\{ b\in B\ \middle |\ \int _{a\in A}\operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (R^{b}_{a},U^{\star }_{a}\webright )=\mathsf{true}\right\} \\ & = \left\{ b\in B\ \middle |\ \begin{aligned} & \text{for each $a\in A$, at least one of the}\\[-2.5pt]& \text{following conditions hold:}\\[7.5pt]& \mspace {25mu}\rlap {\text{1.}}\mspace {22.5mu}\text{We have $R^{b}_{a}=\mathsf{false}$}\\ & \mspace {25mu}\rlap {\text{2.}}\mspace {22.5mu}\text{The following conditions hold:}\\[7.5pt]& \mspace {50mu}\rlap {\text{(a)}}\mspace {30mu}\text{We have $R^{b}_{a}=\mathsf{true}$}\\ & \mspace {50mu}\rlap {\text{(b)}}\mspace {30mu}\text{We have $U^{\star }_{a}=\mathsf{true}$}\\[10pt]\end{aligned} \right\} \\ & = \left\{ b\in B\ \middle |\ \begin{aligned} & \text{for each $a\in A$, at least one of the}\\[-2.5pt]& \text{following conditions hold:}\\[7.5pt]& \mspace {25mu}\rlap {\text{1.}}\mspace {22.5mu}\text{We have $b\not\in R\webleft (A\webright )$}\\ & \mspace {25mu}\rlap {\text{2.}}\mspace {22.5mu}\text{The following conditions hold:}\\[7.5pt]& \mspace {50mu}\rlap {\text{(a)}}\mspace {30mu}\text{We have $b\in R\webleft (a\webright )$}\\ & \mspace {50mu}\rlap {\text{(b)}}\mspace {30mu}\text{We have $a\in U$}\\[10pt]\end{aligned} \right\} \\ & = \left\{ b\in B\ \middle |\ \begin{aligned} & \text{for each $a\in A$, if we have}\\ & \text{$b\in R\webleft (a\webright )$, then $a\in U$}\end{aligned} \right\} \\ & = \left\{ b\in B\ \middle |\ R^{-1}\webleft (b\webright )\subset U\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R^{-1}\webleft (U\webright ).\end{align*}

This finishes the proof.

Proposition 8.5.4.1.3 ▶ Properties of Codirect Images

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^{-1}\webleft (U\webright ),V\webright )\cong \operatorname {\mathrm{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:
- (★)
3.
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 $\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\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 )$.
4.
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 $\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\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 )$.
5.
Symmetric Lax Monoidality With Respect to Unions. The codirect image 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 )$.
6.
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 )$.
7.
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 )$.

Proof of Proposition 8.5.4.1.3.

Item 1: Functoriality

Clear.

Item 2: Adjointness

This follows from

Item 3: Lax Preservation of Colimits

Omitted.

Item 4: Preservation of Limits

This follows from Item 2 and

Item 5: Symmetric Lax Monoidality With Respect to Unions

This follows from Item 3.

Item 6: Symmetric Strict Monoidality With Respect to Intersections

This follows from Item 4.

Item 7: Relation to Direct Images

This follows from Item 7 of Proposition 8.5.1.1.3. Alternatively, we may prove it directly as follows, with the proof proceeding in the same way as in the case of functions (Chapter 4: Constructions With Sets, Item 16 of Proposition 4.6.3.1.7).

We claim that $R_{*}\webleft (U\webright )=B\setminus R_{!}\webleft (A\setminus U\webright )$:

•
The First Implication. We claim that

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

Let $b\in R_{*}\webleft (U\webright )$. We need to show that $b\not\in R_{!}\webleft (A\setminus U\webright )$, i.e. that there is no $a\in A\setminus U$ such that $b\in R\webleft (a\webright )$.

This is indeed the case, as otherwise we would have $a\in R^{-1}\webleft (b\webright )$ and $a\not\in U$, contradicting $R^{-1}\webleft (b\webright )\subset U$ (which holds since $b\in R_{*}\webleft (U\webright )$).

Thus $b\in B\setminus R_{!}\webleft (A\setminus U\webright )$.
•
The Second Implication. We claim that

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

Let $b\in B\setminus R_{!}\webleft (A\setminus U\webright )$. We need to show that $b\in R_{*}\webleft (U\webright )$, i.e. that $R^{-1}\webleft (b\webright )\subset U$.

Since $b\not\in R_{!}\webleft (A\setminus U\webright )$, there exists no $a\in A\setminus U$ such that $b\in R\webleft (a\webright )$, and hence $R^{-1}\webleft (b\webright )\subset U$.

Thus $b\in R_{*}\webleft (U\webright )$.

This finishes the proof.

Proposition 8.5.4.1.4 ▶ Properties of the Codirect 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 \mathsf{Sets}\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 \mathsf{Sets}\webleft (A,B\webright ) \to \operatorname {\mathrm{Hom}}_{\mathsf{Pos}}\webleft (\webleft (\mathcal{P}\webleft (A\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (B\webright ),\subset \webright )\webright ). \]

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

\[ \webleft (\operatorname {\mathrm{id}}_{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

Proof of Proposition 8.5.4.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}}}=}}\left\{ a\in A\ \middle |\ \chi ^{-1}_{A}\webleft (a\webright )\subset U\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ a\in A\ \middle |\ \left\{ a\right\} \subset U\right\} \\ & = U \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}}}=}}\left\{ c\in C\ \middle |\ \webleft [S\mathbin {\diamond }R\webright ]^{-1}\webleft (c\webright )\subset U\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ c\in C\ \middle |\ S^{-1}\webleft (R^{-1}\webleft (c\webright )\webright )\subset U\right\} \\ & = \left\{ c\in C\ \middle |\ R^{-1}\webleft (c\webright )\subset S_{*}\webleft (U\webright )\right\} \\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}R_{*}\webleft (S_{*}\webleft (U\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft [R_{*}\circ S_{*}\webright ]\webleft (U\webright ) \end{align*}

for each $U\in \mathcal{P}\webleft (C\webright )$, where we used Item 2 of Proposition 8.5.4.1.3, which implies that the conditions

•
We have $S^{-1}\webleft (R^{-1}\webleft (c\webright )\webright )\subset U$.
•
We have $R^{-1}\webleft (c\webright )\subset S_{*}\webleft (U\webright )$.

are equivalent. 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: