English
Let K be algebraically closed and I an ideal in the ring of multivariate polynomials in I variables. If S is the zero locus of I in K^I, then any injective polynomial self-map of S is surjective onto S.
Русский
Пусть K — алгебраически замкнутое поле, I — идеал в кольце многочленов в несколько переменных. Пусть S = zeroLocus(K,I) в K^I. Тогда любая инъективная полиномиальная отображение S → S является сюръектом на S.
LaTeX
$$$$\\forall I,\\ I.K, \\ I.(I : \\text{Ideal} (\\mathrm{MvPolynomial}_{\\iota} K)),\\\\\nS := \\mathrm{zeroLocus} K I, \nS.MapsTo (\\lambda v,i. eval v (p i)) S \\Rightarrow S.InjOn (\\lambda v,i. eval v (p i)) \\Rightarrow S.SurjOn (\\lambda v,i. eval v (p i)) S$$$$
Lean4
/-- The **Ax-Grothendieck** theorem
If `K` is an algebraically closed field, and `S : Set (ι → K)` is the `zeroLocus` of an ideal
of the multivariable polynomial ring, then any injective polynomial map `S → S` is also
surjective on `S`. -/
theorem ax_grothendieck_zeroLocus (I : Ideal (MvPolynomial ι K)) (p : ι → MvPolynomial ι K) :
let S := zeroLocus K I
S.MapsTo (fun v i => eval v (p i)) S → S.InjOn (fun v i => eval v (p i)) → S.SurjOn (fun v i => eval v (p i)) S :=
by
letI := compatibleRingOfRing K
intro S
obtain ⟨s, rfl⟩ : I.FG := IsNoetherian.noetherian I
exact ax_grothendieck_of_definable S (mvPolynomial_zeroLocus_definable s) p
