Powerset functors

Definition 41   The powerset of a set A is the set of all subsets of A. Standard notations for this include P(A), ${\cal P}(A)$ and 2^A.

Proposition 5.1   ${\cal P}(A)$ is partially ordered by $\subseteq$ with largest element A and smallest element $\emptyset$.

There are three ways to define functions on the powerset from a function

$$f:A\to B$$

Definition 42   The inverse image functor $f^*:{\cal P}(B)\to {\cal P}(A)$ takes a subset B' to the set

$$f^*(B')=\{a\vert a\in A \mbox{ and } f(a)\in B'\}.$$

This is also sometimes (confusingly) written f^-1(B').

Definition 43   The direct image functor $\exists_f:{\cal P}(A) \to {\cal P}(B)$ takes the subset A' to the set

$$\exists_f(A')=\{b\vert b\in B \mbox{ and there is an }a\in A' \mbox{ with } b=f(a)\}.$$

This functor is sometimes (again, somewhat confusingly) written as f(A').

Definition 44   The universal quantification functor $\forall_f:{\cal P}(A) \to {\cal P}(B)$ takes the subset A' to the set

$$\forall_f(A')=\{b\vert b\in B \mbox{ and every }a\in A \mbox{ with } b=f(a) \mbox{ has }a \in A'\}.$$

This functor is much less used than the inverse image and direct image functors.

Proposition 5.2   The function $f^*:{\cal P}(B)\to {\cal P}(A)$ is a functor; that is, if $B''\subseteq B'$ then $f^*(B'')\subseteq f^*(B')$.

Proposition 5.3   The function $\exists_f:{\cal P}(A) \to {\cal P}(B)$ is a functor; that is, if $A''\subseteq A'$ then $\exists_f(A'')\subseteq \exists_f(A')$.

Proposition 5.4   The function $\forall_f:{\cal P}(A) \to {\cal P}(B)$ is a functor; that is, if $A''\subseteq A'$ then $\forall_f(A'')\subseteq \forall_f(A')$.

Proposition 5.5   If f is an epimorphism then so is f^*.

Proposition 5.6   If f is a monomorphism then so is f^*.

Proposition 5.7   If f is an epimorphism then so is $\exists_f$.

Proposition 5.8   If f is a monomorphism then so is $\forall_f$.

Proposition 5.9   For any f, f^* preserves intersection and union.

Proposition 5.10   For any f, $\exists_f$ preserves union, but need not preserve intersection.

Proposition 5.11   For any f, $\forall_f$ preserves intersection, but need not preserve union.

Proposition 5.12   For any $A'\subseteq A$ and $B'\subseteq B$, $f^*(B')\subseteq A'$ if and only if $B' \subseteq \forall_f(A')$.

Proposition 5.13   For any $A'\subseteq A$ and $B'\subseteq B$, $A' \subseteq f^*(B')$ if and only if $\exists_f(A') \subseteq B'$.