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 _