ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero

English

If p is prime or zero, then for all φ mons the Ax–Grothendieck models hold (or reduce to the prime case).

Русский

Если p простое или ноль, то для всех φ mons выполняются (или редуцируются к) модели Ax–Grothendieck.

LaTeX

$$$ \\text{ACF models for prime or zero}$$$

Lean4

theorem ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero [Finite ι] {p : ℕ} (hp : p.Prime ∨ p = 0)
    (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) : Theory.ACF p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons :=
  by
  rcases hp with hp | rfl
  · exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons
  · rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]
    convert Set.infinite_univ (α := Nat.Primes)
    rw [Set.eq_univ_iff_forall]
    intro ⟨p, hp⟩
    exact ACF_models_genericPolyMapSurjOnOfInjOn_of_prime hp φ mons

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