ACF_models_genericPolyMapSurjOnOfInjOn_of_prime

English

For finite ι and prime p or p = 0, the Ax–Grothendieck realization yields that the theory AC_FP realizes the generic polynomial surjectivity condition for φ mons.

Русский

Для конечного ι и простого p или p = 0, реализация Ax–Grothendieck выполняет условие сюръективности для общих отображений полиномов φ mons.

LaTeX

$$$ (\\text{ACF } p) \\modelsᵇ genericPolyMapSurjOnOfInjOn φ mons $$$

Lean4

theorem ACF_models_genericPolyMapSurjOnOfInjOn_of_prime [Finite ι] {p : ℕ} (hp : p.Prime) (φ : ring.Formula (α ⊕ ι))
    (mons : ι → Finset (ι →₀ ℕ)) : Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons := by
  classical
  have : Fact p.Prime := ⟨hp⟩
  letI := compatibleRingOfRing (AlgebraicClosure (ZMod p))
  rw [← (ACF_isComplete (Or.inl hp)).realize_sentence_iff _ (AlgebraicClosure (ZMod p)),
    realize_genericPolyMapSurjOnOfInjOn]
  rintro v ⟨f, _⟩
  exact ax_grothendieck_of_locally_finite (K := ZMod p) (ι := ι) f _

Похожие утверждения