On monomorphisms and subfields

Christoph Schwarzweller


This is the second part of a four-article series containing a Mizar [2], [1] 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 [5], [3], [4]. 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.
Author Christoph Schwarzweller (FMPI/II)
Christoph Schwarzweller,,
- Institute of Informatics
Journal seriesFormalized Mathematics, ISSN 1426-2630, e-ISSN 1898-9934, (N/A 20 pkt, Not active)
Issue year2019
Publication size in sheets0.50
Keywords in Englishroots of polynomials, field extensions, Kronecker’s construction
ASJC Classification2604 Applied Mathematics; 2605 Computational Mathematics
URL https://content.sciendo.com/downloadpdf/journals/forma/27/2/article-p133.xml
Languageen angielski
LicenseJournal (articles only); published final; Uznanie Autorstwa - Na Tych Samych Warunkach (CC-BY-SA); with publication
Score (nominal)20
Score sourcejournalList
ScoreMinisterial score = 20.0, 16-07-2020, ArticleFromJournal
Publication indicators WoS Citations = 0.000; Scopus SNIP (Source Normalised Impact per Paper): 2018 = 0.169
Citation count*
Share Share

Get link to the record

* presented citation count is obtained through Internet information analysis and it is close to the number calculated by the Publish or Perish system.
Are you sure?