English
Let K be algebraically closed and I a finite index set. If S is a definable subset of K^I in the language of rings, and ps is a family of multivariable polynomials indexed by I, then whenever the map on S given by evaluating each i-th polynomial on elements of S is a well-defined map S → S that is injective, it is automatically surjective.
Русский
Пусть K — алгебраически замкнутое поле, I — конечное множество индексов. Пусть S⊆K^I является определимым множеством (в языке колец), а ps = (p_i) — семейство много\-зVariables polynomials. Тогда отображение v ↦ (p_i(v))_i по S в S, если оно определено и инъективно, обязательно сюръектно на S.
LaTeX
$$$\\forall K, \\iota, [\\text{Field }K], [\\text{IsAlgClosed }K], [\\text{Finite }\\iota],\\\\\n\\forall S \\subseteq (\\iota \\to K), \\; S\\ Definable_{\\mathcal{L}_{\\text{ring}}}(S)\\;\\Rightarrow \\\\ \\\\forall (ps:\\\\iota \\to \\mathrm{MvPolynomial}_{\\iota} K), \n S.MapsTo (\\lambda v, i. eval v (ps i)) S \\\\Rightarrow S.InjOn (\\lambda v, i. eval v (ps i)) \\\\Rightarrow S.SurjOn (\\lambda v, i. eval v (ps i)) S$$$
Lean4
/-- A slight generalization of the **Ax-Grothendieck** theorem
If `K` is an algebraically closed field, `ι` is a finite type, and `S` is a definable subset of
`ι → K`, then any injective polynomial map `S → S` is also surjective on `S`. -/
theorem ax_grothendieck_of_definable [CompatibleRing K] {c : Set K} (S : Set (ι → K)) (hS : c.Definable Language.ring S)
(ps : ι → MvPolynomial ι K) :
S.MapsTo (fun v i => eval v (ps i)) S →
S.InjOn (fun v i => eval v (ps i)) → S.SurjOn (fun v i => eval v (ps i)) S :=
by
letI := Fintype.ofFinite ι
let p : ℕ := ringChar K
rw [Set.definable_iff_finitely_definable] at hS
rcases hS with ⟨c, _, hS⟩
rw [Set.definable_iff_exists_formula_sum] at hS
rcases hS with ⟨φ, hφ⟩
rw [hφ]
have :=
ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero (CharP.char_is_prime_or_zero K p) φ
(fun i => (ps i).support)
rw [← (ACF_isComplete (CharP.char_is_prime_or_zero K p)).realize_sentence_iff _ K,
realize_genericPolyMapSurjOnOfInjOn] at this
exact this Subtype.val ⟨ps, fun i => Set.Subset.refl _⟩
