= A forcing atom determines a ground-model generic filter
{title2=$G_p=\{q\in\mathbb P:q\text{ is compatible with }p\}$}
For a <forcing atom> $p$ in a ground-model <forcing> order, $G_p$ is a ground-model <generic filter>. It contains $p$ and is upward closed. For $q,r\in G_p$, choose $q'\leq p,q$ and $r'\leq p,r$. The atom property gives $s\leq q',r'$, so $s\in G_p$ is a common strengthening of $q,r$. Thus $G_p$ is a <filter in an ordered set>. Every <dense subset of a forcing order> has some $d\leq p$, and $d\in G_p$. The defining compatibility predicate is bounded to the ground-model <set> of conditions, so <axiom schema of separation> forms $G_p$ inside the ground model. For a nonminimal atom, this filter can strictly contain the <principal filter> above $p$.
Back to article page
