Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory
Journal Title: Annals of Computer Science and Information Systems - Year 2018, Vol 15, Issue
Abstract
In this paper we develop a Mizar formalization of Kronecker's construction, which states that for every field $F$ and irreducible polynomial $p \in F[X]$ there exists a field extension $E$ of $F$ such that $p$ has a root over $E$. It turns out that to prove the correctness of the construction the field $F$ needs to provide a disjointness condition, namely $F \cap F[X] = \emptyset$. Surprisingly this property does not hold for arbitrary representations of a field $F$: We construct for almost every field $F$ another representation $F'$, i.e. an isomorphic copy $F'$ of $F$, not satisfying this condition. As a consequence to $F'$ our formalization of Kro\-necker's construction cannot be applied. All proofs have been carried out in the Mizar system. Based on Mizar's representation of the fields $\mathbb{Z}\_p, \mathbb{Q}$ and $\mathbb{R}$ we also have proven that $\mathbb{Z}\_p \cap \mathbb{Z}\_p[X] = \emptyset$, $\mathbb{Q} \cap \mathbb{Q}[X] = \emptyset$, and $\mathbb{R} \cap \mathbb{R}[X] = \emptyset$ respectively.
Authors and Affiliations
Christoph Schwarzweller
Keywords
Related Articles
- EP ID EP569795
- DOI 10.15439/2018F88
- Views 33
- Downloads 0
Unintended effects of dependencies in source code on the flexibility of IT in organizations
This study links business requirements and adaptability of existing software systems. Organizations expect flexibility of IT with regard to business requirements. We hypothesize that the flexibility of business requireme...
"Passeport Vacances": an assignment problem with cost balancing
asseport Vacances is an offer for school-aged children to discover a set of activities during holidays. For more than 30 years, it has been an established social function in several countries, including Germany and Switz...
Business Process Management: Terms, Trends and Models
Business Process Management (BPM) is a subject that is becoming a growing trend in the fields of Business Administration, Engineering, Information Technology (IT), among others. Understanding the subject is a complex and...
Data quality evaluation: a comparative analysis of company registers’ open data in four European countries
This paper is devoted to the analysis of open data quality of the company registers in four different countries. The data quality evaluation was obtained using a methodology that involves the creation of three-part data...
A Detailed Study of EEG based Brain Computer Interface
Brain Computer Interface (BCI) generate a direct method to communicate with the outside world. Many patients are not able to communicate. For example:- the patient who are suffered with the several disease like post stro...