Theorems · Theorem · algebraic geometry

ax_grothendieck_zeroLocus

• 1000+ list: Ax–Grothendieck theorem

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

Defined in

Mathlib.FieldTheory.AxGrothendieck

Cited by

1 results in Mathlib

Foundations

Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldIsAlgClosedFinite