Atom for a notion of forcing and order theory atom. I was reading a bit about forcing. I just saw a definition of an atom in this context that is :
Let $\mathbb{P}$ be a notion of forcing. An element $p \in \mathbb{P}$ is called an atom of P if and only if $¬∃q,r∈P(q≤p∧r≤p∧q⊥r)$. I was wondering how this relates to the notion of atom that I found on wikipedia.
 A: Consider a forcing $\mathbb P$ and define a relation on $\mathbb P$ by $p\sim q$ iff $p$ and $q$ are compatible with the same conditions, i.e. $\forall r\in\mathbb P (r\|p\Leftrightarrow r\|q)$. For all purposes of forcing, $p$ and $q$ are essentially identical if $p\sim q$. The reason is that any $\mathbb P$-generic filter $G$ contains $p$ if and only if it contains $q$:
Assume $p\in G$. If $r\leq p$ then $r$ is compatible with $q$, so that $D=\{s\in\mathbb P\mid s\leq q\}$ is dense below $p$. As $p\in G$, $G\cap D\neq\emptyset$, so that $G$ contains an element below $q$ and thus $q\in G$ as well. The other direction works similarly
Note that $\sim$ is an equivalence relation so that we can build the forcing $\mathbb Q=\mathbb P/\sim$, ordered by $[p]\leq [q]$ iff any $r$ that is compatible with $p$ is also compatible with $q$. It is easy to check that this yields a welldefined p.o.. With the argument from before it is not difficult to see that $\mathbb P$ and $\mathbb Q$ are forcing equivalent, i.e. they induce the same generic extensions. [If $G$ is $\mathbb P$-generic and $\pi:\mathbb P\rightarrow\mathbb Q$ is the projection then $H=\pi[G]$ is $\mathbb Q$-generic with $V[G]=V[H]$ and if $H$ is $\mathbb Q$-generic then $G=\pi^{-1}[H]$ is $\mathbb P$-generic with $V[G]=V[H]$.]
Now $p$ is an atom in $\mathbb P$ in the forcing sense iff $[p]$ is a minimal element of $\mathbb Q$. That already looks more like the definition from order theory, except that we have no least element $0$ here. You can now add a least element to $\mathbb Q$ artifically if you like (but this will result in a trivial forcing). A more natural way to bridge the gap is to embed $\mathbb Q$ into its boolean completion (which exists as $\mathbb Q$ is automatically seperative), call the map $\mu:\mathbb Q\rightarrow\mathcal B(\mathbb Q)$. Then $\mu$ is a dense embedding from $\mathbb Q$ into $\mathcal B(\mathbb Q)^\times=\mathcal B(\mathbb Q)\setminus \{0\}$ so that $\mathbb P$, $\mathbb Q$ and $\mathcal B(\mathbb Q)^\times$ are all mutually forcing equivalent.
Now $p$ is an atom in $\mathbb P$ in the forcing sense iff $\mu([p])$ is an atom in $\mathcal B(\mathbb Q)$ in the order theory sense. The map $p\mapsto \mu([p])$ is even a dense embedding from $\mathbb P$ into $\mathcal B(\mathbb Q)^\times$.
