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 23
- Downloads 0
An Efficient Load Balancing Algorithms in Stream Processing With the Cloud Computing Environment
Fog personal computers is definitely correctly buzzword that is receiving, it provides firms zīmju base might be coming availability specialist knowledge. Impair price serve should you have of superiorities in studying t...
Adaptive Lighting System as a Smart Urban Object
In this article we present an approach to an adaptive lighting system as an intelligent object supporting urban space, especially for the elderly. This intelligent lighting system is used as an instrument to improve the...
A Survey on Advanced Approaches of EHR in inter-related data using Machine Learning
Medical data is being used for huge number of research works over the globe which is for predicting something novel case studies in each work. The current research which we are handling is on utilizing the EHR (Electroni...
Acoustic Model Training, using Kaldi, for Automatic Whispery Speech Recognition
The article presents research on the automatic whispery speech recognition. The main task was to find dependences between a number of triphone classes (number of leaves in decision tree) and the total number of Gaussian...
The Role of Computer Science and Software Technology in Organizing Universities for Industry 4.0 and Beyond
This paper analyzes the recent developments around Industry 4.0 and beyond, identifies the necessary organizational structures of universities to assist companies in their transition processes, defines the relevant sub-d...