# 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

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

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

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.
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.

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`

.