English
The theory ACF p is κ-categorical for every uncountable cardinal κ.
Русский
Теория ACF p катигориальна для любого неприводимого кардинала κ, большего чем счетный.
LaTeX
$$theorem ACF_categorical (κ : Cardinal) (hκ : ℵ₀ < κ) : Categorical κ (Theory.ACF p)$$
Lean4
/-- The Theory `Theory.ACF p` is `κ`-categorical whenever `κ` is an uncountable cardinal. -/
theorem ACF_categorical {p : ℕ} (κ : Cardinal) (hκ : ℵ₀ < κ) : Categorical κ (Theory.ACF p) :=
by
rintro ⟨M⟩ ⟨N⟩ hM hN
let _ := fieldOfModelACF p M
have := modelField_of_modelACF p M
let _ := compatibleRingOfModelField M
have := isAlgClosed_of_model_ACF p M
have := charP_of_model_fieldOfChar p M
let _ := fieldOfModelACF p N
have := modelField_of_modelACF p N
let _ := compatibleRingOfModelField N
have := isAlgClosed_of_model_ACF p N
have := charP_of_model_fieldOfChar p N
constructor
refine languageEquivEquivRingEquiv.symm ?_
apply Classical.choice
refine IsAlgClosed.ringEquiv_of_equiv_of_char_eq p ?_ ?_
· rw [hM]; exact hκ
· rw [← Cardinal.eq, hM, hN]
