On monomorphisms and subfields
AbstractThis is the second part of a four-article series containing a Mizar ,  formalization of Kronecker's construction about roots of polynomials in field extensions, i.e. that for every field F and every polynomial p is an element of 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 , , . In the first part we show that an irreducible polynomial p is an element of 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 subset of 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 phi : F -> F[X]/ and show that the translated polynomial phi(p) has a root over F[X]/ . Because F is not a subfield of F[X]/ we construct in this second part the field (E\phi F)boolean OR F for a given monomorphism phi : 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 phi F in F[X]/ and therefore consider F as a subfield of F[X]/ ". Interestingly, to do so we need to assume that F boolean AND E = empty set, in particular Kronecker's construction can be formalized for fields F with F boolean AND F[X] = empty set. Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields F: With the exception of Z(2) we construct for every field F an isomorphic copy F' of F with F' boolean AND F'[X] not equal empty set. We also prove that for Mizar's representations of Z(n), Q and R we have Z(n) boolean AND Z(n)[x] = empty set, Q boolean AND Q[X] = empty set and R boolean AND R[X] = empty set, respectively. In the fourth part we finally define field extensions: E is a field extension of F iff F is a subfield of E. Note, that in this case we have F subset of 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 phi : F -> F[X]/ . Together with the first part this gives - for fields F with F boolean AND F[X] = empty set - a field extension E of F in which p is an element of F[X]\F has a root.
|Journal series||Formalized Mathematics, ISSN 1426-2630, e-ISSN 1898-9934, (N/A 20 pkt, Not active)|
|Publication size in sheets||0.50|
|Keywords in English||roots of polynomials, field extensions, Kronecker’s construction|
|License||Journal (articles only); published final; ; with publication|
|Score||= 20.0, 16-07-2020, ArticleFromJournal|
|Publication indicators||= 0.000; : 2018 = 0.169|
* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.