Extender model
Extender models are inner models, which have similar fine structure to Gödel's \(L\), but which are able to accommodate large cardinals, typically at the level of measurable cardinals and above. Extender models are either constructed - where they have the form \(L[\vec{E}]\) (here, \(\vec{E}\) is an extender or a coherent sequence of them) - and have their fine structure analysed, or are defined in a more broad scope and the abstract properties of all such models considered. For example, a notion of a (weak) extender model for supercompactness has been isolated, and the properties of such models analysed, however an actual construction of such a model is extremely difficult and has not yet been carried out. N.b: the HOD dichotomy implies that \(\mathrm{HOD}\) may be a weak extender model for supercompactness, but it lacks the necessary fine structure, as mentioned on the page.
In general, if a large cardinal property \(\Phi(\kappa)\) is equivalent to "for all \(\xi \geq \kappa\), there is an ultrafilter \(U_\xi\) on \(X_\xi\) so that \(\psi(U_\xi, \xi)\) holds", where \(X_\xi\) is an arbitrary set and \(\psi\) is an arbitrary formula, the assertion "\(N\) is a weak extender model for \(\Phi(\kappa)\)" means that, for all \(\xi \geq \kappa\), there is an ultrafilter \(U_\xi\) so that \(\psi(U_\xi, \xi)\) holds, \(N \cap X_\xi \in U_\xi\) and \(U_\xi \cap N \in N\). This notion is obviously designed to generalize the properties of a particular constructed extender model - for example, "\(N\) is a weak extender model for \(\kappa\)'s measurability" means that there is an ultrafilter \(U\) witnessing \(\kappa\)'s measurability so that \(U \cap N \in N\) and if \(\kappa\) is a measurable cardinal and \(U\) witnesses this, then \(L[U]\) is the minimal weak extender model for \(\kappa\)'s measurability.
"\(N\) is a weak extender model for \(\kappa\)'s supercompactness" means that, for all \(\lambda \geq \kappa\), there is an ultrafilter \(U\) witnessing \(\kappa\)'s \(\lambda\)-supercompactness so that \(N \cap [\lambda]^{< \kappa} \in U\) and \(U \cap N \in N\).
Weak extender models for supercompactness not only are universal but also possess the following potent closure property: if \(N\) is a weak extender model for \(\kappa\)'s supercompactness and \(\lambda > \kappa\) is a cardinal in \(N\), then, for any elementary embedding \(j: H(\lambda^+)^N \to H(j(\lambda)^+)^N\) with critical point at least \(\kappa\), we have \(j \in N\). This follows from the weak extender model version of Magidor's lemma. Furthermore, If \(E\) is an \(N\)-extender with length \(\eta\) and the embedding \(j_E\) generated by \(E\) has critical point at least \(\kappa\), and, for each \(A \subseteq \eta\), we have \(j_E(A) \cap \eta \in N\), then \(E \cap N \in N\).
Therefore, the HOD hypothesis implies that, if \(\delta\) is an extendible cardinal, \(\lambda > \kappa\) is a cardinal in \(\mathrm{HOD}\), and \(j: H(\lambda^+)^{\mathrm{HOD}} \to H(j(\lambda)^+)^{\mathrm{HOD}}\) is an elementary embedding with critical point at least \(\delta\), \(j\) is ordinal-definable. In fact, an even stronger theorem holds: assume the HOD hypothesis holds and there is an extendible cardinal. Then there is an ordinal \(\lambda\) so that, for all \(\gamma > \lambda\), if \(j: \mathrm{HOD} \cap V_{\gamma+1} \to \mathrm{HOD} \cap V_{j(\gamma)+1}\) is an elementary embedding with \(j(\lambda) = \lambda\) (so the critical point is either above or far below \(\lambda\)), then \(j\) is hereditarily ordinal-definable.