# Annals of Computer Science and Information Systems, Volume 15

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

### Christoph Schwarzweller

Citation: Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 15, pages 6772 ()

Full text

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.

### References

1. G. Bancerek, Tarski’s Classes and Ranks. Formalized Mathematics 1(3), 563–567, 1990.
2. G. Bancerek, Arithmetic of Non Negative Rational Numbers. Mizar Mathematical Library, 1998.
3. G. Bancerek et.al., Mizar: State-of-the-art and Beyond. in: M. Kerber et.al. (eds.), Proceedings of the 2015 International Conference on Intelligent Computer Mathematics, Lecture Notes in Computer Science 9150, 261–279, 2015. http://dx.doi.org/10.1007/978-3-319-20615-8_17
4. The Coq Proof Assistant. available at www.coq.inria.fr.
5. H.B. Enderton, Elements of Set Theory. Elsevier, 1977.
6. Y. Futa, H. Okazaki, and Y. Shidama, Set of Points on Elliptic Curve in Projective Coordinates. Formalized Mathematics 19(3), 131–138, 2011. http://dx.doi.org/10.2478/v10037-011-0021-6
7. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Mizar in a Nutshell. Journal of Formalized Reasoning 3(2), 153–245, 2010. https://doi.org/10.6092/issn.1972-5787/1980
8. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, Equality in Computer Proof-Assistants. in: Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds.), ACSIS, Vol. 5, 45–54, 2015. http://dx.doi.org/10.15439/2015F229
9. A. Grabowski, A. Korniłowicz, and C. Schwarzweller, On Algebraic Hierarchies in Mathematical Repository of Mizar. in: Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 8, 363–371, 2016. http://dx.doi.org/10.15439/2016F520
10. A. Grabowski and C. Schwarzweller, Translating Mathematical Vernacular into Knowledge Repositories. in: M. Kohlhase (ed.), Proceedings of the 4th International Conference on Mathematical Knowledge Management, Lecture Notes in Artificial Intelligence, 3863, 49–64, Springer Verlag, 2006.
11. A. Grabowski and C. Schwarzweller, On Duplication in Mathematical Repositories. in: S. Autexier et.al. (eds.), Intelligent Computer Mathematics, Lecture Notes in Artificial Intelligence, 6167, 300-314, Springer Verlag, 2010.
12. A. Grabowski, A. Korniłowicz, and A. Naumowicz, Four Decades of Mizar. Journal of Automated Reasoning, vol 55(3), 191–198, 2015. http://dx.doi.org/10.1007/s10817-015-9345-1
13. J. Harrison, The HOL Light Theorem Prover. available at http://www.cl.cam.ac.uk/~jrh13/hol-light.
14. The HOL Interactive Theorem Prover. available at hol-theorem-prover. org.
15. Isabelle. available at isabelle.in.tum.de.
16. A. Korniłowicz, Quotient Rings. Formalized Mathematics 13(4), 573–576, 2005.