proof that forcing notions are equivalent to their composition
This is a long and complicated proof, the more so because the meaning of shifts depending on what generic subset of is being used. It is therefore broken into a number of steps. The core of the proof is to prove that, given any generic subset of and a generic subset of there is a corresponding generic subset of such that , and conversely, given any generic subset of we can find some generic of and a generic of such that .
We do this by constructing functions using operations which can be performed within the forced universes so that, for example, since has both and , can be calculated, proving that it contains . To ensure equality, we will also have to ensure that our operations are inverses; that is, given , and given and , and .
The remainder of the proof merely defines the precise operations, proves that they give generic sets, and proves that they are inverses.
Before beginning, we prove a lemma which comes up several times:
Lemma: If is generic in and is dense above some then
Let . This is dense, since if then either is incompatible with , in which case , or there is some such that , and therefore there is some such that , and therefore . So intersects . But since a generic set is directed, no two elements are incompatible, so must contain an element of which is not incompatible with , so it must contain an element of .
is a generic filter
First, given generic subsets and of and , we can define:
is closed
Let and let . Then we can conclude , , , and , so (since is closed) and since and forces both and that is downward closed. So .
is directed
Suppose . So , and since is directed, there is some . Since and is directed, there is some . Therefore there is some , , such that , so and .
is generic
Suppose is a dense subset of . We can project it into a dense subset of using :
Lemma: is dense in
Given any , take any . Then we can define yet another dense subset, this one in :
Lemma: is dense above in
Take any such that . Then, since is dense in , we have some such that . Then by definition and .
From this lemma, we can conclude that there is some such that , and therefore some such that where . So is indeed dense in .
Since is dense in , there is some such that , and so some such that . But since and , , so is indeed generic.
is a generic filter
Given some generic subset of , let:
is closed
Take any and any such that . Then there is some satisfying the definition of , and also , so .
is directed
Consider . Then there is some and some such that and some and some such that . Since is directed, there is some such that , and therefore , .
is generic
Let be a dense subset of . Then . Clearly this is dense, since if then there is some such that , so and . So there is some , and therefore . So is generic.
is a generic filter
Given a generic subset , define:
(Notice that is dependant on , and is a subset of , that is, the forcing notion inside , as opposed to the set of names which weβve been primarily working with.)
is closed
Suppose and . Then there is some such that . Since , there is some such that for some , . By the definition of , there is some such that , and since is directed, there is some and . Since is closed and , we have .
is directed
Suppose . Then for some , , and since is directed, there is some such that . Then and since and , we have .
is generic
Let be a dense subset of (in ). Let be a -name for , and let be a such that is dense. By the definition of , there is some such that for some . Then .
Lemma: is dense (in ) above
Take any such that . Then is dense, and therefore there is some such that and . So and .
Take any . Then , so , and by the definition of , .
If is a generic subset of , observe that:
If then obviously this holds, so . Conversely, if then there exist and such that , and since is directed, some such that . But then and , and since is closed, .
Assume that is generic in and is generic in .
Suppose . Then there is some and some such that and . By the definition of , , and then since is closed .
Conversely, suppose . Then (since is non-trivial), for some , and therefore .
Assume that is generic in and is generic in .
Given any , there is some such that , and so there is some such that , and therefore .
On the other hand, if then there is some , and therefore some .
Title | proof that forcing notions are equivalent to their composition |
---|---|
Canonical name | ProofThatForcingNotionsAreEquivalentToTheirComposition |
Date of creation | 2013-03-22 12:54:26 |
Last modified on | 2013-03-22 12:54:26 |
Owner | Henry (455) |
Last modified by | Henry (455) |
Numerical id | 5 |
Author | Henry (455) |
Entry type | Proof |
Classification | msc 03E40 |
Classification | msc 03E35 |
Related topic | EquivalenceOfForcingNotions |