Classification of Algebraically closed fields #
This file contains results related to classifying algebraically closed fields.
Main statements #
is_alg_closed.equiv_of_transcendence_basisTwo fields with the same characteristic and the same cardinality of transcendence basis are isomorphic.is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eqTwo 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) :
cardinal.mk L ≤ cardinal.mk (Σ (p : polynomial R), {x // x ∈ (polynomial.map (algebra_map R L) p).roots})
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) :
The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or ℵ₀
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
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))
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) :
theorem
is_alg_closed.cardinal_eq_cardinal_transcendence_basis_of_aleph_0_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 : cardinal.mk R ≤ cardinal.aleph_0)
(hK : cardinal.aleph_0 < 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.
@[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 : cardinal.aleph_0 < cardinal.mk K)
(hKL : cardinal.mk K = cardinal.mk L) :
K ≃+* L
Two uncountable algebraically closed fields of characteristic zero are isomorphic if they have the same cardinality.
@[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 : cardinal.aleph_0 < cardinal.mk K)
(hKL : cardinal.mk K = cardinal.mk L) :
K ≃+* L
Two uncountable algebraically closed fields are isomorphic if they have the same cardinality and the same characteristic.