Ax-Grothendieck

This file proves that if K is an algebraically closed field, then any injective polynomial map K^n → K^n is also surjective.

Main results

• ax_grothendieck_zeroLocus: If K is algebraically closed, ι is a finite type, and S : Set (ι → K) is the zeroLocus of some ideal of MvPolynomial ι K, then any injective polynomial map S → S is also surjective on S.
• ax_grothendieck_univ: Any injective polynomial map K^n → K^n is also surjective if K is an algberaically closed field.
• ax_grothendieck_of_definable: Any injective polynomial map S → S is also surjective on S if K is an algebraically closed field and S is a definable subset of K^n.
• ax_grothendieck_of_locally_finite: any injective polynomial map R^n → R^n is also surjective whenever R is an algebraic extension of a finite field.

References

The first order theory of algebraically closed fields, along with the Lefschetz Principle and the Ax-Grothendieck Theorem were first formalized in Lean 3 by Joseph Hua here with the master's thesis here

theorem ax_grothendieck_of_locally_finite {ι : Type u_1} {K : Type u_2} {R : Type u_3} [Field K] [Finite K] [CommRing R] [Finite ι] [Algebra K R] [alg : Algebra.IsAlgebraic K R] (ps : ι → MvPolynomial ι R) (S : Set (ι → R)) (hm : Set.MapsTo (fun (v : ι → R) (i : ι) => (MvPolynomial.eval v) (ps i)) S S) (hinj : Set.InjOn (fun (v : ι → R) (i : ι) => (MvPolynomial.eval v) (ps i)) S) : Set.SurjOn (fun (v : ι → R) (i : ι) => (MvPolynomial.eval v) (ps i)) S S

Any injective polynomial map over an algebraic extension of a finite field is surjective.

noncomputable def FirstOrder.genericPolyMapSurjOnOfInjOn {ι : Type u_1} {α : Type u_2} [Finite α] [Fintype ι] (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) : FirstOrder.Language.ring.Sentence

The collection of first order formulas corresponding to the Ax-Grothendieck theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.realize_genericPolyMapSurjOnOfInjOn {ι : Type u_1} {α : Type u_2} [Finite α] {K : Type u_3} [Field K] [FirstOrder.Ring.CompatibleRing K] [Fintype ι] (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) : K ⊨ FirstOrder.genericPolyMapSurjOnOfInjOn φ mons ↔ ∀ (v : α → K) (p : { p : ι → MvPolynomial ι K // ∀ (i : ι), (p i).support ⊆ mons i }), let f := fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (↑p i); let S := fun (x : ι → K) => φ.Realize (Sum.elim v x); Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S

theorem FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime {ι : Type u_1} {α : Type u_2} [Finite α] [Fintype ι] {p : ℕ} (hp : Nat.Prime p) (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) : FirstOrder.Language.Theory.ACF p ⊨ᵇ FirstOrder.genericPolyMapSurjOnOfInjOn φ mons

theorem FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero {ι : Type u_1} {α : Type u_2} [Finite α] [Fintype ι] {p : ℕ} (hp : Nat.Prime p ∨ p = 0) (φ : FirstOrder.Language.ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) : FirstOrder.Language.Theory.ACF p ⊨ᵇ FirstOrder.genericPolyMapSurjOnOfInjOn φ mons

theorem ax_grothendieck_of_definable {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] [FirstOrder.Ring.CompatibleRing K] {c : Set K} (S : Set (ι → K)) (hS : c.Definable FirstOrder.Language.ring S) (ps : ι → MvPolynomial ι K) : Set.MapsTo (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (ps i)) S S → Set.InjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (ps i)) S → Set.SurjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (ps i)) S S

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_zeroLocus {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] (I : Ideal (MvPolynomial ι K)) (p : ι → MvPolynomial ι K) : let S := MvPolynomial.zeroLocus I; Set.MapsTo (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S S → Set.InjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S → Set.SurjOn (fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) S S

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_univ {K : Type u_1} {ι : Type u_2} [Field K] [IsAlgClosed K] [Finite ι] (p : ι → MvPolynomial ι K) : (Function.Injective fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)) → Function.Surjective fun (v : ι → K) (i : ι) => (MvPolynomial.eval v) (p i)

A special case of the Ax-Grothendieck theorem

Any injective polynomial map K^n → K^n is also surjective if K is an algberaically closed field.