The Covering Lemma for L[U]

Question

Hi,

The covering lemma for L[U] (minimal k-model) is stated in Mitchel's handbook chapter:

"Assuming zero-dagger does not exist then covering holds for L[U] or there is a sequence C ⊆ κ, which is Prikry generic over L[U], such that for all sets x of ordinals there is a set y ∈ L[U,C] such that y ⊇ x and |y| = |x| + ℵ1."

And so a Prikry sequence is the only counter example to covering. Kanamori (19.18) proves a theorem of Solovay saying that the critical points of an iteration define a Prikry sequence. So in the core model L[U] (under zero-dagger) we must have prikry sequences.

What are the main differences between the proof of the (more familiar) covering lemma for L and the theorem above for L[U]? I assume that since the mice of L[U] are not simple $L_\alpha$'s we get indiscernibles when trying to cover a set X in a collapsed model. But is the proof the same as before "modulu" Prikry sequences, or is it more complicated than that and more cases should be handled regarding these sequences?

Answer 1

I don't know enough about these proofs to really answer the questions, but the following seems relevant to Question b. One of the key facts about constructibility is that, if you have two transitive models of an appropriate finite part of ZFC plus V=L, then one of these is an initial segment of the other (because both are of the form $L_\alpha$). The corresponding fact for transitive models of $(\exists U)\ V=L[U]$ (where the notation $U$ means a normal ultrafilter on a measurable cardinal) is that, given any two such models, you can form iterated ultrapowers of both to arrange that the measurable cardinal is the same in both, and then one of the two iterated ultrapowers will be an initial segment of the other. The need to take iterated ultrapowers in such comparison arguments is a major difference between working with L and working with inner models and core models for large cardinals. The larger the cardinals, the more complicated the iterations get, including non-linearly ordered "tree iterations" once you get to Woodin cardinals. (I urge the people here who really know this part of set theory to do whatever editing is needed to make what I wrote here true.)