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

I've heard it said 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 ultrafilter, 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.)

One approach I've tried is to take the extender $F$ of a short length such that $F_a = U$. I can then see that all the maps of the direct system are the identity, and that the direct limit will be our original $M$, and that $j_E = j$. But I'm not sure whether this satisfies all the conditions of an extender, at the moment I'm a bit lost on all the conditions an extender has to satisfy.

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'm not sure whether the target model $M_E$ agrees with $M$.

Any ideas on either approach? Thanks!