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 characteristicp
as a theory over the language of rings.FirstOrder.Field.ACF_isComplete
: the theory of algebraically closed fields of characteristicp
is complete wheneverp
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
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
Instances For
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.
Instances For
The theory of algebraically closed fields of characteristic p
as a theory over
the language of rings
Equations
Instances For
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
Instances For
The Theory Theory.ACF p
is κ
-categorical whenever κ
is an uncountable cardinal.
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
.
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
.