Looking for extender axioms

115 Views Asked by At

Consider the following extender construction:

Given an elementary embedding $j:V\to M$, where $M$ is transitive, with critical point $\kappa$, we can for each $a\in j(V_{\kappa})$ define a $\kappa$-complete ultrafilter $U_a = \{ x\in V_{\kappa}\, |\, a\in j(x)\}$ on $V_{\kappa}$. The ultrapowers $Ult(V,U_a)$ embed into $M$ by $k_a: [f]_{U_a} \mapsto j(f)(a)$ for all $f:V_{\kappa}\to V$.

We can also define $A = \{ j(f)(a)\, |\, f:V_{\kappa}\to V\, \land \, a\in j(V_{\kappa})\}$, which is an elementary substructure of $M$, and each $Ult(V,U_{a})$ also embeds into it.

Next we could define some relation $<_0$ on $j(V_{\kappa})$ that is directed and lets us definably extract each individual $<_0$-predecessor of an $a\in j(V_{\kappa})$ from $a$, e.g. $a<_0 b$ iff $b$ is an n-tuple for some $n<\omega$ and $a$ is one of the components.

Then for $a<_0 b$ we have $\{ j(f)(a)\, |\, f:V_{\kappa}\to V \} \subseteq \{ j(f)(b)\, |\, f:V_{\kappa}\to V \}$ and this inclusion is elementary. We therefore have an embedding $i_{a,b} :Ult(V,U_a)\to Ult(V,U_b)$ by following $k_a$ by $k_b^{-1}$.

The direct limit of the $Ult(V,U_a)$ for $a\in j(V_{\kappa})$ is isomorphic to $A$ with the direct limit of the $k_a$ corresponding to the inclusion of $A$ in $M$.

It is the case that $k_a([id_{V_{\kappa}}]_{U_a})=a$ for all $a\in j(V_{\kappa})$.

Now my question is: There are axioms that characterize extender embeddings of $V$ if we are talking about the $(\kappa,\beta)$-extenders. I have been trying a bit to come up with a compact set of axioms that could sum up this setting. (i.e. axioms for ultrafilters $U_a$ for $a\in T$ for some transitive set $T$ (with certain closure properties?), a relation $<_0$ and something that gives rise to maps $i_{a,b}$ for $a<_0 b$.) In particular, the axioms should imply the limit of the emeddings of $V$ to $Ult(V,U_a)$ has critical point $\kappa$, with each $a\in T$ corresponding to $[id_{V_{\kappa}}]_{U_a}$ and the limit of the ultrapowers being well-founded. And the axioms should not mention models and embeddings, they should only talk about the filters.

Is there something known on this topic could somebody provide me with an idea?

edit: I was looking at A proof of projective determinacy by Martin and Steel, p. 83-84, but that's not quite it.