REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/8132
Tytuł: On Monomorphisms and Subfields
Autorzy: Schwarzweller, Christoph
Słowa kluczowe: roots of polynomials
field extensions
Kronecker’s construction
12E05
12F05
68T99
03B35
Data wydania: 2019
Data dodania: 29-lip-2019
Wydawca: DeGruyter Open
Źródło: Formalized Mathematics, Volume 27, Issue 2, Pages 133 - 137
Abstrakt: 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 ∈ 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 ∈ 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 this 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 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]/ 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.
Afiliacja: Institute of Informatics, University of Gdańsk, Poland
URI: http://hdl.handle.net/11320/8132
DOI: 10.2478/forma-2019-0014
ISSN: 1426-2630
e-ISSN: 1898-9934
metadata.dc.identifier.orcid: 0000-0001-9587-8737
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2019, Volume 27, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma_2019_27_2_005.pdf217,47 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons