View source for Exists functor

{{Stub page|Requires fleshing out}}
__TOC__
==Definition==
The ''{{M|\exists}}-functor'' is a [[covariant functor]] taking [[SET (category)|{{M|\mathrm{SET} }}]] {{M|\leadsto}} {{M|\mathrm{SET} }} defined as follows{{rAITCTHS2010}}:
* {{M|1=\forall A\in\text{Ob}(\mathrm{SET})[\exists:A\mapsto\mathcal{P}(A)]}}, recall {{M|\mathcal{P}(X)}} denotes the [[power set]] of {{M|X}}
** The functor sends all objects to their powerset. and
* {{M|1=\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 {{M|\exists}}-functor takes the function {{M|f}} to a function that takes each element of the powerset of the domain of {{M|f}} to the image of that element under {{M|f}} (which is obviously in the powerset of the co-domain of {{M|f}})
===Proof of claim===
{{Begin Inline Theorem}}
'''Claim: ''' that the {{M|\exists}}-functor is a functor
{{Begin Inline Proof}}
{{Requires proof|See page 82 in<ref name="AITCTHS2010"/>}}
{{End Proof}}{{End Theorem}}
==Properties==
Notice that the {{M|\exists}}-functor has the following property:
* Given a {{M|(f:A\rightarrow B)\in\text{Mor}(\mathrm{SET})}}
* {{M|1=\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 {{M|b}} is in the image of {{M|X}} under the image of {{M|f}} in the functor ''if and only if'' there is an {{M|a\in X}} such that {{M|1=f(a)=b}}}}
==See also==
* [[Forall functor|{{M|\forall}}-functor]] - defined along the same vein as the {{M|\exists}}-functor
{{Todo|A forall-exists-inverse functor page comparison}}
==References==
<references/>



{{Category theory navbox}}
{{Definition|Category Theory}}
{{Theorem Of|Category Theory}}
[[Category:Functors]]