{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T13:50:45Z","timestamp":1777470645035,"version":"3.51.4"},"reference-count":6,"publisher":"Walter de Gruyter GmbH","issue":"3","license":[{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,10,1]]},"abstract":"Summary<\/jats:title>\n \n 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\u2019s classical one as presented by Lang in [3]. In this first part we prove that for a given field\n F<\/jats:italic>\n there exists a field extension\n E<\/jats:italic>\n such that every non-constant polynomial\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ] has a root in\n E<\/jats:italic>\n . Artin\u2019s proof applies Kronecker\u2019s construction to each polynomial\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ]\n \\F<\/jats:italic>\n simultaneously. To do so we need the polynomial ring\n F<\/jats:italic>\n [\n X<\/jats:italic>\n 1<\/jats:sub>\n ,\n X<\/jats:italic>\n 2<\/jats:sub>\n , ...] with infinitely many variables, one for each polynomal\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ]\n \\F<\/jats:italic>\n . The desired field extension\n E<\/jats:italic>\n then is\n F<\/jats:italic>\n [\n X<\/jats:italic>\n 1<\/jats:sub>\n ,\n X<\/jats:italic>\n 2<\/jats:sub>\n , ...]\n \\I<\/jats:italic>\n , where\n I<\/jats:italic>\n is a maximal ideal generated by all non-constant polynomials\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ]. Note, that to show that\n I<\/jats:italic>\n is maximal Zorn\u2019s lemma has to be applied.\n <\/jats:p>\n \n In the second part this construction is iterated giving an infinite sequence of fields, whose union establishes a field extension\n A<\/jats:italic>\n of\n F<\/jats:italic>\n , in which every non-constant polynomial\n p<\/jats:italic>\n \u2208\n A<\/jats:italic>\n [\n X<\/jats:italic>\n ] has a root. The field of algebraic elements of\n A<\/jats:italic>\n then is an algebraic closure of\n F<\/jats:italic>\n . To prove uniqueness of algebraic closures, e.g. that two algebraic closures of\n F<\/jats:italic>\n are isomorphic over\n F<\/jats:italic>\n , the technique of extending monomorphisms is applied: a monomorphism\n F<\/jats:italic>\n \u2192\n A<\/jats:italic>\n , where\n A<\/jats:italic>\n is an algebraic closure of\n F<\/jats:italic>\n can be extended to a monomorphism\n E<\/jats:italic>\n \u2192\n A<\/jats:italic>\n , where\n E<\/jats:italic>\n is any algebraic extension of\n F<\/jats:italic>\n . In case that\n E<\/jats:italic>\n is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn\u2019s lemma.\n <\/jats:p>","DOI":"10.2478\/forma-2022-0014","type":"journal-article","created":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T13:07:56Z","timestamp":1672405676000},"page":"199-207","source":"Crossref","is-referenced-by-count":2,"title":["Artin\u2019s Theorem Towards the Existence of Algebraic Closures"],"prefix":"10.2478","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9587-8737","authenticated-orcid":false,"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[{"name":"Institute of Informatics , University of Gdanacute;sk , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2022,12,30]]},"reference":[{"key":"2026042801401866604_j_forma-2022-0014_ref_001","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Bylinacute;ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi: 10.1007\/978-3-319-20615-8_17.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026042801401866604_j_forma-2022-0014_ref_002","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Bylinacute;ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026042801401866604_j_forma-2022-0014_ref_003","unstructured":"[3] Serge Lang. Algebra. Springer Verlag, 2002 (Revised Third Edition)."},{"key":"2026042801401866604_j_forma-2022-0014_ref_004","unstructured":"[4] Piotr Rudnicki. Little Bezout theorem (factor theorem). Formalized Mathematics, 12(1): 49\u201358, 2004."},{"key":"2026042801401866604_j_forma-2022-0014_ref_005","doi-asserted-by":"crossref","unstructured":"[5] Christoph Schwarzweller. On roots of polynomials over F [X]\/\u3008p\u3009. Formalized Mathematics, 27(2):93\u2013100, 2019. doi:10.2478\/forma-2019-0010.","DOI":"10.2478\/forma-2019-0010"},{"key":"2026042801401866604_j_forma-2022-0014_ref_006","doi-asserted-by":"crossref","unstructured":"[6] Christoph Schwarzweller. Field extensions and Kronecker\u2019s construction. Formalized Mathematics, 27(3):229\u2013235, 2019. doi:10.2478\/forma-2019-0022.","DOI":"10.2478\/forma-2019-0022"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2022-0014","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T13:39:45Z","timestamp":1777383585000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2022-0014"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,1]]},"references-count":6,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2022,12,30]]},"published-print":{"date-parts":[[2022,10,1]]}},"alternative-id":["10.2478\/forma-2022-0014"],"URL":"https:\/\/doi.org\/10.2478\/forma-2022-0014","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,1]]}}}