Am new to forcing (obviously...), and I got to read Definition 14.25 in Jech's Set Theory which defines the canonical ultrafilter $\dot{G}$ on the Boolean algebra $B$ which is:
$\dot{G}(\check{u})=u$ for every $u \in B$ and where $dom(\dot{G})=\{\check{u}: u \in B\}$
I understand that $\dot{G}$ is central in the boolean valued model approach to forcing since it somehow gives reason for the existence of a generic set. But I am a bit confused with the definition of $\dot{G}$ above and so I'd like to ask:
Is $\dot{G} \in V^B$ ?, where $V^B$ is the Boolean Valued model of Jech. If so, then how is it an ultrafilter on $B$?
How to prove that $\Vert \dot{G} \text{ is an ultrafilter on } B \Vert=1$
Am really grateful for any help.
Yes, $\dot G\in V^B$: it is defined as a function $V^B\to B,$ and that's what it means to be an element of $V^B.$
It is not an ultrafilter on $B,$ it is a name for one. The precise statement of this is just your second question: $\Vert \mbox{$\dot G$ is an ultrafilter on $\check B$ }\Vert =1.$
To show this, we need to check that all the properties of an ultrafilter are true in $V^B.$
For instance, $$ \Vert \dot G\subseteq \check B\Vert = \prod_{u\in B} u \Rightarrow 1 = 1,$$ $$ \Vert \check 1\in \dot G\Vert = \sum_{u\in B}\Vert \check u= \check 1\Vert \cdot u = 1$$ (since $\Vert \check u = \check 1\Vert = 1$ for $u=1$), and for $u,v\in B,$ $$ \Vert \check u\in \dot G\Vert \cdot \Vert \check v\in \dot G\Vert = \sum_{u',v' \in B}\Vert \check u'= \check u\Vert\cdot \Vert \check v'=\check v\Vert\cdot u\cdot v = u\cdot v = \dot G((u\cdot v)\check\;)=\Vert(u\cdot v)\check\;\in \dot G\Vert.$$
There are two other properties to check that I'll leave to you. Also, the one I did is a bit unfinished... why was it ok to assume the two elements were check names in $\check B$? (It has to do with the first thing I showed). More generally, how can we track it all the way back to $$ \Vert \forall x,y\in \dot G,\; x\cdot y\in \dot G\Vert=1$$ and what does $x\cdot y$ mean here exactly? ("$\cdot $" is not part of the forcing language).
I'm not sure I'd say $\dot G$ is central to the Boolean-valued model approach, but it is useful for linking it up with the "standard" approach.