Are there always measurables of high Mitchell rank below a supercompact?

Question

It is well-known that if $\kappa$ is supercompact, then it is a limit of measurable cardinals, and that $\kappa$ is also itself a measurable cardinal with Mitchell rank at least $\kappa^{++}$. Do we also know that this is second statement is true about measurables below the supercompact? That is to say, if $\kappa$ is supercompact, does it follow by a known/easy proof that there is some measurable $\lambda<\kappa$ with Mitchell rank $\lambda^{++}$?

I suspect that this is a standard result, but have been unable to find a source proving it.

Answer 1

The answer is yes. If you know that $\kappa$ has high Mitchell rank, then it follows that there must be many measurables below with high Mitchell rank, since this is a $\Sigma_2$-property, observable in any model with the same $V_{\kappa+2}$. So it reflects below.

Specifically, if $j:V\to M$ has critical point $\kappa$ and $M$ has all the measures on $\kappa$, then $M$ will observe that $\kappa$ has the Mitchell rank that it does. So it will be true in $M$ that there is a measurable cardinal as desired below $j(\kappa)$, and consequently by elementarity there will be many such measurable cardinals below $\kappa$ in $V$.