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

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 <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 needed 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 this 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 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.

Existence and Uniqueness of Algebraic Closures

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Existence and Uniqueness of Algebraic Closures"}

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...

Existence and Uniqueness of Algebraic Closures

Data publikacji: 18 lut 2023

Zakres stron: 281 - 294

Przyjęty: 27 gru 2022

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

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-NonCommercial-NoDerivatives 3.0 License.

Existence and Uniqueness of Algebraic Closures

Data publikacji: 18 lut 2023

Zakres stron: 281 - 294

Przyjęty: 27 gru 2022

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

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-NonCommercial-NoDerivatives 3.0 License.

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