REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: `http://hdl.handle.net/11320/14671`
 Tytuł: Artin’s Theorem Towards the Existence of Algebraic Closures Autorzy: Schwarzweller, Christoph Słowa kluczowe: algebraic closurespolynomial rings with countably infinite number of variablesEmil Artin Data wydania: 2022 Data dodania: 15-lut-2023 Wydawca: DeGruyter Open Źródło: Formalized Mathematics, Volume 30, Issue 3, Pages 199-207 Abstrakt: This is the first part of a two-part article formalizing existenceand 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 algebraicclosure 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. Afiliacja: Christoph Schwarzweller - Institute of Informatics, University of Gdańsk, Poland URI: http://hdl.handle.net/11320/14671 DOI: 10.2478/forma-2022-0014 ISSN: 1426-2630 e-ISSN: 1898-9934 Typ Dokumentu: Article metadata.dc.rights.uri: https://creativecommons.org/licenses/by-sa/3.0/ Właściciel praw: © 2022 The Author(s)CC BY-SA 3.0 license Występuje w kolekcji(ach): Formalized Mathematics, 2022, Volume 30, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat