The **Ax-Grothendieck Theorem** says that if *V* is a variety over an algebraically closed field *K*, and *f* : *V* → *V* is a morphism of varieties such that *V*(*K*) → *V*(*K*) is injective, then *V*(*K*) → *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* ⊂ *K*^{n} is definable (with parameters) and *f* : *D* → *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* ⊨ *A**C**F* has the property that the definable closure of any finite subset is finite. Then (*) holds. Indeed, suppose *f* : *D* ↪ *D* is definable and injective, and *p* ∈ *D*. Let *S* be a finite set over which *f*, *D*, *p* are defined. Then *f* induces an injective map from *D*(*S*) := *D* ∩ *d**c**l*(*S*) to itself. Since *D*(*S*) is finite, *f* is a bijection, by the pigeonhole principle. So *p* ∈ *f*(*D*), and *f* is surjective.

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