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

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

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'

theorem IsAlgClosed.cardinal_le_max_transcendence_basis' {R : Type u} [CommRing R] {K' : Type u} [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

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

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

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'

theorem IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt' {R : Type u} [CommRing R] {K' : Type u} [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.

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

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

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

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

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