Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory
Christoph Schwarzweller · Annals of Computer Science and Information Systems · 2018
In this paper we develop a Mizar formalization of Kronecker's construction, which states that for every field F and irreducible polynomial p ∈ 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 ∩ F [X] = ∅.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 Kronecker's construction cannot be applied.All proofs have been carried out in the Mizar system.Based on Mizar's representation of the fields Zp, Q and R we also have proven that Zp ∩ Zp[X] = ∅, Q ∩ Q[X] = ∅, and R ∩ R[X] = ∅ respectively.