On the intersection of fields F with F[X]

Christoph Schwarzweller


This is the third 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]/< p > as the desired field extension E [6], [4], [5]. In the first part we show that an irreducible polynomial p ∈ F[X]\F has a root over F[X]/< p >. Note, however, that this statement cannot be true in a rigid formal sense: We do not have F ⊆ F[X]/< p > as sets, so F is not a subfield of F[X]/< p >, and hence formally p is not even a polynomial over F[X]/< p >. Consequently, we translate p along the canonical monomorphism φ : F → F[X]/< p > and show that the translated polynomial φ(p) has a root over F[X]/< p >. Because F is not a subfield of F[X]/< p > 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]/< p > and therefore consider F as a subfield of F[X]/< p > ”. 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 this third part, this condition is not automatically true for arbitrary fields F: With the exception of Z2 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 Zn, Q and R we have Zn ∩ Zn[X] = ∅, Q ∩ Q[X] = ∅ and R ∩ R[X] = ∅, 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 ⊆ 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]/< p > with the canonical monomorphism φ : F → F[X]/< p >. 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.
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.5
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/3/article-p223.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, 04-03-2020, ArticleFromJournal
Publication indicators 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?