Reference request: $\kappa^+$-saturated ideal from iterated Cohen forcing on measurable $\kappa$

Question

In Kunen [1] the author makes the following note: Let $\kappa$ be measurable with normal measure $\mathscr{U}$ in a model of $\mathsf{GCH}$. Let $\mathbb{P}$ be an iteration of $\operatorname{Add}(\alpha,\alpha^+)$ for all inaccessible $\alpha<\kappa$. Then in a forcing extension by $\mathbb{P}$ there will be a $\kappa^+$-saturated ideal $\mathcal{I}$ on $\kappa$ such that $\mathscr{P}(\kappa)/\mathcal{I}\cong\mathscr{B}(\operatorname{Add}(\kappa,\kappa^+))$.

Question: Where can I find more details on this?

Previously in the paper the author made use of the following result: If $j\colon V\to M$ is an ultrapower embedding from the ultrafilter $\mathscr{U}$ on $\kappa$ and $\pi\colon j(\mathbb{P})\cong\mathbb{P}\ast\dot{\mathbb{Q}}$ is an isomorphism such that $\pi(j(p))=(p,1)$ then, after forcing with $\mathbb{P}$, $\mathscr{P}(\kappa)/\mathcal{I}\cong\mathbb{Q}$, where $\mathcal{I}$ is the ideal generated by $\mathscr{U}$ in the extension.

However, in the case that the author has demonstrated, this only gets me as far as $\mathscr{P}(\kappa)/\mathcal{I}\cong\operatorname{Add}(\kappa,\kappa^+)\ast\operatorname{Add}(\kappa^+,\kappa^+)$, and I cannot seem to find a new $X$ and $\mathcal{J}$ such that $\mathscr{P}(X)/\mathcal{J}\cong\operatorname{Add}(\kappa,\kappa^+)$ in the extension. (The only natural candidates that I can see are $X=\kappa$ and $\mathcal{J}\supseteq\mathcal{I}$ for some well-chosen $\mathcal{J}$, but those that I have tried either fail to be ideals or fail the isomorphism).

[1] Kenneth Kunen, Maximal $\sigma$-independent families., Fund. Math. 117 (1983), no. 1, 75-80.

Answer 1

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^+)$.