I'm looking for a reference (if there is one) for a representation theorem for iterated generic embeddings. What I mean by representation is a generalization of the following:

If $U$ is an ultrafilter on $\kappa$, and we iterate the ultrapower construction to obtain a sequence of embeddings $\langle Ult^{(\alpha)}(V,U),i_{\alpha,\beta} \mid \alpha<\beta<\lambda\rangle$ (for some $\lambda$), then we can define ultrafilters $U_\alpha$ on a subset of $\kappa^\alpha$ (those sequences with finite support) such that $Ult^{(\alpha)}(V,U)\cong Ult(V,U_\alpha)$.

(see e.g. Jech's Third Millennium edition chapter 19).

So I'd like to have a similar representation for iterating generic embeddings (not necessarily using the same forcing at each successor step). This has two ingredients:

- Generalize the above to iterations where different objects (ultrafilters/extenders) are used to define the embedding in each successor step. Specifically - where the object is not in the image of the previous embedding.
- Incorporate the forcing mechanism.

Edit: This is the setting I want:

$\langle M_\alpha, i_{\alpha,\beta} \rangle$ is a sequence of models with elementary embeddings $i_{\alpha,\beta}:M_\alpha \to M_\beta$, each $M_\alpha$ defined in a generic extension $N_\alpha$ such that:

- $N_0=M_0$
- In successor step: pick a precipitous ideal/tower in $M_\alpha$ and an $N_\alpha$-generc for it. Then $N_{\alpha+1}$ is tye generic extension of $N_\alpha$, and $i_{\alpha,\alpha+1}:M_\alpha \to M_{\alpha+1}$ is the induced embedding.
- In limit step take the direct limit of the embeddings, and (I hope this works) the finite support iteration of the extensions.

On the face of it it seems feasable, just much more elaborated. Has something like this been done?

[I skimmed the Handbook chapters of Cummings and Foreman, but haven't seen something like this]

functionswhich were not in the original model. And still I'm not sure I can put everything into a tower, although it might be the case in some examples (perhams using strong enough large cardinal assumptions?). $\endgroup$ – Ur Ya'ar Jul 4 at 13:39