Artin’s Theorem Towards the Existence of Algebraic Closures
Christoph Schwarzweller · Formalized Mathematics · 2022
Summary This is the first part of a two-part article formalizing existence and uniqueness of algebraic closures using the Mizar system [1], [2]. Our proof follows Artin’s classical one as presented by Lang in [3]. In this first part we prove that for a given field F there exists a field extension E such that every non-constant polynomial p ∈ F [ X ] has a root in E . Artin’s proof applies Kronecker’s construction to each polynomial p ∈ F [ X ] \F simultaneously. To do so we need the polynomial ring F [ X 1 , X 2 , ...] with infinitely many variables, one for each polynomal p ∈ F [ X ] \F . The desired field extension E then is F [ X 1 , X 2 , ...] \I , where I is a maximal ideal generated by all non-constant polynomials p ∈ F [ X ]. Note, that to show that I is maximal Zorn’s lemma has to be applied. In the 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 p ∈ A [ 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 F → A , where A is an algebraic closure of F can be extended to a monomorphism E → A , 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.