Documentation

Mathlib.FieldTheory.AxGrothendieck

Ax-Grothendieck for algebraic extensions of ZMod p #

This file proves that if R is an algebraic extension of a finite field, then any injective polynomial map R^n → R^n is also surjective.

This proof is required for the true Ax-Grothendieck theorem, which proves the same result for any algebraically closed field of characteristic zero.

TODO #

The proof of the theorem for characteristic zero is not in mathlib, but it is at https://github.com/Jlh18/ModelTheoryInLean8

theorem ax_grothendieck_of_locally_finite {ι : Type u_1} {K : Type u_2} {R : Type u_3} [Field K] [Finite K] [CommRing R] [Finite ι] [Algebra K R] [Algebra.IsAlgebraic K R] (ps : ιMvPolynomial ι R) (hinj : Function.Injective fun (v : ιR) (i : ι) => (MvPolynomial.eval v) (ps i)) :
Function.Surjective fun (v : ιR) (i : ι) => (MvPolynomial.eval v) (ps i)

Any injective polynomial map over an algebraic extension of a finite field is surjective.