1. bookVolume 29 (2021): Issue 3 (October 2021)
Journal Details
License
Format
Journal
eISSN
1898-9934
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English
access type Open Access

Splitting Fields

Published Online: 30 Dec 2021
Volume & Issue: Volume 29 (2021) - Issue 3 (October 2021)
Page range: 129 - 139
Accepted: 30 Jun 2021
Journal Details
License
Format
Journal
eISSN
1898-9934
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

Summary. In this article we further develop field theory in Mizar [1], [2]: we prove existence and uniqueness of splitting fields. We define the splitting field of a polynomial pF [X] as the smallest field extension of F, in which p splits into linear factors. From this follows, that for a splitting field E of p we have E = F (A) where A is the set of p’s roots. Splitting fields are unique, however, only up to isomorphisms; to be more precise up to F -isomorphims i.e. isomorphisms i with i|F = IdF. We prove that two splitting fields of pF [X] are F -isomorphic using the well-known technique [4], [3] of extending isomorphisms from F1F2 to F1(a) → F2(b) for a and b being algebraic over F1 and F2, respectively.

Keywords

MSC

Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.10.1007/s10817-017-9440-6604425130069070Search in Google Scholar

Adam Grabowski and Christoph Schwarzweller. Translating mathematical vernacular into knowledge repositories. In Michael Kohlhase, editor, Mathematical Knowledge Management, volume 3863 of Lecture Notes in Computer Science, pages 49–64. Springer, 2006. doi:https://doi.org/10.1007/11618027 4. 4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15–17, 2005, Revised Selected Papers.Search in Google Scholar

Serge Lang. Algebra. Springer Verlag, 2002 (Revised Third Edition).Search in Google Scholar

Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991.Search in Google Scholar

Christoph Schwarzweller. Field extensions and Kronecker’s construction. Formalized Mathematics, 27(3):229–235, 2019. doi:10.2478/forma-2019-0022.10.2478/forma-2019-0022Search in Google Scholar

Christoph Schwarzweller. Ring and field adjunctions, algebraic elements and minimal polynomials. Formalized Mathematics, 28(3):251–261, 2020. doi:10.2478/forma-2020-0022.10.2478/forma-2020-0022Search in Google Scholar

Christoph Schwarzweller, Artur Korniłowicz, and Agnieszka Rowińska-Schwarzweller. Some algebraic properties of polynomial rings. Formalized Mathematics, 24(3):227–237, 2016. doi:10.1515/forma-2016-0019.10.1515/forma-2016-0019Search in Google Scholar

Recommended articles from Trend MD

Plan your remote conference with Sciendo