Classification of Algebraically closed fields #

This file contains results related to classifying algebraically closed fields.

Main statements #

is_alg_closed.equiv_of_transcendence_basis Two fields with the same characteristic and the same cardinality of transcendence basis are isomorphic.
is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eq Two uncountable algebraically closed fields are isomorphic if they have the same characteristic and the same cardinality.

theorem algebra.is_algebraic.cardinal_mk_le_sigma_polynomial (R L : Type u) [comm_ring R] [comm_ring L] [is_domain L] [algebra R L] [no_zero_smul_divisors R L] (halg : algebra.is_algebraic R L) :

# L ≤ # (Σ (p : R[X]), {x // x ∈ (polynomial.map (algebra_map R L) p).roots})

source

theorem algebra.is_algebraic.cardinal_mk_le_max (R L : Type u) [comm_ring R] [comm_ring L] [is_domain L] [algebra R L] [no_zero_smul_divisors R L] (halg : algebra.is_algebraic R L) :

# L ≤ max (# R) ω

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

source

theorem is_alg_closed.is_alg_closure_of_transcendence_basis {R : Type u_1} {K : Type u_3} [comm_ring R] [field K] [algebra R K] {ι : Type u_4} (v : ι → K) [is_alg_closed K] (hv : is_transcendence_basis R v) :

is_alg_closure ↥(algebra.adjoin R (set.range v)) K

source

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.

Equations

is_alg_closed.equiv_of_transcendence_basis v w e hv hw = let _inst : is_alg_closure ↥(algebra.adjoin R (set.range v)) K := _, _inst_8 : is_alg_closure ↥(algebra.adjoin R (set.range w)) L := _ in is_alg_closure.equiv_of_equiv K L (_.aeval_equiv.symm.to_ring_equiv.trans ((alg_equiv.of_alg_hom (mv_polynomial.rename ⇑e) (mv_polynomial.rename ⇑(e.symm)) _ _).to_ring_equiv.trans _.aeval_equiv.to_ring_equiv))

source

theorem is_alg_closed.cardinal_le_max_transcendence_basis {R K : Type u} [comm_ring R] [field K] [algebra R K] [is_alg_closed K] {ι : Type u} (v : ι → K) (hv : is_transcendence_basis R v) :

# K ≤ max (max (# R) (# ι)) ω

source

theorem is_alg_closed.cardinal_eq_cardinal_transcendence_basis_of_omega_lt {R K : Type u} [comm_ring R] [field K] [algebra R K] [is_alg_closed K] {ι : Type u} (v : ι → K) [nontrivial R] (hv : is_transcendence_basis R v) (hR : # R ≤ ω) (hK : ω < # K) :

# K = # ι

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

source

@[nolint]

noncomputable theorem is_alg_closed.ring_equiv_of_cardinal_eq_of_char_zero {K L : Type} [field K] [field L] [is_alg_closed K] [is_alg_closed L] [char_zero K] [char_zero L] (hK : ω < # K) (hKL : # K = # L) :

K ≃+* L

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

source

@[nolint]

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 : ω < # K) (hKL : # K = # L) :

K ≃+* L

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