Questions on: $G$ a generic ultrafilter on $B$ if and only if $G$ is a generic filter on $(B+,<)$? Here are the definitions, and then I shall explain which parts of the implication I understand, and which parts I don't, which are the questions.  The definitions are from Jech, as well as the question which is exercise 14.10.
Definitions:
A.  $G$ is a generic ultrafilter on $B$ (complete Boolean algebra in ground model $M$) if and only if


*

*$0 \notin G$, $1 \in G$,

*if $a,b \in G$ then $a*b \in G$,

*if $a < b$ and $a \in G$ then $b \in G$,

*$\Pi X \in G$ whenever $X \in M$ and $X \subset G$, and

*$\forall a \in B$, $a \in G$ or $\neg a \in G$.


B. $G$ is a generic filter on $(B^+,<)$ ($B^+$ is $B/\{0\}$, and $u\le v \iff u*v = u \iff u + v = v \iff u-v = 0$) if and only if


*

*$G$ is nonempty,

*if $p,q \in G$, then $\exists r \in G$; $r \le p$ and $r \le q$,

*if $p \le q$ and $p \in G$ then $q \in G$, and

*if $D \subset B^+$ is dense and $D \in M$, then $D \cap G \neq \emptyset$.


Proof and Questions:
$B \rightarrow A$


*

*Since $G \subset B^+$, $0 \notin G$ since $G$ is nonempty; also and therefore since $G$ is upwards closed, $1 \in G$.

*Let $a,b \in G$, then there is an $r \in G$ such that $r \le a$ and $r \le b$, but then $r \le a*b$ implies $a*b \in G$ since $G$ is upwards closed.

*same-same

*is it a density argument?

*proof by contradiction?


$A \rightarrow B$


*

*$G$ is nonempty since $1 \in G$.

*If $a,b \in G$, then $a*b \in G$, and $a*b \le a$ and $a*b \le b$.

*same-same

*Let $D$ be dense in $B^+$, how do I show $G \cap D \ne \emptyset$?


To summarize, I'd like to know, but have not yet been able to prove, why a generic filter on $(B^+,<)$ is closed under boolean products, and why it is an ultrafilter on $B$.  And, why a generic ultrafilter on a complete Boolean algebra $B$ meets the dense sets in the ground model.
 A: First, the closure under products. Let $G$ be generic on the poset $B^+$ and take $X\subseteq G,X\in M$. Let 
$$D=\{u\in B^+;\forall x\in X\colon u\leq x\}\cup\{u\in B^+;\exists x\in X\colon u\leq\lnot x\}$$
$D$ is dense; to see this, take $v\in B^+$. Now, either $v\leq x$ for all $x\in X$ or $v\cdot \lnot x\neq 0$ for some $x\in X$. In the former case we get $v\in D$ and in the latter we get $v\cdot\lnot x\in D$ with $v\cdot\neg x\leq v$. Now, because of genericity we find $u\in G\cap D$. But $u$ cannot come from the second piece of $D$, since it must be compatible with all elements of $X$. Therefore $u\leq x$ for all $x\in X$ and upward closure gives $\prod X\in G$. 
Next, the maximality condition. Take $a\in B$ and let $D=\{u\in B^+; u\leq a\}\cup\{u\in B^+;u\leq\lnot a\}$. The same argument as before shows that $D$ is dense, so either $a\in G$ or $\lnot a\in G$.
Finally, let's see that a generic ultrafilter $G\subseteq B$ meets all dense sets in the ground model. Let $D$ be dense and assume $G\cap D=\emptyset$. Since $G$ is an ultrafilter, we must have $\{\lnot u;u\in D\}\subseteq G$ and, because of genericity,
$\prod_{u\in D}\lnot u\in G$. If this product equals 0, we have found our contradiction. But even if $\prod_{u\in D}\lnot u>0$ we get into trouble. Since $D$ is dense, we find a
$v\in D$ such that $0<v<\prod_{u\in D}\lnot u$, which is clearly absurd. All of this shows that $G\cap D$ is nonempty.
As a side note, it is very common to construct dense sets in the way shown: one piece contains the elements you want to capture and the other one makes the whole thing dense. A very similar argument shows that, if you have a condition in $G$ forcing a statement, you can assume that 1 already forces it.
Also, it's interesting to notice what the closure of the ultrafilter under arbitrary products means. The generic ultrafilter is used to pick out which Boolean values translate to "true" when reducing the Boolean-valued logic to the usual two-valued logic. Closure under finite products and the maximality condition all correspond to the standard rules of logic: conjunctions of true statements are true and each statement is either true or false. This basically shows that when reducing by (nongeneric) ultrafilters, propositional logic is preserved. Closure under arbitrary products can now be seen as validating universal quantification (over sets in the ground model): if all instances of a statement over a set are true, then universally quantifying over that set will also give a true statement. Adding this condition means that we are preserving first-order logic. It's peculiar that ultrafilters interpreting propositional logic are such mundane things, while moving to first-order logic gives these fantastic generic ultrafilters which may or may not exist.
