[proofplan]
The proof is a back-and-forth argument controlled by algebraic closure. First we show that finite independent tuples from the two bases extend to elementary bijections between the corresponding algebraic closures, using uniqueness of the non-algebraic type over algebraically closed sets in a strongly minimal theory and the algebraic-extension lemma for elementary partial maps. Then we use [Zorn's lemma](/theorems/1226) to build one maximal coherent elementary map extending $g\cup f$ on as much of the basis as possible; maximality forces its basis domain to be all of $B$. Since the bases generate the models under algebraic closure, this maximal map is an isomorphism $M\to N$.
[/proofplan]
[step:Prove the algebraic closure extension lemma]
[claim:Algebraic closures over a partial elementary map can be matched]
In this proof, an elementary bijection between subsets means a partial elementary map: a bijection $u:D\to D'$ such that for every integer $m\geq 1$, every tuple $a=(a_1,\dots,a_m)\in D^m$, and every $\mathcal L$-formula $\varphi(x_1,\dots,x_m)$,
\begin{align*}
M\models \varphi(a_1,\dots,a_m)\quad\Longleftrightarrow\quad N\models \varphi(u(a_1),\dots,u(a_m)).
\end{align*}
If $D\subseteq M$ and $D'\subseteq N$ are algebraically closed subsets and $u:D\to D'$ is a partial elementary bijection, then for any tuples $a\in M^r$ and $a'\in N^r$ such that $u\cup\{(a_i,a'_i):1\leq i\leq r\}$ is partial elementary, this map extends to a partial elementary bijection
\begin{align*}
\operatorname{acl}^M(D\cup\{a_1,\dots,a_r\})&\to \operatorname{acl}^N(D'\cup\{a'_1,\dots,a'_r\}).
\end{align*}
[/claim]
[proof]
Let $v_0:=u\cup\{(a_i,a'_i):1\leq i\leq r\}$, and define
\begin{align*}
D_a&:=D\cup\{a_1,\dots,a_r\},&
D'_{a'}&:=D'\cup\{a'_1,\dots,a'_r\}.
\end{align*}
For any finite tuple $d\in \operatorname{acl}^M(D_a)^m$, the complete type $\operatorname{tp}^M(d/D_a)$ is algebraic. Choose an $\mathcal L(D_a)$-formula $\theta(x)$ in this type whose solution set in $M$ is finite and has minimal possible cardinality among algebraic formulas in the type. Minimality implies that $\theta(x)$ isolates $\operatorname{tp}^M(d/D_a)$: if an $\mathcal L(D_a)$-formula $\psi(x)$ did not have a truth value decided by $\theta(x)$, then one of $\theta(x)\wedge\psi(x)$ and $\theta(x)\wedge\neg\psi(x)$ would be a strictly smaller non-empty algebraic formula in the type.
Transport $\theta$ by $v_0$ to an $\mathcal L(D'_{a'})$-formula $v_0(\theta)(x)$. Suppose $\theta(x)$ has exactly $q\in\mathbb N$ realizations in $M$. For each integer $k\geq 1$, the assertion that there exist at least $k$ pairwise distinct realizations of $\theta$ is first-order over $D_a$. Since $v_0$ is partial elementary, the corresponding assertion holds for $v_0(\theta)$ in $N$ exactly when it holds for $\theta$ in $M$. Hence $v_0(\theta)(x)$ has exactly $q$ realizations in $N$. Choose $d'\in N^m$ satisfying $v_0(\theta)(d')$. Because $v_0(\theta)$ isolates the transported algebraic type, the extension sending $d$ to $d'$ is partial elementary. This gives the forth step; the same argument applied to $v_0^{-1}$ gives the back step for tuples from $\operatorname{acl}^N(D'_{a'})$.
Enumerating the two algebraic closures and alternating these forth and back extensions, with unions taken at limit stages, yields a partial elementary bijection from $\operatorname{acl}^M(D_a)$ onto $\operatorname{acl}^N(D'_{a'})$ extending $v_0$.
[/proof]
[/step]
[step:Show that finite basis tuples extend to elementary maps on their algebraic closures]
Let $b=(b_1,\dots,b_n) \in B^n$ be a tuple of pairwise distinct elements. For each $i\in\{1,\dots,n\}$, define $c_i:=f(b_i)\in C$, and write
\begin{align*}
c &:=(c_1,\dots,c_n)\in C^n.
\end{align*}
We prove that there exists an elementary bijection
\begin{align*}
h_b:\operatorname{acl}^M(A_M\cup\{b_1,\dots,b_n\})&\to \operatorname{acl}^N(A_N\cup\{c_1,\dots,c_n\})
\end{align*}
extending $g$ and satisfying $h_b(b_i)=c_i$ for each $i\in\{1,\dots,n\}$.
We use induction on $n$. For $n=0$, this is the given elementary bijection $g:A_M\to A_N$. Assume that
\begin{align*}
h_n:E_M&\to E_N
\end{align*}
is an elementary bijection, where
\begin{align*}
E_M&:=\operatorname{acl}^M(A_M\cup\{b_1,\dots,b_n\}),\\
E_N&:=\operatorname{acl}^N(A_N\cup\{c_1,\dots,c_n\}).
\end{align*}
Let $b_{n+1}\in B\setminus\{b_1,\dots,b_n\}$ and define $c_{n+1}:=f(b_{n+1})\in C$. Since $B$ and $C$ are bases, $b_{n+1}\notin E_M$ and $c_{n+1}\notin E_N$.
By the [unique generic type over algebraically closed sets in a strongly minimal theory](/page/Strongly%20Minimal%20Theory), over an algebraically closed parameter set there is a unique non-algebraic complete $1$-type: for every formula $\varphi(x,e)$ with parameter tuple $e$ from the algebraically [closed set](/page/Closed%20Set), $\varphi(x,e)$ belongs to that type exactly when its complement is algebraic over the parameter set. Applying this to $E_M$ and transporting formulas by $h_n$, the elements $b_{n+1}$ and $c_{n+1}$ realize corresponding non-algebraic types over $E_M$ and $E_N$. Hence
\begin{align*}
h_n\cup\{(b_{n+1},c_{n+1})\}:E_M\cup\{b_{n+1}\}&\to E_N\cup\{c_{n+1}\}
\end{align*}
is elementary. The claim on matching algebraic closures applies with $D=E_M$, $D'=E_N$, $u=h_n$, $a=b_{n+1}$, and $a'=c_{n+1}$. Its hypotheses hold because $E_M$ and $E_N$ are algebraically closed by definition and the displayed map is partial elementary. Therefore it extends to an elementary bijection
\begin{align*}
h_{n+1}:\operatorname{acl}^M(E_M\cup\{b_{n+1}\})&\to \operatorname{acl}^N(E_N\cup\{c_{n+1}\}),
\end{align*}
which is the required induction step.
[guided]
The point of this step is not merely to compare the finite tuples $b$ and $c$; we must also build the elementary correspondence between the algebraic closures generated by those tuples. This avoids using an unnamed map between $\operatorname{acl}^M(A_M\cup b)$ and $\operatorname{acl}^N(A_N\cup c)$ before such a map has been constructed.
Fix distinct basis elements $b_1,\dots,b_n\in B$. For each $i\in\{1,\dots,n\}$, define $c_i:=f(b_i)\in C$. We prove by induction on $n$ that there is an elementary bijection
\begin{align*}
h_b:\operatorname{acl}^M(A_M\cup\{b_1,\dots,b_n\})&\to \operatorname{acl}^N(A_N\cup\{c_1,\dots,c_n\})
\end{align*}
extending $g$ and sending each $b_i$ to $c_i$.
For $n=0$, the algebraic closures are $A_M$ and $A_N$, and the required map is exactly the elementary bijection $g:A_M\to A_N$ from the theorem statement.
Assume the construction has been made for $b_1,\dots,b_n$. Thus we have an elementary bijection
\begin{align*}
h_n:E_M&\to E_N,
\end{align*}
where
\begin{align*}
E_M&:=\operatorname{acl}^M(A_M\cup\{b_1,\dots,b_n\}),\\
E_N&:=\operatorname{acl}^N(A_N\cup\{c_1,\dots,c_n\}).
\end{align*}
Now choose $b_{n+1}\in B\setminus\{b_1,\dots,b_n\}$ and define $c_{n+1}:=f(b_{n+1})$. Since $B$ is algebraically independent over $A_M$, the element $b_{n+1}$ is not in $E_M$. Since $C$ is algebraically independent over $A_N$, the element $c_{n+1}$ is not in $E_N$.
We now use strong minimality over the already constructed algebraically closed domains. By the [unique generic type over algebraically closed sets in a strongly minimal theory](/page/Strongly%20Minimal%20Theory), if $E$ is algebraically closed in a model of a strongly minimal theory, then there is a unique non-algebraic complete $1$-type over $E$. Indeed, let $\varphi(x,e)$ be an $\mathcal L$-formula with parameter tuple $e$ from $E$. Strong minimality says that the definable set $\varphi(M,e)$ is finite or cofinite. If it is finite, then every element satisfying $\varphi(x,e)$ is algebraic over $E$, so no element outside $\operatorname{acl}(E)$ satisfies it. If it is cofinite, then the complement is finite and therefore algebraic over $E$, so every element outside $\operatorname{acl}(E)$ satisfies $\varphi(x,e)$. Thus an element outside $\operatorname{acl}(E)$ has its complete type over $E$ determined solely by which definable subsets are cofinite.
Apply this with $E=E_M$ and $E=E_N$. Because $h_n:E_M\to E_N$ is elementary, it sends each formula over $E_M$ to the corresponding formula over $E_N$ and preserves whether the corresponding definable set is finite or cofinite. Since $b_{n+1}\notin E_M$ and $c_{n+1}\notin E_N$, the two elements realize corresponding unique non-algebraic types over these algebraically closed domains. Therefore the map
\begin{align*}
h_n\cup\{(b_{n+1},c_{n+1})\}:E_M\cup\{b_{n+1}\}&\to E_N\cup\{c_{n+1}\}
\end{align*}
is elementary.
It remains to pass from the elementary map on $E_M\cup\{b_{n+1}\}$ to the algebraic closures generated by this domain. The claim on matching algebraic closures applies with $D=E_M$, $D'=E_N$, $u=h_n$, $a=b_{n+1}$, and $a'=c_{n+1}$. We have already checked that $h_n\cup\{(b_{n+1},c_{n+1})\}$ is partial elementary, and $E_M,E_N$ are algebraically closed by their definitions as algebraic closures. The claim therefore gives an elementary bijection
\begin{align*}
h_{n+1}:\operatorname{acl}^M(E_M\cup\{b_{n+1}\})&\to \operatorname{acl}^N(E_N\cup\{c_{n+1}\})
\end{align*}
extending $h_n\cup\{(b_{n+1},c_{n+1})\}$. This completes the induction and constructs the required elementary bijection on the algebraic closures.
[/guided]
[/step]
[step:Build one maximal coherent elementary map by Zorn's lemma]
Let $\mathcal P$ be the set of pairs $(B_0,h_0)$ such that $B_0\subseteq B$ and
\begin{align*}
h_0:\operatorname{acl}^M(A_M\cup B_0)&\to \operatorname{acl}^N(A_N\cup f(B_0))
\end{align*}
is an elementary bijection extending $g\cup f|_{B_0}$. Order $\mathcal P$ by extension: $(B_0,h_0)\leq (B_1,h_1)$ when $B_0\subseteq B_1$ and $h_1|_{\operatorname{acl}^M(A_M\cup B_0)}=h_0$.
The set $\mathcal P$ is non-empty because $(\varnothing,g)\in\mathcal P$. If $\mathcal C\subseteq\mathcal P$ is a chain, define
\begin{align*}
B_{\mathcal C}&:=\bigcup_{(B_0,h_0)\in\mathcal C}B_0,\\
h_{\mathcal C}&:=\bigcup_{(B_0,h_0)\in\mathcal C}h_0.
\end{align*}
Compatibility in the chain makes $h_{\mathcal C}$ a well-defined elementary map. By the [finite character of algebraic closure](/page/Algebraic%20Closure), if $a\in\operatorname{acl}^M(A_M\cup B_{\mathcal C})$, then there is a finite set $F\subseteq B_{\mathcal C}$ such that $a\in\operatorname{acl}^M(A_M\cup F)$. For each $b\in F$, choose $(B_b,h_b)\in\mathcal C$ with $b\in B_b$. Since $F$ is finite and $\mathcal C$ is linearly ordered, one member $(B_0,h_0)\in\mathcal C$ contains all elements of $F$ in its basis part, so $a\in\operatorname{acl}^M(A_M\cup B_0)$. The same argument on the $N$ side shows that $h_{\mathcal C}$ has range $\operatorname{acl}^N(A_N\cup f(B_{\mathcal C}))$. Hence $(B_{\mathcal C},h_{\mathcal C})\in\mathcal P$ is an upper bound for the chain. By [Zorn's Lemma](/page/Zorn%27s%20Lemma), choose a maximal element $(B_*,h_*)\in\mathcal P$.
We prove that $B_*=B$. Suppose not, and choose $b\in B\setminus B_*$. Define $c:=f(b)\in C$. Since $B$ and $C$ are bases, $b\notin\operatorname{acl}^M(A_M\cup B_*)$ and $c\notin\operatorname{acl}^N(A_N\cup f(B_*))$. By the [unique generic type over algebraically closed sets in a strongly minimal theory](/page/Strongly%20Minimal%20Theory), transported through the elementary bijection $h_*$, the map
\begin{align*}
h_*\cup\{(b,c)\}:\operatorname{acl}^M(A_M\cup B_*)\cup\{b\}&\to \operatorname{acl}^N(A_N\cup f(B_*))\cup\{c\}
\end{align*}
is elementary. Apply the claim on matching algebraic closures with
\begin{align*}
D&:=\operatorname{acl}^M(A_M\cup B_*),&
D'&:=\operatorname{acl}^N(A_N\cup f(B_*)),&
u&:=h_*,&
a&:=b,&
a'&:=c.
\end{align*}
The sets $D$ and $D'$ are algebraically closed by definition, and the previous paragraph shows that $h_*\cup\{(b,c)\}$ is partial elementary. The claim gives an elementary bijection
\begin{align*}
h':\operatorname{acl}^M(A_M\cup B_*\cup\{b\})&\to \operatorname{acl}^N(A_N\cup f(B_*\cup\{b\}))
\end{align*}
extending $h_*\cup\{(b,c)\}$. This contradicts maximality of $(B_*,h_*)$. Therefore $B_*=B$.
[/step]
[step:Identify the maximal map as an isomorphism of the two models]
Set $H:=h_*$, where $(B_*,h_*)$ is the maximal element constructed in the previous step. Since $B_*=B$, the domain and range of $H$ are
\begin{align*}
\operatorname{dom}(H)&=\operatorname{acl}^M(A_M\cup B),\\
\operatorname{Range}(H)&=\operatorname{acl}^N(A_N\cup f(B)).
\end{align*}
Because $B$ is a basis of $M$ over $A_M$ and $f(B)=C$ is a basis of $N$ over $A_N$,
\begin{align*}
M&=\operatorname{acl}^M(A_M\cup B),\\
N&=\operatorname{acl}^N(A_N\cup C)=\operatorname{acl}^N(A_N\cup f(B)).
\end{align*}
Thus $H$ has domain $M$ and range $N$. Therefore $H:M\to N$ is an $\mathcal L$-isomorphism extending $g\cup f$.
[/step]
[step:Derive the dimension classification]
If $\dim(M)=\dim(N)$, then there is a bijection $f:B\to C$ between bases. The construction above gives an isomorphism $M\cong N$ extending the fixed elementary bijection $g:A_M\to A_N$.
Conversely, if $H:M\to N$ is an isomorphism extending $g$, then $H$ preserves [algebraic closure](/page/Algebraic%20Closure) and independence. Hence $H(B)$ is a basis of $N$ over $A_N$. Therefore
\begin{align*}
\dim(M)=|B|=|H(B)|=\dim(N).
\end{align*}
This proves the stated equivalence.
[/step]
