Classification of Algebraically closed fields

This file contains results related to classifying algebraically closed fields.

Main statements

• IsAlgClosed.equivOfTranscendenceBasis Two algebraically closed fields with the same characteristic and the same cardinality of transcendence basis are isomorphic.
• IsAlgClosed.ringEquivOfCardinalEqOfCharEq Two uncountable algebraically closed fields are isomorphic if they have the same characteristic and the same cardinality.

theorem Algebra.IsAlgebraic.cardinal_mk_le_sigma_polynomial (R : Type u) (L : Type u) [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [NoZeroSMulDivisors R L] [Algebra.IsAlgebraic R L] : Cardinal.mk L ≤ Cardinal.mk ((p : Polynomial R) × { x : L // x ∈ p.aroots L })

theorem Algebra.IsAlgebraic.cardinal_mk_le_max (R : Type u) (L : Type u) [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [NoZeroSMulDivisors R L] [Algebra.IsAlgebraic R L] : Cardinal.mk L ≤ max (Cardinal.mk R) Cardinal.aleph0

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

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) : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K

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) : K ≃+* L

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.

theorem IsAlgClosed.cardinal_le_max_transcendence_basis {R : Type u} {K : Type u} [CommRing R] [Field K] [Algebra R K] [IsAlgClosed K] {ι : Type u} (v : ι → K) (hv : IsTranscendenceBasis R v) : Cardinal.mk K ≤ max (max (Cardinal.mk R) (Cardinal.mk ι)) Cardinal.aleph0

theorem IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt {R : Type u} {K : Type u} [CommRing R] [Field K] [Algebra R K] [IsAlgClosed K] {ι : Type u} (v : ι → K) [Nontrivial R] (hv : IsTranscendenceBasis R v) (hR : Cardinal.mk R ≤ Cardinal.aleph0) (hK : Cardinal.aleph0 < Cardinal.mk K) : Cardinal.mk K = Cardinal.mk ι

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

theorem IsAlgClosed.ringEquivOfCardinalEqOfCharZero {K : Type} {L : Type} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L] [CharZero K] [CharZero L] (hK : Cardinal.aleph0 < Cardinal.mk K) (hKL : Cardinal.mk K = Cardinal.mk L) : Nonempty (K ≃+* L)

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

theorem IsAlgClosed.ringEquivOfCardinalEqOfCharEq {K : Type} {L : Type} [Field K] [Field L] [IsAlgClosed K] [IsAlgClosed L] (p : ℕ) [CharP K p] [CharP L p] (hK : Cardinal.aleph0 < Cardinal.mk K) (hKL : Cardinal.mk K = Cardinal.mk L) : Nonempty (K ≃+* L)

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