Search

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 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 needed the polynomial ring F [X1, X2,...] with infinitely many variables, one for each polynomal p ∈ F [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 p ∈ F [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 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. [ABSTRACT FROM AUTHOR]

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 [X1, X2,...] with infinitely many variables, one for each polynomal p ∈ F [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 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. [ABSTRACT FROM AUTHOR]

We study the problem of finding the Artin L-functions with the smallest conductor for a given Galois type. We adapt standard analytic techniques to our novel situation of fixed Galois type and obtain much improved lower bounds on the smallest conductor. For small Galois types we use complete tables of number fields to determine the actual smallest conductor. [ABSTRACT FROM AUTHOR]