The Ax-Grothendieck Theorem says that if $V$ is a variety over an algebraically closed field $K$ , and $f:V\to V$ is a morphism of varieties such that $V(K)\to V(K)$ is injective, then $V(K)\to V(K)$ is bijective. Here, "variety" can be interpreted as finite-type scheme over $K$ .

The Ax-Grothendieck theorem has a relatively straightforward proof using model theory, and is often listed as an example of a theorem that is easy to prove using mathematical logic, and harder to prove directly using algebraic geometry.

Proof sketch[]

Varieties can be seen as (special) definable sets, and morphisms of varieties yield definable maps. Therefore, it suffices to show that for every model $K$ of ACF, the following condition holds:

(*) If $D\subset K^{n}$ is definable (with parameters) and $f:D\to D$ is definable (with parameters), and injective, then $f$ is a bijection.

Conditition (*) is equivalent to a small conjunction of first-order statements (an easy exercise). In other words, the set of models of ACF satisfying (*) is an elementary class.

Suppose $K\models ACF$ has the property that the definable closure of any finite subset is finite. Then (*) holds. Indeed, suppose $f:D\hookrightarrow D$ is definable and injective, and $p\in D$ . Let $S$ be a finite set over which $f,D,p$ are defined. Then $f$ induces an injective map from $D(S):=D\cap \operatorname {dcl} (S)$ to itself. Since $D(S)$ is finite, $f$ is a bijection, by the pigeonhole principle. So $p\in f(D)$ , and $f$ is surjective.

The algebraic closure ${\overline {\mathbb {F} _{p}}}$ of $\mathbb {F} _{p}$ is a model of ACF in which every finite set has finite definable closure. (The perfect field generated by any finite set is finite.) So (*) holds in ${\overline {\mathbb {F} _{p}}}$ . Every characteristic $p$ model of ACF (every model of $ACF_{p}$ ) is elementarily equivalent to ${\overline {\mathbb {F} _{p}}}$ . Since (*) is a conjunction of first-order statements, (*) holds in all models of $ACF_{p}$ . Then by compactness, it also holds in at least one model of $ACF_{0}$ , hence in all models of $ACF_{0}$ . So (*) holds in all models of ACF. ::: ::: :::