mathlib documentation


Classification of Algebraically closed fields #

This file contains results related to classifying algebraically closed fields.

Main statements #

The cardinality of an algebraic extension is at most the maximum of the cardinality of the base ring or ℵ₀

noncomputable def is_alg_closed.equiv_of_transcendence_basis {R : Type u_1} {L : Type u_2} {K : Type u_3} [comm_ring R] [field K] [algebra R K] [field L] [algebra R L] {ι : Type u_4} (v : ι K) {κ : Type u_5} (w : κ L) [is_alg_closed K] [is_alg_closed L] (e : ι κ) (hv : is_transcendence_basis R v) (hw : is_transcendence_basis R w) :
K ≃+* L

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


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


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

noncomputable theorem is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eq {K L : Type} [field K] [field L] [is_alg_closed K] [is_alg_closed L] (p : ) [char_p K p] [char_p L p] (hK : cardinal.aleph_0 < K) (hKL : K = L) :
K ≃+* L

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