In his answer to user42090's mathoverflow question"Minimal Generalized Contnuum Hypothesis & Axiom of Choice", Prof. Hamkins writes:


"...one can build the analogue of the symmetric models for $\lnot$$AC$ above any cardinal, while preserving $GCH$ below..."


Are there any examples of such models in the literature which also satisfy the large cardinal axiom $I\_0$ (which builds the symmetric model satisfying $\lnot$$AC$ above the '$I\_0$ cardinals') , and how are these models constructed by forcing?


Also, if such models exist, can they serve as a 'laboratory' to study the behavior of $ZF$ beyond the '$AC$ barrier'?



A question regarding models of $ZF+I_0$ [Revised]
I think there's a misunderstanding here: there is *one* method for building a model in which choice breaks, and the point is that to get a model in which choice fails and some large cardinal axiom $(\*)$ holds, we start with a model in which $\kappa$ has $(\*)$, and then cause a failure of AC sufficiently far above $\kappa$ that $\kappa$ still satisfies $(\*)$ in the resulting model.


In this example, if there is an elementary embedding $j$ of $L(V\_{\lambda+1})$ into itself with critical point below $\lambda$, then $j$ is also an elementary embedding of $L(W\_{\lambda+1})$ into itself with critical point below $\lambda$ as long as $W$ is any forcing extension of $V$ such that $W\_{\lambda+1}=V\_{\lambda+1}$. So if we start with a $V\models I\_0$, and add a failure of choice by taking a symmetric submodel of an extension of $V$ by a forcing which is sufficiently closed (so doesn't alter $V\_{\lambda+1}$), the resulting model will still satisfy $I\_0$.




---


EDITED FOR CLARITY: Note that all we're using is that the $I\_0$ axiom depends only on an initial segment of the universe; so breaking choice above that segment won't affect things. This isn't entirely obvious, since unlike e.g. inaccessibility, the $I\_0$ axiom seems to refer to a *proper-class sized* object - namely, $L(V\_{\lambda+1})$ and the embedding $j$. However, the statement "$x\in L(y)$" is absolute, and so things are no more complicated (from a killing-choice-while-preserving-the-axiom point of view) than the case of $I\_1$, which is explicitly about the *set* $V\_\lambda$. 


In principle, we could imagine variations on the $I\_0$ axiom of the following form: "There is an elementary embedding of $M(V\_{\lambda+1})$ into itself with critical point below $\lambda$," where "$M(-)$" is shorthand for "the class of $x$ such that $\varphi(x, -)$" for some $\varphi$. So long as $M(-)$ is always guaranteed to be an inner model, this could be interesting, and if (the formula $\varphi$ associated to) $M$ were sufficiently non-absolute, then there wouldn't be an obvious way to kill choice while preserving "$I\_0(M)$". However, I'm unaware of anything interesting along these lines.


