English
For finite ι and prime p (or p = 0), the Ax–Grothendieck theorem holds for the given polynomial maps in the algebraic closure context; i.e., the realizable models satisfy surjectivity statements for generic polynomial maps.
Русский
Для конечного множества ι и простого p (или p = 0) теорема Акс–Гротендикета применяется к данным полиномным отображениям в рамках алгебраических замыканий; модели удовлетворяют свойствам сюръективности для общих полиномных отображений.
LaTeX
$$$ \\text{Theorem } \\text{ACF}_p \\models\\n \\text{genericPolyMapSurjOnOfInjOn}_{\\varphi,\\text{mons}} $$$
Lean4
/-- Any injective polynomial map over an algebraic extension of a finite field is surjective. -/
theorem ax_grothendieck_of_locally_finite {ι K R : Type*} [Field K] [Finite K] [CommRing R] [Finite ι] [Algebra K R]
[alg : Algebra.IsAlgebraic K R] (ps : ι → MvPolynomial ι R) (S : Set (ι → R))
(hm : S.MapsTo (fun v i => eval v (ps i)) S) (hinj : S.InjOn (fun v i => eval v (ps i))) :
S.SurjOn (fun v i => eval v (ps i)) S :=
by
have is_int : ∀ x : R, IsIntegral K x := fun x => isAlgebraic_iff_isIntegral.1 (alg.isAlgebraic x)
classical
intro v hvS
cases nonempty_fintype ι
let s : Finset R :=
(Finset.biUnion (univ : Finset ι) fun i => (ps i).support.image fun x => coeff x (ps i)) ∪ (univ : Finset ι).image v
have hv : ∀ i, v i ∈ Algebra.adjoin K (s : Set R) := fun j =>
Algebra.subset_adjoin (mem_union_right _ (mem_image.2 ⟨j, mem_univ _, rfl⟩))
have hs₁ : ∀ (i : ι) (k : ι →₀ ℕ), k ∈ (ps i).support → coeff k (ps i) ∈ Algebra.adjoin K (s : Set R) := fun i k hk =>
Algebra.subset_adjoin (mem_union_left _ (mem_biUnion.2 ⟨i, mem_univ _, mem_image_of_mem _ hk⟩))
have := isNoetherian_adjoin_finset s fun x _ => is_int x
have : Finite (Algebra.adjoin K (s : Set R)) := Module.finite_of_finite K
let S' : Set (ι → Algebra.adjoin K (s : Set R)) := (fun v => Subtype.val ∘ v) ⁻¹' S
let res : S' → S' := fun x =>
⟨fun i => ⟨eval (fun j : ι => (x.1 j : R)) (ps i), eval_mem (hs₁ _) fun i => (x.1 i).2⟩, hm x.2⟩
have hres_surj : Function.Surjective res :=
by
rw [← Finite.injective_iff_surjective]
intro x y hxy
ext i
simp only [Subtype.ext_iff, funext_iff] at hxy
exact congr_fun (hinj x.2 y.2 (funext hxy)) i
rcases hres_surj ⟨fun i => ⟨v i, hv i⟩, hvS⟩ with ⟨⟨w, hwS'⟩, hw⟩
refine ⟨fun i => w i, hwS', ?_⟩
simpa [Subtype.ext_iff, funext_iff] using hw
