I want to use this post to construct club guessing sequences in the extension by vanilla Prikry forcing over a measurable. This was definitely known before-hand (as Todd pointed out to me), and I think this sort of thing has gotten around mostly by word of mouth. So I figured I may as well write it down since the argument is so short.
So let be measurable, and let be a witnessing normal measure on . Let , and for each fix an increasing and continuous with . In particular, puts in bijection with a club subset of , and so gets copied up to a normal measure over that club. Now let be Prikry forcing over with respect to , and let be the generic Prikry sequence.
In , let for each , and set . Recall that is -cc, and so every club subset of in the extension contains a ground model club (so in particular is stationary in ). Next note that for every , the set is a Prikry sequence for , and in particular will diagonalize all club subsets of in the ground model.
Claim: In , for any club , there is a club such that, for every , we have . Here is inclusion modulo bounded.
Proof: Let be club, and let be a ground model club contained in . Let be the set of accumulation points of . If , then is a club subset of which is in the ground model, and so .
Okay now (still working in the extension), let’s consider the cofinality map . We may as well assume that every point of is a regular cardinal. Since each was continuous, note that is just our original Prikry sequence. So, we’re in the rather bizarre situation where the points that guess clubs all concentrate on a cofinal, progressive -sequence of regular cardinals. On interesting thing to do is look at , as that would give us some insight as to how scales and club guessing sequences might interact. The following is a theorem of Jech:
Thm: Let be a non-trivial elementary embedding where came from. Then .
So here’s a question that’s probably much easier than I’m making it: Suppose I blow up before singularizing . Is there any way in which I can make sure that I can find with ? If so, that’ll mean that I can guess clubs in such a way that the image of the ladder system under the cofinality map does not carry a scale. That would be kind of interesting.