Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/9013
Tytuł: | Field Extensions and Kronecker’s Construction |
Autorzy: | Schwarzweller, Christoph |
Słowa kluczowe: | roots of polynomials field extensions Kronecker’s construction |
Data wydania: | 2019 |
Data dodania: | 16-kwi-2020 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 27, Issue 3, Pages 229–235 |
Abstrakt: | This is the fourth part of a four-article series containing a Mizar [3], [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 ∈ 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 the third part, this condition is not automatically true for arbitrary 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 this 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. |
Afiliacja: | Institute of Informatics, University of Gdansk, Poland |
URI: | http://hdl.handle.net/11320/9013 |
DOI: | 10.2478/forma-2019-0022 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
metadata.dc.identifier.orcid: | 0000-0001-9587-8737 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | http://creativecommons.org/licenses/by-sa/3.0/pl/ |
Występuje w kolekcji(ach): | Formalized Mathematics, 2019, Volume 27, Issue 3 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
forma_2019_27_3_0022.pdf | 263,99 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL