On Roots of Polynomials over F [ X ]/ 〈 p 〉
Christoph Schwarzweller · Formalized Mathematics · 2019
Summary 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.