Theorems · Theorem · algebraic geometry

ax_grothendieck_of_locally_finite

∀ {ι : Type u_1} {K : Type u_2} {R : Type u_3} [inst : Field K] [Finite K] [inst_2 : CommRing R] [Finite ι]
  [inst_4 : Algebra K R] [alg : Algebra.IsAlgebraic K R] (ps : ι → MvPolynomial ι R) (S : Set (ι → R)),
  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

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

Defined in

Mathlib.FieldTheory.AxGrothendieck

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFiniteCommRingFiniteAlgebraAlgebra.IsAlgebraic