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.
The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or
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
- 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))
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.
Two uncountable algebraically closed fields are isomorphic if they have the same cardinality and the same characteristic.