Theorems · Theorem · algebraic geometry

ax_grothendieck_of_definable

∀ {K : Type u_1} {ι : Type u_2} [inst : Field K] [IsAlgClosed K] [Finite ι] [inst_3 : FirstOrder.Ring.CompatibleRing K]
  {c : Set K} (S : Set (ι → K)),
  c.Definable FirstOrder.Language.ring S →
    ∀ (ps : ι → MvPolynomial ι K),
      Set.MapsTo (fun v i => (MvPolynomial.eval v) (ps i)) S S →
        Set.InjOn (fun v i => (MvPolynomial.eval v) (ps i)) S → Set.SurjOn (fun v 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.

Defined in

Mathlib.FieldTheory.AxGrothendieck

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldIsAlgClosedFiniteFirstOrder.Ring.CompatibleRing