Non-stationary support iterations of Prikry forcings and restrictions of ultrapower embeddings to the ground model (Q2084953)

One of the cornerstones of inner model theory is that under suitable anti-large cardinal hypothesis, every elementary embedding \(j \colon V \to M\) such that \(M\) is closed enough, restricts into an iteration (tree) of extenders in the core model, see [\textit{R. Schindler}, J. Symb. Log. 71, No. 1, 241--251 (2006; Zbl 1109.03063)]. Intuitively, we expect this result to remain true over inner models that contains large cardinals much above the limitations of the inner model program, such as models of strongly compact cardinals. As we do not have core models for those large cardinal axioms, we can replace the question by inquiring whether the restrictions of elementary embeddings in a generic extension to the ground model must be an iteration of extenders in the ground model, and whether it is definable. This question was first studied in by \textit{J. D. Hamkins}, in the case where the forcing notion contains a \(\delta\)-\textit{gap} for \(\delta\) below the critical point [Isr. J. Math. 125, 237--252 (2001; Zbl 1010.03042)]. The main result of this paper is that one can obtain a core-model type characterization of elementary embeddings in a generic extension by an iteration of Prikry forcings, using only the properties of the forcing, without any anti-large cardinal hypothesis. As Prikry forcings are never \(\sigma\)-distributive, this forcing does not admit any gap. This paper addresses the problem of classifying the normal measures and their corresponding elementary embedding in the generic extension by the non-stationary support iteration of the standard Prikry forcing. The main result of the paper is a complete description of the restriction to the ground model of any ultrapower embedding by a normal measure in the generic extension. This iteration is going to use only normal measures. During this iteration, Prikry sequences for cardinals above the critical points are going to be constructed in a way that resembles the Bokovský-Dehornoy theorem, [\textit{L. Bukovsky}, Commentat. Math. Univ. Carol. 18, 77--85 (1977; Zbl 0358.02069); \textit{P. Dehornoy}, Ann. Math. Logic 15, 109--160 (1978; Zbl 0417.03025)]. At each step of the iteration, the next critical point is going to be the next element in some Prikry sequence.