I have a few somehow related questions:
Question 1. What do we expect for an inner model $\mathcal{K}$ to be a core model for a supercompact cardinal? What properties should it have, and what should be its relation with $V$.
The reason I am asking this question, is that we can not expect such a model be $L-$like, for example square principles should fail in it, from somewhere above, ....
My second question is a bout a concept which seems to play an essential role in core model theorey, namely the notion of iteration trees.
Question 2. Can one explain me in a very short way, what are ``iteration trees'' and what is their relation with core model constructions?
As far as I understand the iterability in core model constructions is important.
Question 3. How can one expect to construct a core model for supercompact cardinals? Do we expect iteration trees play any role in the construction, and if yes, how?
My finial last question is about forcing and core models. Most of known core models are known to be invariant under set generic extensions, in the sense that if $V[G]$ is a set generic extension of $V$, then $\mathcal{K}_V=\mathcal{K}_{V[G]},$ where $\mathcal{K}_V$ is the corresponding core model as computed in $V$. This is the case for example for $L$, or Dodd-Jensen core model, ...
Question 4. Is there any known core model which is not invariant under set forcing extensions? What if we consider cardinal preserving (or even tame ) class generic extensions?
Of course core models like $L$, Dodd-Jensen core model, ... are invariant under cardinal preserving class generic extensions.