Documentation

Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

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 #

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
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
        @[reducible]

        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.