Return to Answer

The key here is that you don't have to force beyond $\mathrm{Add}(\kappa,\kappa^+)$ in order to lift the embedding.

Suppose $G \subseteq \mathbb P$ is generic and $H \subseteq \mathrm{Add}(\kappa,\kappa^+)$ is generic over $V[G]$. Since we have GCH, $j(\kappa) < \kappa^{++}$. We also have $M^\kappa \subseteq M$, and this is preserved by the forcing so that $M[G*H]^\kappa \subseteq M[G*H]$ in $V[G*H]$.

Now the tail of the iteration, $j(\mathbb P)/(G*H)$ is $\kappa^+$-closed but of size $\kappa^+$ from the perspective of $V[G*H]$. Thus we may build a filter $F$ for this that is generic over $M[G*H]$, and lift the embedding to $j : V[G] \to M[G']$ (where $G' = G*H*F$).

So by forcing with $\mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, we get an elementary embedding lifting the ultrapower embedding. Applying Foreman's Duality Theorem (proof given as 2.12 here), with $I$ being the dual of $\mathscr U$ in that notation, there is in $V[G]$ a normal ideal $J$ on $\kappa$ such that $P(\kappa)/J$ is isomorphic to what I called $(j(\mathbb P)/\dot K)/G$ there. What is $\dot K$? In this case, it is the dual ideal (in the Boolean completion) to the filter of elements forced to be in $G*H*F$, and $j(\mathbb P)/\dot K \sim \mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, and $(j(\mathbb P)/\dot K)/G \sim\dot{\mathrm{Add}}(\kappa,\kappa^+)$.

The key here is that you don't have to force beyond $\mathrm{Add}(\kappa,\kappa^+)$ in order to lift the embedding.

Suppose $G \subseteq \mathbb P$ is generic and $H \subseteq \mathrm{Add}(\kappa,\kappa^+)$ is generic over $V[G]$. Since we have GCH, $j(\kappa) < \kappa^{++}$. We also have $M^\kappa \subseteq M$, and this is preserved by the forcing so that $M[G*H]^\kappa \subseteq M[G*H]$ in $V[G*H]$.

Now the tail of the iteration, $j(\mathbb P)/(G*H)$ is $\kappa^+$-closed and of size $j(\kappa)$ and with the $j(\kappa)$-c.c., but from the perspective of $V[G*H]$, it has only $\kappa^+$-many maximal antichains. Thus we may inductively build a filter $F$ for this that is generic over $M[G*H]$, and lift the embedding to $j : V[G] \to M[G']$ (where $G' = G*H*F$).

So by forcing with $\mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, we get an elementary embedding lifting the ultrapower embedding. Applying Foreman's Duality Theorem (proof given as 2.12 here), with $I$ being the dual of $\mathscr U$ in that notation, there is in $V[G]$ a normal ideal $J$ on $\kappa$ such that $P(\kappa)/J$ is isomorphic to what I called $(j(\mathbb P)/\dot K)/G$ there. What is $\dot K$? In this case, it is the dual ideal (in the Boolean completion) to the filter of elements forced to be in $G*H*F$, and $j(\mathbb P)/\dot K \sim \mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, and $(j(\mathbb P)/\dot K)/G \sim\dot{\mathrm{Add}}(\kappa,\kappa^+)$.

The key here is that you don't have to force beyond $\mathrm{Add}(\kappa,\kappa^+)$ in order to lift the embedding.

Suppose $G \subseteq \mathbb P$ is generic and $H \subseteq \mathrm{Add}(\kappa,\kappa^+)$ is generic over $V[G]$. Since we have GCH, $j(\kappa) < \kappa^{++}$. We also have $M^\kappa \subseteq M$, and this is preserved by the forcing so that $M[G*H]^\kappa \subseteq M[G*H]$ in $V[G*H]$.

Now the tail of the iteration, $j(\mathbb P)/(G*H)$ is $\kappa^+$-closed but of size $\kappa^+$ from the perspective of $V[G*H]$. Thus we may build a filter $F$ for this that is generic over $M[G*H]$, and lift the embedding to $j : V[G] \to M[G']$.

So by forcing with $\mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, we get an elementary embedding lifting the ultrapower embedding. Applying Foreman's Duality Theorem (proof given as 2.12 here), with $I$ being the dual of $\mathscr U$ in that notation, there is in $V[G]$ a normal ideal $J$ on $\kappa$ such that $P(\kappa)/J$ is isomorphic to what I called $j(\mathbb P)/\dot K$ there. What is $\dot K$? In this case, it is the dual ideal (in the Boolean completion) to the filter of elements forced to be in $G*H*F$, and $j(\mathbb P)/\dot K \sim \mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$.

The key here is that you don't have to force beyond $\mathrm{Add}(\kappa,\kappa^+)$ in order to lift the embedding.

Suppose $G \subseteq \mathbb P$ is generic and $H \subseteq \mathrm{Add}(\kappa,\kappa^+)$ is generic over $V[G]$. Since we have GCH, $j(\kappa) < \kappa^{++}$. We also have $M^\kappa \subseteq M$, and this is preserved by the forcing so that $M[G*H]^\kappa \subseteq M[G*H]$ in $V[G*H]$.

Now the tail of the iteration, $j(\mathbb P)/(G*H)$ is $\kappa^+$-closed but of size $\kappa^+$ from the perspective of $V[G*H]$. Thus we may build a filter $F$ for this that is generic over $M[G*H]$, and lift the embedding to $j : V[G] \to M[G']$ (where $G' = G*H*F$).

So by forcing with $\mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, we get an elementary embedding lifting the ultrapower embedding. Applying Foreman's Duality Theorem (proof given as 2.12 here), with $I$ being the dual of $\mathscr U$ in that notation, there is in $V[G]$ a normal ideal $J$ on $\kappa$ such that $P(\kappa)/J$ is isomorphic to what I called $(j(\mathbb P)/\dot K)/G$ there. What is $\dot K$? In this case, it is the dual ideal (in the Boolean completion) to the filter of elements forced to be in $G*H*F$, and $j(\mathbb P)/\dot K \sim \mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, and $(j(\mathbb P)/\dot K)/G \sim\dot{\mathrm{Add}}(\kappa,\kappa^+)$.

The key here is that you don't have to force beyond $\mathrm{Add}(\kappa,\kappa^+)$ in order to lift the embedding.

Suppose $G \subseteq \mathbb P$ is generic and $H \subseteq \mathrm{Add}(\kappa,\kappa^+)$ is generic over $V[G]$. Since we have GCH, $j(\kappa) < \kappa^{++}$. We also have $M^\kappa \subseteq M$, and this is preserved by the forcing so that $M[G*H]^\kappa \subseteq M[G*H]$ in $V[G*H]$.

Now the tail of the iteration, $j(\mathbb P)/(G*H)$ is $\kappa^+$-closed but of size $\kappa^+$ from the perspective of $V[G*H]$. Thus we may build a filter $F$ for this that is generic over $M[G*H]$, and lift the embedding to $j : V[G] \to M[G']$.

So by forcing with $\mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, we get an elementary embedding lifting the ultrapower embedding. Applying Foreman's Duality Theorem (proof given as 2.12 here), with $I$ being the dual of $\mathscr U$ in that notation, there is in $V[G]$ a normal ideal $J$ on $\kappa$ such that $P(\kappa)/J$ is isomorphic to what I called $j(\mathbb P)/\dot K$ there. What is $\dot K$? In this case, it is built using the name for $F$, so it is engineered to give $j(\mathbb P)/\dot K \sim \mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$.

The key here is that you don't have to force beyond $\mathrm{Add}(\kappa,\kappa^+)$ in order to lift the embedding.

Suppose $G \subseteq \mathbb P$ is generic and $H \subseteq \mathrm{Add}(\kappa,\kappa^+)$ is generic over $V[G]$. Since we have GCH, $j(\kappa) < \kappa^{++}$. We also have $M^\kappa \subseteq M$, and this is preserved by the forcing so that $M[G*H]^\kappa \subseteq M[G*H]$ in $V[G*H]$.

Now the tail of the iteration, $j(\mathbb P)/(G*H)$ is $\kappa^+$-closed but of size $\kappa^+$ from the perspective of $V[G*H]$. Thus we may build a filter $F$ for this that is generic over $M[G*H]$, and lift the embedding to $j : V[G] \to M[G']$.

So by forcing with $\mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$, we get an elementary embedding lifting the ultrapower embedding. Applying Foreman's Duality Theorem (proof given as 2.12 here), with $I$ being the dual of $\mathscr U$ in that notation, there is in $V[G]$ a normal ideal $J$ on $\kappa$ such that $P(\kappa)/J$ is isomorphic to what I called $j(\mathbb P)/\dot K$ there. What is $\dot K$? In this case, it is the dual ideal (in the Boolean completion) to the filter of elements forced to be in $G*H*F$, and $j(\mathbb P)/\dot K \sim \mathbb P * \dot{\mathrm{Add}}(\kappa,\kappa^+)$.