Difference between revisions of "Exists functor"

Revision as of 16:36, 20 February 2016

Definition

The $\exists$-functor is a covariant functor taking $\mathrm{SET}$ $\leadsto$ $\mathrm{SET}$ defined as follows^[1]:

• $\forall A\in\text{Ob}(\mathrm{SET})[\exists:A\mapsto\mathcal{P}(A)]$, recall $\mathcal{P}(X)$ denotes the power set of $X$
  • The functor sends all objects to their powerset. and
• $\forall (f:A\rightarrow B)\in\text{Mor}(\mathrm{SET})\left[\exists(f)\mapsto\left\{\begin{array}{l}:\mathcal{P}(A)\rightarrow\mathcal{P}(B)\\:X\mapsto f(X)\end{array}\right.\right]$
  • That is to say the $\exists$-functor takes the function $f$ to a function that takes each element of the powerset of the domain of $f$ to the image of that element under $f$ (which is obviously in the powerset of the co-domain of $f$)

Proof of claim

Properties

Notice that the $\exists$-functor has the following property:

• Given a $(f:A\rightarrow B)\in\text{Mor}(\mathrm{SET})$
• $\forall X\in\mathcal{P}(A)\ \forall b\in B\Big[ [b\in(\exists(f))(X)]\iff[\exists a\in A(b=f(a)\wedge a\in X)]\Big]$

TODO: Describe this, something like $b$ is in the image of $X$ under the image of $f$ in the functor if and only if there is an $a\in X$ such that $f(a)=b$

See also

• $\forall$-functor - defined along the same vein as the $\exists$-functor

TODO: A forall-exists-inverse functor page comparison

References

1. ↑ ^{Jump up to: 1.0 1.1} An Introduction to Category Theory - Harold Simmons - 1st September 2010 edition