Let $T$ be a theory with a good notion of independence. Generally, we have in mind forking independence, though something weaker would be acceptable. In fact, for our proof, the only properties we use are that independence is invariant under replacing a set by its algebraic closure
- For $A \subseteq B$ and $A \subseteq C$, we have that $B$ is free from $C$ over $A$ if and only if $\operatorname{acl}(B)$ is free from $\operatorname{C}$ over $\operatorname{A}$. Here, $\operatorname{acl}$ is the algebraic closure in the home sort. We are not assuming elimination of imaginaries.
the fact that
- For any pair of sets $A \subseteq B$ we have that $B$ is free from $A$ over $A$.
and two monotonicity properties for independence
- If $A$ is independent over $B$ and $C \subseteq A$, then $C$ is independent over $B$.
- If $A \subseteq B \subseteq C$ and $C$ is independent over $A$, then $C \smallsetminus B$ is independent over $B$.
(To be honest we also use, very weakly, the hypothesis that $\operatorname{acl}(\varnothing) \neq \varnothing$.)
Let $n$ be a von Neumann natural number, that is, $n = \{0, 1, \ldots, n-1\}$. We write $\mathcal{P}(n)^-$ for $\mathcal{P}(n) \smallsetminus n$. Let $W \subseteq \mathcal{P}(n)$ be closed downwards. That is, if $v \subseteq w \in W$, then $v \in W$.
A $W$-variable assignment is an association $w \mapsto x_w$ from $W$ to variables ranging over some (possibly infinite) product $S_w$ of sorts so that for $w \leq v \in W$, we require that $S_v$ is a subproduct of $S_w$ and if $\pi_{w,v}:S_w \to S_v$ is the natural projection, then $x_v = x_w \circ \pi_{w,v}$. If $\{i\} \in W$, then we write $x_{\{i\}} =: x_i$. Note our conventions: $x_i$ may be naturally a tuple (even infinite) of variables. In this way, if $i \in w \in W$, then $x_i = x_w \circ \pi_{w,\{i\}}$.
By an $W$-independent system of types we mean that we are given a $W$-variable assignment and then for each $w \in W$ a complete type $p_w$ relative to $T$ in the variable $x_w$ so that
- If $v \subseteq w$, then $p_v = {\pi_{w,v}}_* (p_w)$.
- $p_w \vdash \{ x_i : i \in w\}$ is independent.
- $p_w \vdash x_w \subseteq \operatorname{acl}(\{ x_i : i \in w \})$. Recall that $x_w$ ranges over some product of sorts $S_w$. With this condition we are asking that $p_w$ include formulae explicitly requiring each component of $x_w$ to lie be algebraic over the components of the $x_i$ for $i \in w$.
We say that $T$ has $n$-amalgamation over algebraically closed sets if for every model $M \models T$, every $E \subseteq M$ with $\operatorname{acl}(E) = E$, every downward closed $W \subseteq \mathcal{P}(n)$, and every $W$-independent system $(p_w)_{w \in W}$ of types relative to $\operatorname{Th}(M_E)$, there is a $\mathcal{P}(n)$-independent system $(q_u)_{u \in \mathcal{P}(n)}$ with $q_w = p_w$ for $w \in W$.
Lemma: A theory $T$ has independent $n$-amalgamation over algebraically closed sets if and only if it has independent $m$-amalgamation for all $m < n$ and every $\mathcal{P}(n)^{-}$-independent system over an algebraically closed subset of a model of $T$ may be extended to a $\mathcal{P}(n)$-independent system.
Proof: The left to right direction is immediate. For the other direction, we suppose that $T$ has independent $m$-amalgamation for all $m < n$ and every $\mathcal{P}(n)^{-}$-independent system over an algebraically closed subset of a model of $T$ may be extended to a $\mathcal{P}(n)$-independent system, that $W \subseteq \mathcal{P}(n)$ is downwards closed and that $(p_w)_{w \in W}$ is a $W$-independent system over some algebraically closed subset $E$ of some model of $T$.
If $W = \mathcal{P}(n)$.
Working by induction on $|W|$, it suffices to show that we may extend the system to any given downwards closed $W’ \supseteq W$ with $|W’ \smallsetminus W| = 1$. Let $w \in W’ \smallsetminus W$.
- If $w = n$, then $W = \mathcal{P}(n)^-$ so that by our hypotheses on $T$ we may extend the system.
- If $w = \{ i \}$ for some $i \in n$, then pick any $e \in E$ (this is where we are using the hypothesis that $\operatorname{acl}(\varnothing) \neq \varnothing$). Set $p_i := \ulcorner x_i = e \urcorner$. Then because $p_i \vdash x_i \in E$, this extension is $W’$-independent. Here we are using both of our hypotheses about the behavior of the notion of independence with respect to algebraic closure.
- If $1 < |w| < n$, then by our hypothesis that all independent systems over $\mathcal{P}(|w|)^-$ may be extended, we can find $p_w$ so that $(p_u)_{u \subseteq w}$ is a $\mathcal{P}(w)$-independent system. The resulting system $\{ p_w \} \cup (p_u)_{u \in W}$ is a $W’$-independent system. $\Box$
Lemma: A theory $T$ has $n$-amalgamation over algebraically closed sets if and only if every independent system in which (3) is strengthened to (3)’: $x_w = \operatorname{acl}(\{x_i:i \in w\})$ may be extended to a $\mathcal{P}(n)$-independent system.
Proof: Let us start with some downwards closed $W \subseteq \mathcal{P}(n)$ and a $W$-independent system satisfying the usual definition and show how to expand it to a $W$-independent system $(q_w)_{w \in W}$ in the variables $(y_w)_{w \in W}$ satisfying (3)’ so that for each $w$ the variable $x_w$ ranges over a subtuple of $y_w$ and $p_w = q_w \upharpoonright \mathcal{L}_{x_w}$. We work by induction on the size of $B := \{ w \in W : p_w \not \vdash x_w = \operatorname{acl}(\{ x_i : i \in w \}) \}$. If $B = \varnothing$, we are done. Note that if $w \in W \smallsetminus B$, then for every $u \subseteq w$ we have $u \notin B$ as well. Thus, if $B \neq \varnothing$, there is some $w \in B$ so that $\{ u \in W : w \subseteq u \} = \{w\}$. Pick such a $w$. Let $a_w$ realize $p_w$ in some model $M \models T$. Let $b_w$ be (an enumeration of) $\operatorname{acl}(a_w)$. Let $y_w$ be the variable context corresponding to this enumeration of $b_w$. For $u \subseteq w$, let $b_u := b_w \cap \operatorname{acl}(a_u)$ where $a_u$ is the restriction to $x_u$ of $b_u$ and where we choose the variable context $y_u$ for $b_u$ compatibly with $y_w$ and the pre-existing $x_u$. Set $q_u := \operatorname{tp}(a_u/E)$. For $u \in W$ with $u \not \subseteq w$, let $y_u$ be the concatenation of $x_u$ and $y_{u \cap w}$, identifying $x_{u \cap w}$ with the corresponding subtuple of $y_{u \cap w}$. Let $q_u := p_u \cup q_{u \cap w}$. Then by our first condition on the behavior of independence with respect to algebraic closure, $(q_u)_{u \in W}$ is still a $W$-independent system. $\Box$.
Definition: For $K \models \text{ACFA}$ and $A \subseteq B$ and $A \subseteq C$, we say that $B$ is free from $C$ over $A$ if $\operatorname{acl}(B)$ is free from $\operatorname{acl}(C)$ over $\operatorname{acl}(A)$ in the sense of ACF. Equivalently, the field $\operatorname{acl}(B)$ is linearly disjoint from the field $\operatorname{acl}(C)$ over the field $\operatorname{acl}(A)$.
Theorem: For every natural number $n$, ACFA has independent $n$-amalgamation over algebraically closed sets.
Proof: Note that the case of $n = 1$ is trivial – take $p_{0}$ to be any type over $E$. Working by induction $n$, we may assume that we know ACFA has independent $m$-amalgamation of algebraically closed sets for $m < n$. By our lemmas, it suffices to consider $E \subseteq \mathbb{U} \models \text{ACFA}$ where $E = \operatorname{acl}(E)$, $K$ is $|E|^+$-saturated, and $(p_w)_{w \in \mathcal{P}(n)^-}$ is an independent $\mathcal{P}(n)^-$-system over $E$ in which $p_w \vdash x_w = \operatorname{acl}(E \cup \{ x_i : i \in w\})$. Let $W’ := \{ w \in \mathcal{P}(n)^- : n-1 \in w \}$. Let $a_n \models p_n$. For $u \in \mathcal{P}(n-1)^-$, let $y_u = x_{u \cup \{n-1\}}$ and set $q_u := p_{u \cup \{ n \}} \cup x_n = a_n \in S_{y_u}(a_n)$. The system $(q_u)_{u \in \mathcal{P}(n-1)^-}$ is a $\mathcal{P}(n-1)^-$-independent system over the algebraically closed $a_n$. Hence, by induction, it may be extended to a $\mathcal{P}(n-1)$-independent system $(q_u)_{u \in \mathcal{P}(n-1)^-}$. Let $b$ realize $q_{\{0, \ldots, n-2\}}$ and let $L := \operatorname{acl}(b)$. (If we were to apply our lemma about requiring (3)’ to hold, then we would already have $b = L$.). Let $K$ be the compositum of $b_u := x_u(b)$ for $u \in \mathcal{P}(n-1)$. Let $M$ be (generated by) a realization of $p_{\{0, 1, \ldots, n-2\}}$. We have a copy of $K$ embedded in $M$ so that $M = K^\text{alg}$ (though it need not be the case that $M = K^\text{alg}$ as a sub-difference field of $\mathbb{U}$.
Because $K$ is a compositum of algebraically closed fields, and both $M$ and $L$ are perfect, check that $M \otimes_K L$ is a domain, it suffices to show that $M \cap L = K$. Note that if we succeed in showing that $M \otimes_K L$ is a domain, then embedding this domain (with the endomorphisms coming from $\sigma$ on each tensor factor) into $\mathbb{U}$ over $E$, we could complete the system by taking $a_{\{0, \ldots, n-1\}}$ to be the image of $ a_{\{0, \ldots, n-2\}} \otimes 1 \frown 1 \otimes b$ and $p_{\{0, \ldots, n-1\}} := \operatorname{tp}(a_{\{0, \ldots, n-1\}}/E)$, we complete the system.
Let us check now that $M \cap L = K$. Let $c \in M \cap L$. Any element $c$ of $L$ may be expressed as $c = \sum_{i=1}^m \prod_{u \in \mathcal{P}(n-1)^-} c_{i,u}$ where $c_{i,u} \in \operatorname{acl}(a_{n-1},b_w)$. Let $Q_{i,w}(x,y) \in K[x,y]$ be a polynomial so that $Q_{i,w}[x,a_{n-1}]$ is the minimal monic polynomial over $K (a_{n-1})$ of $b_{i,w}$. Let $\phi(x,y) := (\exists z_{i,u})_{i=1,u \in \mathcal{P}(n-1)^-}^m \left( x = \sum_i \prod_w z_{i,w} \land \bigwedge_{i,w} Q_{i,w}(z_{i,w},y) \land Q_{i,w}(X,y) \not \equiv 0 \right)$.
Now, $c$ satisfies $\phi(x,a_{n-1})$ and because $c \in M$, which is the algebraic closure of $\{ a_i : 0 \leq i < n-1\}$, $c$ is free from $a_{n-1}$ over $E$ in the sense of ACF. Hence, $\phi(c,y)$ defines a cofinite set and there is some $a \in E$ so that $\phi(c,a)$ holds. But then $\phi(c,a)$ says that $c$ lies in the compositum of the $b_w$ for $w \in \mathcal{P}(n-1)^-$, that is, in $K$. $\Box$