Extender

An extender is a collection of ultrafilters which, when combined, are able to coherently code a single elementary embedding (this can be either a nontrivial elementary embedding between a universe and an inner model, or a cofinal elementary embedding between two models of ZFC minus the powerset axiom). Namely, an extender consists of ultrafilters \(E_a\), where \(a\) is a finite set of ordinals, which cohere in a certain way, so that one is able to take the direct limit of the ultrapowers of the universe. Extenders, or sequences of them, are used to build inner models (more precisely, extender models), which possess the fine structure of \(L\) yet witness the existence of elementary embeddings of the universe - namely, one starts with \(L\) and then "enriches" the definable powerset operator by allowing a predicate for the set \(\{(a,x): x \in E_a\}\). Therefore the model sees such elementary embeddings while still satisfying the axiom of choice.