I'm not sure whether this belongs here or on math stackexchange, but I'll give a try here. 


I've heard that an extender is a generalization of an ultrafilter. This is not to say that an ultrafilter is the same sort of object as an extender, since whereas an ultrafilter on an uncountable $\kappa$ is in $V\_{\kappa + 2}$, an extender in general is an element of a much higher level $V\_\alpha$. But that an extender captures all the information an ultrafilter has about elementary embeddings. Or so I think. 


What I am trying to prove is a precise statement of this:


*Lemma*: given a non-principal $\kappa$-complete ultrafilter on an uncountable $\kappa$, and $j: V \rightarrow M \cong Ult(V,U)$, there is an extender $E$ such that $j\_E : V \rightarrow M$ and also $j\_E = j$. ($j\_E$ is the embedding built from $E$, that is, $j\_E$ elementarily maps $V$ into the direct limit of a direct system, one whose elements are ultraproducts of $V$, and whose maps are appropriately defined to commute with the maps from $V$ to these ultraproducts.)


I've tried to take the extender $F$ of a short length such that $F\_a = U$. Then all the maps of the direct system are the identity, and the direct limit will be our original $M$, and $j\_E = j$. *But* I'm not convinced this is a genuine extender in that is satisfies one of the (all equivalent?) definitions of extenders. 


Another approach is to take $j\_U$, and take the embedding $E\_{j\_U}$ derived from it, and then try to show $j\_{E\_{j\_U}} = j$. This will in fact be an extender, but I can't show whether the target model $M\_E$ agrees with $M$. 


Any ideas or suggestions?



An Extender is a Generalization of an Ultrafilter?
My preferred account of extenders is the following: an elementary
embedding $j:V\to M$ is an extender embedding if every element of
$M$ can be expressed in the form $j(f)(\alpha)$, where
$f:\kappa\to V$ and $\alpha\lt j(\kappa)$.


(With this extender concept, it is obvious that any ultrapower by
a normal measure on $\kappa$ is an extender, since in this case
every element of $M$ has the form $j(f)(\kappa)$. More generally,
if $j:V\to M$ is the ultrapower by any ultrafilter $U$ on a set
$I$, then it is an elementary exercise to see that every element
of $M$ has the form $j(f)([id]\_U)$, were $id:I\to I$ is the
identity map.)


With this extender concept, one never needs *all* the ordinals
$\alpha$ up to $j(\kappa)$, and more generally one has a set
$S\subset j(\kappa)$ of generators, such that every element of $M$
has the form $j(f)(s)$, where $s\in S^{\lt\omega}$ and
$f:\kappa^{\lt\omega}\to V$.


In this formulation, the extender object itself can be viewed as
the set $$E=\{(s,X)\mid X\subset\kappa^{\lt\omega},s\in
S^{\lt\omega},s\in j(X)\},$$
which contains all the information
necessary to rebuild the embedding. For any fixed seed $s\in
S^{\lt\omega}$, one has the induced measure $U\_s=\{X\mid s\in
j(X)\}$, and the corresponding ultrapower maps $j\_s:V\to
M\_s=V^{\kappa^{|s|}}/U\_s$ fit into a directed system of
embeddings, for whenever $s\subset t$ then we may build the map
$k\_{s,t}:M\_s\to M\_t$ by transforming functions in the obvious way.
The extender embedding $j:V\to M$ will be precisely the direct
limit of this system of ultrapowers. One way to see this is by
using the representation of the direct limit as equivalence
classes of threads, and mapping any thread containing $[f]\_{U\_s}$
to $j(f)(s)$, which will be well-defined, $\in$-preserving and
surjective, hence an isomorphism. Alternatively, one can verify
the universal property, in that if we have maps $r\_s:M\_s\to N$,
then we can build a factor map $r:M\to N$ via $j(f)(s)\mapsto
r\_s([f]\_{U\_s})$, which is well-defined and elementary.


