I am reading the proof of $L[U] \models \mathsf{GCH}$ given on Mitchell's Beginning Inner Model Theory at the handbook, but I confronted a detail how to fill the details.
Mitchell's proof goes as follows: let $\kappa$ be a measurable cardinal with a normal measure $U$. We only consider the case $\lambda<\kappa$, and we will show that $2^\lambda=\lambda^+$.
Let $x\subseteq \lambda$. Take $\tau$ such that $x\in L_\tau[U]\models \mathsf{ZFC^-}$. Take a Skolem hull $X\prec L_\tau[U]$ such that $\lambda\cup\{x\}\subseteq X$ and $|X|=\lambda$. If $M_x\cong X$ be the transitive collapse, then $M_x=L_{\alpha_x}[U_x]$ for some ordinal $\alpha_x$ and a normal filter $U_x$.
We claim that $\{z\subseteq \lambda\mid z<_{L[U]}x\}\subseteq M_x$. Consider the iterated ultrapower $\operatorname{Ult}_\kappa (M_x,U_x)$ and $i^{U_x}_\kappa: M_x\to \operatorname{Ult}_\kappa (M_x,U_x)$. Then
-
$\operatorname{Ult}_\kappa (M_x,U_x)=L_{\alpha_x'}[i^{U_x}_\kappa(U_x)]$ for some $\alpha_x'$, and
-
$i^{U_x}_\kappa(U_x)\subseteq U$, since $i^{U_x}_\kappa(U_x)$ is 'generated' by a club set $\{i_\nu^{U_x}(\kappa):\nu<\kappa\}$.
Since $i_\lambda^{U_x}$ is the identity over $\mathcal{P}^{M_x}(\lambda)$, we have $\{z\subseteq\lambda\mid z<_{L[U]}x\}\subseteq \mathcal{P}^{L_{\alpha_x'}[U_x]}(\lambda)\subseteq M_x$.
I see that why $i_\lambda^{U_x}$ is the identity over $\mathcal{P}^{M_x}(\lambda)$, but I have no idea that why the inclusions hold.
The second inclusion has some oddity since $\alpha_x'$ apparently bears no relation with $U_x$. I guess $U_x$ is a typo of $i_\kappa^{U_x}(U_x)$, but is it really a typo?
I also have no idea about how to show the first inclusion. The proof has not used $i^{U_x}_\kappa(U_x)\subseteq U$, so I guess it might be related. I would appreciate your help.
Best Answer
First, I believe you are right that $U_x$ is a typo and should be $i^{U_x}_\kappa(U_x)$ instead.
I don't know how the proof should go without some kind of comparison lemma. In particular, I am not sure if this is the sketch that the article has in mind. But here it goes: with the comparison lemma, we iterate $L[U]$ and $M_x$ far enough so that they become comparable as some $L[D]$ and $L_\xi[D]$ respectively.
So now let $z<_{L[U]}x$ where $x\in M_x$. The iterate $L_\xi[D]$ of $M_x$ has the same rank $\lambda+1$ stuff as $M_x$, so in particular $x\in V_{\lambda+1}\cap M_x = V_{\lambda+1}\cap L_\xi[D]$. Also, the embedding from $L[U]$ to $L[D]$ fixes all elements from $V_\kappa$ and since $\kappa>\lambda$, we have that $z<_{L[D]}x$ in $L[D]$ as well. But now it's straightforward that if $x\in L_\xi[D]$ and $z<_{L[D]}x$, then $z\in L_\xi[D]$, by general properties of the definable well-ordering of structures like $L[D]$.