@misc{FIELD_1.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {On Roots of Polynomials over K[X]/<p>},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {The polynomials $a \cdot x^n$},
      SECTION3 = {More on Homomorphisms},
      SECTION4 = {Lifting Homomorphisms from R to R[X]},
      SECTION5 = {Kronecker's Construction},
      DAY = {28},
      MONTH = {March},
      YEAR = {2019},
      SUMMARY = {This is the first part of a four-article series containing a Mizar formalization of Kronecker's construction
  about roots of polynomials in field extensions, i.e. that for every field $F$ and
  every polynomial $p \in F[X] \backslash F$ there exists a field extension $E$ of $F$ such
  that $p$ has a root over $E$. The formalization follows Kronecker's classical proof
  using $F[X]/\!\!<\!\!p\!\!>$ as the desired field extension $E$.\par
  In this first part we show that an irreducible polynomial $p \in F[X] \backslash F$ has a root
  over $F[X]/\!\!<\!\!p\!\!>$. Note, however, that this statement cannot be true in a rigid formal sense:
  We do not have $F \subseteq F[X]/\!\!<\!\!p\!\!>$ as sets, so $F$ is not a subfield of
  $F[X]/\!\!<\!\!p\!\!>$, and hence
  formally $p$ is not even a polynomial over $F[X]/\!\!<\!\!p\!\!>$. Consequently, we translate $p$
  along the canonical monomorphism $\phi : F \longrightarrow F[X]/\!\!<\!\!p\!\!>$ and show that the
  translated polynomial $\phi(p)$ has a root over $F[X]/\!\!<\!\!p\!\!>$.
  \par
  Because $F$ is not a subfield of $F[X]/\!\!<\!\!p\!\!>$ we construct in the second part the field
  $(E\, \backslash \, \phi(F)) \cup F$ for a given monomorphism $\phi : F \longrightarrow E$
  and show that this field both is isomorphic to $F$ and includes $F$ as a subfield.
  In the literature this part of the proof usually consists of saying that ``one can identify
  $F$ with its image $\phi(F)$ in $F[X]/\!\!<\!\!p\!\!>$ and therefore consider $F$ as a subfield of $F[X]/\!\!<\!\!p\!\!>$".
  Interestingly, to do so we need to assume that $F \cap E = \emptyset$, in particular
  Kronecker's construction can be formalized for fields $F$ with $F \cap F[X] = \emptyset$.
   \par
  Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields $F$:
  With the exception of $\mathbb{Z}_2$ we construct for every field $F$ an isomorphic copy $F'$ of $F$ with
  $F' \cap F'[X] \neq \emptyset$.
  We also prove that for Mizar's representations of $\mathbb{Z}_n$, $\mathbb{Q}$ and $\mathbb{R}$
  we have $\mathbb{Z}_n \cap \mathbb{Z}_n[X] = \emptyset$, $\mathbb{Q} \cap \mathbb{Q}[X] = \emptyset$
  and $\mathbb{R} \cap \mathbb{R}[X] = \emptyset$, respectively.
  \par
  In the fourth part we finally define field extensions: $E$ is a field extension of $F$
  iff $F$ is a subfield of $E$. Note, that in this case we have $F \subseteq E$ as sets, and thus a polynomial $p$ over $F$ is
  also a polynomial over $E$. We then apply the construction of the second part to $F[X]/\!\!<\!\!p\!\!>$
  with the canonical monomorphism $\phi : F \longrightarrow F[X]/\!\!<\!\!p\!\!>$.
  Together with the first part this gives -- for fields $F$ with $F \cap F[X] = \emptyset$ - a field extension $E$ of $F$
  in which $p \in F[X] \backslash F$ has a root.}}

@BOOK{HL99,
      AUTHOR = {H. L\"{u}neburg},
      TITLE = {Gruppen, Ringe, K\"{o}rper: Die grundlegenden Strukturen der Algebra},
      PUBLISHER = {Oldenbourg Verlag},
      YEAR = {1990}}

@BOOK{Rad89,
      AUTHOR = {Knut Radbruch},
      TITLE = {Algebra I},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

@BOOK{Jac85,
      AUTHOR = {Nathan Jacobson},
      TITLE = {Basic Algebra I},
      PUBLISHER = {Dover Books on Mathematics},
      YEAR = {1985}}
