The First Order Theory of Algebraically Closed Fields

This file defines the theory of algebraically closed fields of characteristic p, as well as proving completeness of the theory and the Lefschetz Principle.

Main definitions

• FirstOrder.Language.Theory.ACF p : the theory of algebraically closed fields of characteristic p as a theory over the language of rings.
• FirstOrder.Field.ACF_isComplete : the theory of algebraically closed fields of characteristic p is complete whenever p is prime or zero.
• FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize : the Lefschetz principle.

Implementation details

To apply a theorem about the model theory of algebraically closed fields to a specific algebraically closed field K which does not have a Language.ring.Structure instance, you must introduce the local instance compatibleRingOfRing K. Theorems whose statement requires both a Language.ring.Structure instance and a Field instance will all be stated with the assumption Field K, CharP K p, IsAlgClosed K and CompatibleRing K and there are instances defined saying that these assumptions imply Theory.field.Model K and (Theory.ACF p).Model K

References

The first order theory of algebraically closed fields, along with the Lefschetz Principle and the Ax-Grothendieck Theorem were first formalized in Lean 3 by Joseph Hua here with the master's thesis here

def FirstOrder.Field.genericMonicPoly (n : ℕ) : FreeCommRing (Fin (n + 1))

A generic monic polynomial of degree n as an element of the free commutative ring in n+1 variables, with a variable for each of the n non-leading coefficients of the polynomial and one variable (Fin.last n) for X.

Equations

• FirstOrder.Field.genericMonicPoly n = FreeCommRing.of (Fin.last n) ^ n + ∑ i : Fin n, FreeCommRing.of i.castSucc * FreeCommRing.of (Fin.last n) ^ ↑i

theorem FirstOrder.Field.lift_genericMonicPoly {K : Type u_1} [CommRing K] [Nontrivial K] {n : ℕ} (v : Fin (n + 1) → K) : (FreeCommRing.lift v) (FirstOrder.Field.genericMonicPoly n) = Polynomial.eval (v (Fin.last n)) ↑(((Polynomial.monicEquivDegreeLT n).trans (Polynomial.degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc))

noncomputable def FirstOrder.Field.genericMonicPolyHasRoot (n : ℕ) : FirstOrder.Language.ring.Sentence

A sentence saying every monic polynomial of degree n has a root.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Field.realize_genericMonicPolyHasRoot {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] (n : ℕ) : K ⊨ FirstOrder.Field.genericMonicPolyHasRoot n ↔ ∀ (p : { p : Polynomial K // p.Monic ∧ p.natDegree = n }), ∃ (x : K), Polynomial.eval x ↑p = 0

def FirstOrder.Language.Theory.ACF (p : ℕ) : FirstOrder.Language.ring.Theory

The theory of algebraically closed fields of characteristic p as a theory over the language of rings

Equations

• FirstOrder.Language.Theory.ACF p = FirstOrder.Language.Theory.fieldOfChar p ∪ FirstOrder.Field.genericMonicPolyHasRoot '' {n : ℕ | 0 < n}

instance FirstOrder.Field.instModelFieldOfCharOfACF {K : Type u_1} [FirstOrder.Language.ring.Structure K] (p : ℕ) [h : K ⊨ FirstOrder.Language.Theory.ACF p] : K ⊨ FirstOrder.Language.Theory.fieldOfChar p

Equations

• ⋯ = ⋯

instance FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed {K : Type u_1} [Field K] [FirstOrder.Ring.CompatibleRing K] {p : ℕ} [CharP K p] [IsAlgClosed K] : K ⊨ FirstOrder.Language.Theory.ACF p

Equations

• ⋯ = ⋯

theorem FirstOrder.Field.modelField_of_modelACF (p : ℕ) (K : Type u_2) [FirstOrder.Language.ring.Structure K] [h : K ⊨ FirstOrder.Language.Theory.ACF p] : K ⊨ FirstOrder.Language.Theory.field

@[reducible]

noncomputable def FirstOrder.Field.fieldOfModelACF (p : ℕ) (K : Type u_2) [FirstOrder.Language.ring.Structure K] [h : K ⊨ FirstOrder.Language.Theory.ACF p] : Field K

A model for the Theory of algebraically closed fields is a Field. After introducing this as a local instance on a particular Type, you should usually also introduce modelField_of_modelACF p M, compatibleRingOfModelField and isAlgClosed_of_model_ACF

Equations

• FirstOrder.Field.fieldOfModelACF p K = FirstOrder.Field.fieldOfModelField K

theorem FirstOrder.Field.isAlgClosed_of_model_ACF (p : ℕ) (K : Type u_2) [Field K] [FirstOrder.Ring.CompatibleRing K] [h : K ⊨ FirstOrder.Language.Theory.ACF p] : IsAlgClosed K

theorem FirstOrder.Field.ACF_isSatisfiable {p : ℕ} (hp : Nat.Prime p ∨ p = 0) : (FirstOrder.Language.Theory.ACF p).IsSatisfiable

theorem FirstOrder.Field.ACF_categorical {p : ℕ} (κ : Cardinal.{0}) (hκ : Cardinal.aleph0 < κ) : κ.Categorical (FirstOrder.Language.Theory.ACF p)

The Theory Theory.ACF p is κ-categorical whenever κ is an uncountable cardinal. At the moment this is not as universe polymorphic as it could be, it currently requires κ : Cardinal.{0}, but it is true for any universe.

theorem FirstOrder.Field.ACF_isComplete {p : ℕ} (hp : Nat.Prime p ∨ p = 0) : (FirstOrder.Language.Theory.ACF p).IsComplete

theorem FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize (φ : FirstOrder.Language.ring.Sentence) (h : FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ) : {p : Nat.Primes | ¬FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Finite

theorem FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize {φ : FirstOrder.Language.ring.Sentence} : FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p : Nat.Primes | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}.Infinite

The Lefschetz principle. A first order sentence is modeled by the theory of algebraically closed fields of characteristic zero if and only if it is modeled by the theory of algebraically closed fields of characteristic p for infinitely many p.

theorem FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize {φ : FirstOrder.Language.ring.Sentence} : FirstOrder.Language.Theory.ACF 0 ⊨ᵇ φ ↔ {p : Nat.Primes | FirstOrder.Language.Theory.ACF ↑p ⊨ᵇ φ}ᶜ.Finite

Another statement of the Lefschetz principle. A first order sentence is modeled by the theory of algebraically closed fields of characteristic zero if and only if it is modeled by the theory of algebraically closed fields of characteristic p for all but finitely many primes p.