@misc{FIELD_11.MIZ,
       AUTHOR = {Schwarzweller, Christoph},
        TITLE = {Artin's Theorem towards the Existence of Algebraic Closures},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      DAY = {30},
      MONTH = {September},
      YEAR = {2022},
      SUMMARY = {This is the first part of a two-part article formalizing existence and uniqueness
                 of algebraic closures. Our proof follows Artin's classical one as presented by
		Lang in \cite{Lan02}.
                 In this first part we prove that for a given field $F$ there exists a field
                 extension
                 $E$ such that every non-constant polynomial $p \in F[X]$ has a root in $E$.
                 Artin's
                 proof applies Kronecker's construction to each polynomial $p \in F[X] \backslash F$
                 simultaneously.
                 To do so we need the polynomial ring $F[X_1,X_2,...]$ with infinitely many
                 variables,
                 one for each polynomal $p \in F[X] \backslash F$. The desired field extension $E$
                 then
                 is $F[X_1,X_2,...] \backslash I$, where $I$ is a maximal ideal generated by all
                 non-constant
                 polynomials $p \in F[X]$. Note, that to show that $I$ is maximal Zorn's lemma has to be
                 applied.
                 In the second part this construction is iterated giving an infinite sequence of fields,
                 whose union establishes a field extension $A$ of $F$, in which every non-constant polynomial
                 $p \in A[X]$ has a root. The field of algebraic elements of $A$ then is an algebraic closure
                 of $F$.
                 To prove uniqueness of algebraic closures, e.g. that two algebraic closures of $F$ are
                 isomorphic over $F$, the technique of extending monomorphisms is applied: a monomorphism
                 $F \longrightarrow A$, where $A$ is an algebraic closure of $F$ can be extended to a
                 monomorphism $E \longrightarrow A$, where $E$ is any algebraic extension of $F$.
                 In case that
                 $E$ is algebraically closed this monomorphism is an isomorphism. Note that the
                 existence of
                 the extended monomorphism again relies on Zorn's lemma.}}

                 @BOOK{Lan02,
      AUTHOR = {Serge Lang},
      TITLE = {Algebra, {R}evised {T}hird {E}dition},
      PUBLISHER = {Springer Verlag},
      YEAR = {2002}}
