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 ultrafilterextender, 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?