Exists functor
From Maths
Revision as of 11:57, 20 February 2016 by Alec (Talk | contribs) (Created page with "{{Stub page|Requires fleshing out}} __TOC__ ==Definition== The ''{{M|\exists}}-functor'' is a covariant functor taking \mathrm{SET} }} {{M|\leadsto}...")
(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 [ilmath]\exists[/ilmath]-functor is a covariant functor taking [ilmath]\mathrm{SET} [/ilmath] [ilmath]\leadsto[/ilmath] [ilmath]\mathrm{SET} [/ilmath] defined as follows[1]:
- [ilmath]\forall A\in\text{Ob}(\mathrm{SET})[\exists:A\mapsto\mathcal{P}(A)][/ilmath], recall [ilmath]\mathcal{P}(X)[/ilmath] denotes the power set of [ilmath]X[/ilmath]
- The functor sends all objects to their powerset. and
- [ilmath]\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][/ilmath]
- That is to say the [ilmath]\exists[/ilmath]-functor takes the function [ilmath]f[/ilmath] to a function that takes each element of the powerset of the domain of [ilmath]f[/ilmath] to the image of that element under [ilmath]f[/ilmath] (which is obviously in the powerset of the co-domain of [ilmath]f[/ilmath])
Proof of claim
Claim: that the [ilmath]\exists[/ilmath]-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:
The message provided is:
See page 82 in[1]
Properties
Notice that the [ilmath]\exists[/ilmath]-functor has the following property:
- Given a [ilmath](f:A\rightarrow B)\in\text{Mor}(\mathrm{SET})[/ilmath]
- [ilmath]\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][/ilmath]
TODO: Describe this, something like [ilmath]b[/ilmath] is in the image of [ilmath]X[/ilmath] under the image of [ilmath]f[/ilmath] in the functor if and only if there is an [ilmath]a\in X[/ilmath] such that [ilmath]f(a)=b[/ilmath]
See also
- [ilmath]\forall[/ilmath]-functor - defined along the same vein as the [ilmath]\exists[/ilmath]-functor
TODO: A forall-exists-inverse functor page comparison
References
| ||||||||||||||||||||||||||||||||
