English
In an algebraically closed field K, every injective polynomial map K^n → K^n is surjective.
Русский
Пусть K — алгебраически замкнутое поле. Любое инъективное полиномиальное отображение K^n → K^n является сюръектом.
LaTeX
$$$$\\forall p:\\nath (\\iota \\to \\mathrm{MvPolynomial}_{\\iota} K),\\\\\n(\\lambda v,i. eval v (p i)).Injective\\;\\Rightarrow\\; (\\lambda v,i. eval v (p i)).Surjective$$$$
Lean4
/-- A special case of the **Ax-Grothendieck** theorem
Any injective polynomial map `K^n → K^n` is also surjective if `K` is an
algebraically closed field. -/
theorem ax_grothendieck_univ (p : ι → MvPolynomial ι K) :
(fun v i => eval v (p i)).Injective → (fun v i => eval v (p i)).Surjective := by
simpa [Set.injective_iff_injOn_univ, Set.surjective_iff_surjOn_univ] using ax_grothendieck_zeroLocus 0 p
