<abstract xmlns="http://www.w3.org/1999/xhtml">

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 <italic>F</italic> there exists a field extension <italic>E</italic> such that every non-constant polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>] has a root in <italic>E</italic>. Artin’s proof applies Kronecker’s construction to each polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> simultaneously. To do so we need the polynomial ring <italic>F</italic> [<italic>X</italic>1, <italic>X</italic>2, ...] with infinitely many variables, one for each polynomal <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> . The desired field extension <italic>E</italic> then is <italic>F</italic> [<italic>X</italic>1, <italic>X</italic>2, ...]<italic>\I</italic>, where <italic>I</italic> is a maximal ideal generated by all non-constant polynomials <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]. Note, that to show that <italic>I</italic> 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 <italic>A</italic> of <italic>F</italic>, in which every non-constant polynomial <italic>p</italic> ∈ <italic>A</italic>[<italic>X</italic>] has a root. The field of algebraic elements of <italic>A</italic> then is an algebraic closure of <italic>F</italic> . To prove uniqueness of algebraic closures, e.g. that two algebraic closures of <italic>F</italic> are isomorphic over <italic>F</italic>, the technique of extending monomorphisms is applied: a monomorphism <italic>F</italic> → <italic>A</italic>, where <italic>A</italic> is an algebraic closure of <italic>F</italic> can be extended to a monomorphism <italic>E</italic> → <italic>A</italic>, where <italic>E</italic> is any algebraic extension of <italic>F</italic> . In case that <italic>E</italic> is algebraically closed this monomorphism is an isomorphism. Note that the existence of the extended monomorphism again relies on Zorn’s lemma.
</abstract>

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.

Artin’s Theorem Towards the Existence of Algebraic Closures

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"Artin\u2019s Theorem Towards the Existence of Algebraic Closures"}

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 Theorem Towards the Existence of Algebraic Closures

Data publikacji: 30 gru 2022

Zakres stron: 199 - 207

Przyjęty: 30 wrz 2022

DOI: https://doi.org/10.2478/forma-2022-0014

Słowa kluczowe
algebraic closures, polynomial rings with countably infinite number of variables, Emil Artin

© 2022 Christoph Schwarzweller, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Artin’s Theorem Towards the Existence of Algebraic Closures

Data publikacji: 30 gru 2022

Zakres stron: 199 - 207

Przyjęty: 30 wrz 2022

DOI: https://doi.org/10.2478/forma-2022-0014

Słowa kluczowealgebraic closures, polynomial rings with countably infinite number of variables, Emil Artin

© 2022 Christoph Schwarzweller, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Słowa kluczowe
algebraic closures, polynomial rings with countably infinite number of variables, Emil Artin