Theorems · Theorem · algebraic geometry

FirstOrder.realize_genericPolyMapSurjOnOfInjOn

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

Defined in

Mathlib.FieldTheory.AxGrothendieck

Cited by

2 results in Mathlib

Foundations

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

Assumes

FiniteFieldFirstOrder.Ring.CompatibleRingFinite