<abstract xmlns="http://www.w3.org/1999/xhtml">This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field <italic>F</italic> and every polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> there exists a field extension <italic>E</italic> of <italic>F</italic> such that <italic>p</italic> has a root over <italic>E</italic>. The formalization follows Kronecker’s classical proof using <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic> as the desired field extension <italic>E</italic> [9], [4], [6].In this first part we show that an irreducible polynomial <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> has a root over <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic>. Note, however, that this statement cannot be true in a rigid formal sense: We do not have <italic>F</italic> ⊆ [<italic>X</italic>]<italic>/ &lt; p ></italic> as sets, so <italic>F</italic> is not a subfield of <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic>, and hence formally <italic>p</italic> is not even a polynomial over <italic>F</italic> [<italic>X</italic>]<italic>/ &lt; p ></italic>. Consequently, we translate <italic>p</italic> along the canonical monomorphism <italic>ϕ</italic>: <italic>F</italic> → <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic> and show that the translated polynomial <italic>ϕ</italic>(<italic>p</italic>) has a root over <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic>.Because <italic>F</italic> is not a subfield of <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic> we construct in the second part the field (<italic>E \ ϕF</italic> )∪<italic>F</italic> for a given monomorphism <italic>ϕ : F</italic> → <italic>E</italic> and show that this field both is isomorphic to <italic>F</italic> and includes <italic>F</italic> as a subfield. In the literature this part of the proof usually consists of saying that “one can identify <italic>F</italic> with its image <italic>ϕF</italic> in <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic> and therefore consider <italic>F</italic> as a subfield of <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic>”. Interestingly, to do so we need to assume that <italic>F ∩ E</italic> =∅, in particular Kronecker’s construction can be formalized for fields <italic>F</italic> with <italic>F \ F</italic> [<italic>X</italic>] =∅.Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields <italic>F</italic> : With the exception of 𝕑2 we construct for every field <italic>F</italic> an isomorphic copy <italic>F</italic>′ of <italic>F</italic> with <italic>F′</italic> ∩ <italic>F′</italic> [<italic>X</italic>] <italic>≠</italic>∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[<italic>X</italic>] = ∅, 𝕈 ∩ 𝕈[<italic>X</italic>] = ∅and 𝕉 ∩ 𝕉[<italic>X</italic>] = ∅, respectively.In the fourth part we finally define field extensions: <italic>E</italic> is a field extension of <italic>F</italic> i <italic>F</italic> is a subfield of <italic>E</italic>. Note, that in this case we have <italic>F ⊆ E</italic> as sets, and thus a polynomial <italic>p</italic> over <italic>F</italic> is also a polynomial over <italic>E</italic>. We then apply the construction of the second part to <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic> with the canonical monomorphism <italic>ϕ : F</italic> → <italic>F</italic> [<italic>X</italic>]<italic>/&lt;p></italic>. Together with the first part this gives - for fields <italic>F</italic> with <italic>F</italic> ∩ <italic>F</italic> [<italic>X</italic>] = ∅ - a field extension <italic>E</italic> of <italic>F</italic> in which <italic>p</italic> ∈ <italic>F</italic> [<italic>X</italic>]<italic>\F</italic> has a root.</abstract>

This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/ as the desired field extension E [9], [4], [6].In this first part we show that an irreducible polynomial p ∈ F [X]\F has a root over F [X]/. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/ as sets, so F is not a subfield of F [X]/, and hence formally p is not even a polynomial over F [X]/ . Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/ and show that the translated polynomial ϕ(p) has a root over F [X]/.Because F is not a subfield of F [X]/ we construct in the second part the field (E \ ϕF )∪F for a given monomorphism ϕ : F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/ and therefore consider F as a subfield of F [X]/”. Interestingly, to do so we need to assume that F ∩ E =∅, in particular Kronecker’s construction can be formalized for fields F with F \ F [X] =∅.Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈[X] = ∅and 𝕉 ∩ 𝕉[X] = ∅, respectively.In the fourth part we finally define field extensions: E is a field extension of F i F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/ with the canonical monomorphism ϕ : F → F [X]/. Together with the first part this gives - for fields F with F ∩ F [X] = ∅ - a field extension E of F in which p ∈ F [X]\F has a root.

On Roots of Polynomials over <italic>F</italic>[<italic>X</italic>]/ 〈<italic>p</italic>〉

Formalized Mathematics

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p ∈ F [X]\F there exists a field extension E of F such that p has a root over E. The formalization follows Kronecker’s classical proof using F [X]/ as the desired field extension E [9], [4], [6].In this first part we show that an irreducible polynomial p ∈ F [X]\F has a root over F [X]/. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ [X]/  as sets, so F is not a subfield of F [X]/, and hence formally p is not even a polynomial over F [X]/ . Consequently, we translate p along the canonical monomorphism ϕ: F → F [X]/ and show that the translated polynomial ϕ(p) has a root over F [X]/.Because F is not a subfield of F [X]/ we construct in the second part the field (E \ ϕF )∪F for a given monomorphism ϕ : F → E and show that this field both is isomorphic to F and includes F as a subfield. In the literature this part of the proof usually consists of saying that “one can identify F with its image ϕF in F [X]/ and therefore consider F as a subfield of F [X]/”. Interestingly, to do so we need to assume that F ∩ E =∅, in particular Kronecker’s construction can be formalized for fields F with F \ F [X] =∅.Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F : With the exception of 𝕑2 we construct for every field F an isomorphic copy F′ of F with F′ ∩ F′ [X] ≠∅. We also prove that for Mizar’s representations of 𝕑n, 𝕈 and 𝕉 we have 𝕑n ∩ 𝕑n[X] = ∅, 𝕈 ∩ 𝕈[X] = ∅and 𝕉 ∩ 𝕉[X] = ∅, respectively.In the fourth part we finally define field extensions: E is a field extension of F i F is a subfield of E. Note, that in this case we have F ⊆ E as sets, and thus a polynomial p over F is also a polynomial over E. We then apply the construction of the second part to F [X]/ with the canonical monomorphism ϕ : F → F [X]/. Together with the first part this gives - for fields F with F ∩ F [X] = ∅ - a field extension E of F in which p ∈ F [X]\F has a root.

This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field...

On Roots of Polynomials over F[X]/ 〈p〉

Data publikacji: 20 lip 2019

Zakres stron: 93 - 100

Przyjęty: 28 mar 2019

DOI: https://doi.org/10.2478/forma-2019-0010

Słowa kluczowe
roots of polynomials, field extensions, Kronecker’s construction

© 2019 Christoph Schwarzweller, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

On Roots of Polynomials over F[X]/ 〈p〉

Data publikacji: 20 lip 2019

Zakres stron: 93 - 100

Przyjęty: 28 mar 2019

DOI: https://doi.org/10.2478/forma-2019-0010

Słowa kluczoweroots of polynomials, field extensions, Kronecker’s construction

© 2019 Christoph Schwarzweller, published by Sciendo

This work is licensed under a Creative Commons Attribution Share-Alike 4.0 License.

Słowa kluczowe
roots of polynomials, field extensions, Kronecker’s construction