Acceso abierto

Existence and Uniqueness of Algebraic Closures


This is the second part of a two-part article formalizing existence and uniqueness of algebraic closures, using the Mizar [2], [1] formalism. Our proof follows Artin’s classical one as presented by Lang in [3]. In the first part we proved that for a given field F there exists a field extension E such that every non-constant polynomial pF [X] has a root in E. Artin’s proof applies Kronecker’s construction to each polynomial pF [X]\F simultaneously. To do so we needed the polynomial ring F [X1, X2, ...] with infinitely many variables, one for each polynomal pF [X]\F. The desired field extension E then is F [X1, X2, …]\I, where I is a maximal ideal generated by all non-constant polynomials pF [X]. Note, that to show that I is maximal Zorn’s lemma has to be applied.

In this second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension A of F, in which every non-constant polynomial pA[X] has a root. The field of algebraic elements of A then is an algebraic closure of F. To prove uniqueness of algebraic closures, e.g. that two algebraic closures of F are isomorphic over F, the technique of extending monomorphisms is applied: a monomorphism FA, where A is an algebraic closure of F can be extended to a monomorphism EA, where E is any algebraic extension of F. In case that E is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.

Calendario de la edición:
Volume Open
Temas de la revista:
Computer Sciences, other, Mathematics, General Mathematics