Let $B_{0}\supseteq B_{1}\supseteq\dots\supseteq B_{\alpha}\supseteq\dots\,\,\left(\alpha<\kappa\right)$ be a descending sequence of complete Boolean algebras, $B_{\kappa}:=\bigcap_{\alpha<\kappa}B_{\alpha}$, $G_0$ a $V$-generic filter on $B_0$ and for every $\alpha\leq\kappa$, $G_{\alpha}:=G\cap B_{\alpha}$. I want to understand the intersection $\bigcap_{\alpha<\kappa}V\left[G_{\alpha}\right]$, which clearly contains $V[G_{\kappa}]$.

In *Iterating ordinal definability*, Zadrożny surveys without proof some results. First are general results:

- (Grigorief) $\bigcap_{\alpha<\kappa}V\left[G_{\alpha}\right]\vDash ZF$
- (Jech) If $B_0$ is $\kappa$-distributive, then $\bigcap_{\alpha<\kappa}V\left[G_{\alpha}\right]=V[G_\kappa]$ (so in particular satisfies $ZFC$)

[The latter appears as lemma 26.6 in the 1978 edition of Jech's Set Theory, but curiously I haven't found it in the 3rd Millennium edition].

Then he gives a more concrete characterization of $V\left[G_{\kappa}\right]$, attributed to Sakarovitch:

For $p,q\in B_0^+$, let $p\sim q$ iff $\exists \alpha<\kappa$ such that $$ \inf\{d\in B_\alpha \mid d\geq p\}=\inf\{d\in B_\alpha \mid d\geq q\}$$Then the separative part of $B_0/{\sim}$ is isomorphic to $B_\kappa^+$. In particular, from $G_0$ one can define a $B_0/{\sim}$ generic $G_0/{\sim}$, and if $B_0$ is $\kappa$-distributive then $$\bigcap_{\alpha<\kappa}V\left[G_{\alpha}\right]=V[G_\kappa]=V[G_0/{\sim}]$$

I want to understand this result more, however Zadrożny references Sakarovitch's PhD thesis, which is in French, not available online and as far as I can tell, has no adaptation to a paper. So my questions are:

- Is there some other source where this result is presented?
- Can someone provide a proof or at least a sketch?
- What more can be said on this intersection, given the properties of the descending sequence?

A particular case I'm interested in, is when the sequence is given by "tails" of an iteration (or even product): assume $\langle P_\alpha \mid\alpha\leq\kappa\rangle$ is an iteration, and set for every $\alpha$ $P_\kappa=P_\alpha * \dot{P}^\alpha$ (so $\dot{P}^\alpha$ is the "tail" of the iteration), and "$B_\alpha=ro(\dot{P}^\alpha)$" (I guess that for this to make perfect sense we should say something like $B_\alpha=ro(P_\kappa)/ro(P_\alpha)$). Can something more concrete be said in this case?

Edit: note that if $P_\kappa$ is a direct limit (and $\kappa$-distributive), we'd get that all elements are eventually equivalent so $B_0/{\sim}$ is trivial. So on one hand this shows that the intersection is $V$. And on the other hand, the question is interesting only when non-direct limit is taken.

2more comments