{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T11:19:49Z","timestamp":1777461589527,"version":"3.51.4"},"reference-count":4,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T00:00:00Z","timestamp":1669852800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,12,1]]},"abstract":"Summary<\/jats:title>\n \n 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\u2019s classical one as presented by Lang in [3]. In the first part we proved 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 needed 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 , \u2026]\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 this 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-0022","type":"journal-article","created":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T12:23:12Z","timestamp":1676722992000},"page":"281-294","source":"Crossref","is-referenced-by-count":4,"title":["Existence and Uniqueness 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 Gda\u0144sk , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2023,2,18]]},"reference":[{"key":"2026042801384887992_j_forma-2022-0022_ref_001","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, 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":"2026042801384887992_j_forma-2022-0022_ref_002","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, 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":"2026042801384887992_j_forma-2022-0022_ref_003","unstructured":"[3] Serge Lang. Algebra. Springer Verlag, 2002 (Revised Third Edition)."},{"key":"2026042801384887992_j_forma-2022-0022_ref_004","doi-asserted-by":"crossref","unstructured":"[4] 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-0022","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T13:15:07Z","timestamp":1777382107000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2022-0022"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,1]]},"references-count":4,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2023,2,18]]},"published-print":{"date-parts":[[2022,12,1]]}},"alternative-id":["10.2478\/forma-2022-0022"],"URL":"https:\/\/doi.org\/10.2478\/forma-2022-0022","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,12,1]]}}}