$\exists$-functor

(Unknown grade)

This page is a stub

This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:

Requires fleshing out

Definition

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

• $\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

[Expand]

Claim: that the $\exists$-functor is a functor

---

(Unknown grade)

This page requires one or more proofs to be filled in, it is on a to-do list for being expanded with them.

Please note that this does not mean the content is unreliable. Unless there are any caveats mentioned below the statement comes from a reliable source. As always, Warnings and limitations will be clearly shown and possibly highlighted if very important (see template:Caution et al).
The message provided is:

See page 82 in

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

---