The inverse image function associated to $R$ is the function
defined by1
for each $V\in \mathcal{P}(Y)$.
- 1Further Terminology: The set $R^{-1}(V)$ is called the inverse image of $V$ by $R$ or simply the inverse image of $V$ by $R$.
Let $X$ and $Y$ be sets and let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y$ be a relation.
The inverse image function associated to $R$ is the function
defined by1
for each $V\in \mathcal{P}(Y)$.
Identifying $\mathcal{P}(Y)$ with $\mathrm{Rel}(Y,\mathrm{pt})$ via Chapter 4: Constructions With Sets, Item 3 of Proposition 4.4.1.1.4, we see that the inverse image function associated to $R$ is equivalently the function
defined by
for each $V\in \mathcal{P}(X)$, where $R\mathbin {\diamond }V$ is the composition
We have
This finishes the proof.
Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y$ be a relation.
Functoriality. The assignment $V\mapsto R^{-1}(V)$ defines a functor
In particular, for each $U,V\in \mathcal{P}(Y)$, the following condition is satisfied:
Adjointness. We have an adjunction
Units and counits of the form
In particular:
For each $V\in \mathcal{P}(Y)$, we have $V\subset R_{*}(R^{-1}(V))$.
For each $U\in \mathcal{P}(X)$, we have $R^{-1}(R_{*}(U))\subset U$.
A bijections of sets
natural in $U\in \mathcal{P}(X)$ and $V\in \mathcal{P}(Y)$. In particular:
We have $R^{-1}(U)\subset V$.
We have $U\subset R_{*}(V)$.
Interaction With Unions of Families of Subsets. The diagram
for each $\mathcal{U}\in \mathcal{P}(X)$, where $R^{-1}(\mathcal{U})\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(R^{-1})_{!}(\mathcal{U})$.
Interaction With Intersections of Families of Subsets. The diagram
for each $\mathcal{U}\in \mathcal{P}(X)$, where $R^{-1}(\mathcal{U})\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(R^{-1})_{!}(\mathcal{U})$.
Interaction With Binary Unions. The diagram
for each $U,V\in \mathcal{P}(X)$.
Interaction With Binary Intersections. We have a natural transformation
indexed by $U,V\in \mathcal{P}(X)$.
Interaction With Differences. We have a natural transformation
indexed by $U,V\in \mathcal{P}(X)$.
Interaction With Complements. The diagram
for each $U\in \mathcal{P}(X)$.
Interaction With Symmetric Differences. We have a natural transformation
indexed by $U,V\in \mathcal{P}(X)$.
Interaction With Internal Homs of Powersets. The diagram
natural in $U,V\in \mathcal{P}(X)$.
Preservation of Colimits. We have an equality of sets
natural in $\left\{ U_{i}\right\} _{i\in I}\in \mathcal{P}(Y)^{\times I}$. In particular, we have equalities
natural in $U,V\in \mathcal{P}(Y)$.
Oplax Preservation of Limits. We have an inclusion of sets
natural in $\left\{ U_{i}\right\} _{i\in I}\in \mathcal{P}(Y)^{\times I}$. In particular, we have inclusions
natural in $U,V\in \mathcal{P}(Y)$.
Symmetric Strict Monoidality With Respect to Unions. The direct image function of Item 1 has a symmetric strict monoidal structure
being equipped with equalities
natural in $U,V\in \mathcal{P}(Y)$.
Symmetric Oplax Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric oplax monoidal structure
being equipped with inclusions
natural in $U,V\in \mathcal{P}(Y)$.
Interaction With Coproducts. Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X'$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y'$ be relations. The diagram
for each $U'\in \mathcal{P}(X')$ and each $V'\in \mathcal{P}(Y')$.
Interaction With Products. Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X'$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y'$ be relations. The diagram
for each $U'\in \mathcal{P}(X')$ and each $V'\in \mathcal{P}(Y')$.
Relation to Coinverse Images. We have
for each $V\in \mathcal{P}(Y)$.
Interaction With Functional Relations. If $R$ is functional, then we have
so
for each $V\in \mathcal{P}(Y)$.
Interaction With Total Relations. If $R$ is total, then we have
so
for each $V\in \mathcal{P}(Y)$.
Interaction With Functions I. If $R$ is a function, then we have
so $R_{-1}=R^{-1}$.
Interaction With Functions II. If $R_{-1}=R^{-1}$, then $R$ is a function.
This finishes the proof.
This finishes the proof.
where we have used Chapter 4: Constructions With Sets, Item 8 of Proposition 4.3.9.1.2 for the fourth equality.
This finishes the proof.
Since $\mathcal{P}(X)$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2). This finishes the proof.
This finishes the proof.
where we have used:
Chapter 4: Constructions With Sets, Item 2 of Proposition 4.3.12.1.2 for the first equality.
Item 6 of this proposition together with Chapter 4: Constructions With Sets, Item 1 of Proposition 4.3.10.1.2 for the first inclusion.
Item 5 for the second equality.
Item 7 for the second inclusion.
Chapter 4: Constructions With Sets, Item 2 of Proposition 4.3.12.1.2 for the last equality.
Since $\mathcal{P}(X)$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2). This finishes the proof.
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.
Let $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y$ be a relation.
Functionality I. The assignment $R\mapsto R^{-1}$ defines a function
Functionality II. The assignment $R\mapsto R^{-1}$ defines a function
Interaction With Identities. For each $X\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, we have
Interaction With Composition. For each pair of composable relations $R\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}Y$ and $S\colon Y\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$, we have
Interaction With Converses. We have