Ax-Grothendieck for algebraic extensions of zmod p #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
[comm_ring R]
[finite ι]
[algebra K R]
(alg : algebra.is_algebraic K R)
(ps : ι → mv_polynomial ι R)
(hinj : function.injective (λ (v : ι → R) (i : ι), ⇑(mv_polynomial.eval v) (ps i))) :
function.surjective (λ (v : ι → R) (i : ι), ⇑(mv_polynomial.eval v) (ps i))
Any injective polynomial map over an algebraic extension of a finite field is surjective.