Documentation

Mathlib.FieldTheory.IsAlgClosed.Classification

Classification of Algebraically closed fields #

This file contains results related to classifying algebraically closed fields.

Main statements #

theorem IsAlgClosed.isAlgClosure_of_transcendence_basis {R : Type u_1} {K : Type u_3} [CommRing R] [Field K] [Algebra R K] {ι : Type u_4} (v : ιK) [IsAlgClosed K] (hv : IsTranscendenceBasis R v) :
def IsAlgClosed.equivOfTranscendenceBasis {R : Type u_1} {L : Type u_2} {K : Type u_3} [CommRing R] [Field K] [Algebra R K] [Field L] [Algebra R L] {ι : Type u_4} (v : ιK) {κ : Type u_5} (w : κL) [IsAlgClosed K] [IsAlgClosed L] (e : ι κ) (hv : IsTranscendenceBasis R v) (hw : IsTranscendenceBasis R w) :

setting R to be ZMod (ringChar R) this result shows that if two algebraically closed fields have equipotent transcendence bases and the same characteristic then they are isomorphic.

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

    The cardinality of an algebraically closed R-algebra is less than or equal to the maximum of of the cardinality of R, the cardinality of a transcendence basis and ℵ₀

    For a simpler, but less universe-polymorphic statement, see IsAlgClosed.cardinal_le_max_transcendence_basis'

    The cardinality of an algebraically closed R-algebra is less than or equal to the maximum of of the cardinality of R, the cardinality of a transcendence basis and ℵ₀

    A less-universe polymorphic, but simpler statement of IsAlgClosed.cardinal_le_max_transcendence_basis

    If K is an uncountable algebraically closed field, then its cardinality is the same as that of a transcendence basis.

    For a simpler, but less universe-polymorphic statement, see IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt'

    If K is an uncountable algebraically closed field, then its cardinality is the same as that of a transcendence basis.

    This is a simpler, but less general statement of cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt.

    Two uncountable algebraically closed fields of characteristic zero are isomorphic if they have the same cardinality.

    Two uncountable algebraically closed fields are isomorphic if they have the same cardinality and the same characteristic.