Proposition 7.4.1.1.4 (00RK): Properties of the Direct Image Function Operation

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

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

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 ). \]
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 ). \]
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 )}; \]
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

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}\webleft\{ a\webright\} \\ & = U\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\text{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 )_{*}=\text{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 7.4.1.1.3. Thus $\webleft (S\mathbin {\diamond }R\webright )_{*}=S_{*}\circ R_{*}$.