English
A first-order sentence φ is modeled by algebraically closed fields of characteristic zero iff it is modeled by algebraically closed fields of characteristic p for infinitely many primes p.
Русский
Для первой‑порядковой формулы φ она истинна в теории алгебраически замкнутых полей характеристики нуль тогда и только тогда, когда φ истинна для бесконечно многих простых p в теории алгебраически замкнутых полей характеристики p.
LaTeX
$$$\text{Theory.ACF }0 \models \varphi \iff \{p:\text{Nat.Primes} \mid \text{Theory.ACF }p \models \varphi\} \text{ бесконечно}.$$$
Lean4
theorem finite_ACF_prime_not_realize_of_ACF_zero_realize (φ : Language.ring.Sentence) (h : Theory.ACF 0 ⊨ᵇ φ) :
Set.Finite {p : Nat.Primes | ¬Theory.ACF p ⊨ᵇ φ} :=
by
rw [Theory.models_iff_finset_models] at h
rcases h with ⟨T0, hT0, h⟩
have f : ∀ ψ ∈ Theory.ACF 0, { s : Finset Nat.Primes // ∀ q : Nat.Primes, q ∉ s → Theory.ACF q ⊨ᵇ ψ } :=
by
intro ψ hψ
rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm, Set.mem_union, if_pos rfl, Set.mem_image] at hψ
apply Classical.choice
rcases hψ with h | ⟨p, hp, rfl⟩
· refine ⟨⟨∅, ?_⟩⟩
intro q _
exact
Theory.models_sentence_of_mem
(by rw [Theory.ACF, Theory.fieldOfChar, Set.union_right_comm]; exact Set.mem_union_left _ h)
· refine ⟨⟨{⟨p, hp⟩}, ?_⟩⟩
rintro ⟨q, _⟩ hq ⟨K⟩ _ _
have hqp : q ≠ p := by simpa [← Nat.Primes.coe_nat_inj] using hq
let _ := fieldOfModelACF q K
have := modelField_of_modelACF q K
let _ := compatibleRingOfModelField K
have := charP_of_model_fieldOfChar q K
simp only [eqZero, Term.equal, BoundedFormula.realize_not, BoundedFormula.realize_bdEqual, Term.realize_relabel,
Sum.elim_comp_inl, realize_termOfFreeCommRing, map_natCast, realize_zero, ← CharP.charP_iff_prime_eq_zero hp]
intro _
exact hqp <| CharP.eq K this inferInstance
let s : Finset Nat.Primes := T0.attach.biUnion (fun φ => f φ.1 (hT0 φ.2))
have hs : ∀ (p : Nat.Primes) ψ, ψ ∈ T0 → p ∉ s → Theory.ACF p ⊨ᵇ ψ :=
by
intro p ψ hψ hpψ
simp only [s, Finset.mem_biUnion, Finset.mem_attach, true_and, Subtype.exists, not_exists] at hpψ
exact (f ψ (hT0 hψ)).2 p (hpψ _ hψ)
refine Set.Finite.subset (Finset.finite_toSet s) (Set.compl_subset_comm.2 ?_)
intro p hp
exact Theory.models_of_models_theory (fun ψ hψ => hs p ψ hψ hp) h
