The Ax-Grothendieck Theorem says that if {\displaystyle V} is a variety over an algebraically closed field {\displaystyle K}, and {\displaystyle f:V\to V} is a morphism of varieties such that {\displaystyle V(K)\to V(K)} is injective, then {\displaystyle V(K)\to V(K)} is bijective. Here, "variety" can be interpreted as finite-type scheme over {\displaystyle 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 {\displaystyle K} of ACF, the following condition holds:

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

The algebraic closure {\displaystyle {\overline {\mathbb {F} _{p}}}} of {\displaystyle \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 {\displaystyle {\overline {\mathbb {F} _{p}}}}. Every characteristic {\displaystyle p} model of ACF (every model of {\displaystyle ACF_{p}}) is elementarily equivalent to {\displaystyle {\overline {\mathbb {F} _{p}}}}. Since (*) is a conjunction of first-order statements, (*) holds in all models of {\displaystyle ACF_{p}}. Then by compactness, it also holds in at least one model of {\displaystyle ACF_{0}}, hence in all models of {\displaystyle ACF_{0}}. So (*) holds in all models of ACF. ::: ::: :::