Representation Matters: An Unexpected Property of Polynomial Rings and its Consequences for Formalizing Abstract Field Theory

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^{\prime}$ , i.e. an isomorphic copy $F^{\prime}$ of $F$ , not satisfying this condition. As a consequence to $F^{\prime}$ 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 $\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.