@MISC{RING_EMB.MIZ,
  AUTHOR = {Watase, Yasushige},
  TITLE = {Embedding Principle for Rings and Abelian Groups},
  SECTION1 = {Preliminaries from Set Theory},
  SECTION2 = {Apply Embedding Principle to Rings},
  SECTION3 = {Apply Embedding Principle to Abelian Groups},
  SECTION4 = {Relation with Polynomial Rings},
  DAY = {21},
  MONTH = {November},
  YEAR = {2023},
  ADDRESS1 = {Suginami-ku Matsunoki 6, 3-21 Tokyo\\Japan},
  SUMMARY = {The article concerns about formalizing a certain lemma on embedding of algebraic
  structures in the Mizar System \cite{Mizar-State-2015}, along with the lemma appeared 
  in the book \cite{Zariski1975} at \S13 of Chapter 1. 
  The lemma claims that if a ring $A$ is embedded in a ring $B$ then there exists 
  a ring $C$ which is isomorphic to $B$ and includes $A$ as a subring. A basic idea 
  to prove the lemma is that for given monomorphism $\varphi$ from $A$ to $B$, one can 
  obtain such ring $C$ by introducing the addition and multiplication on the set 
  $(B \setminus \varphi(A)) \cup A$, while $B$ does not meet $A$. The same argument 
  has already been discussed and formalized in \cite{FIELD_2.ABS} in line with filed extension. \par
  We treat here a general case, namely the case of $B$ meets $A$, it is enough to create 
  a set $X$ which does not meet $A$ and $X \cong B \setminus \varphi(A)$ and construct a new 
  ring $C$ from the set $(X \cong B \setminus \varphi(A)) \cup A$. 
  The formalized lemma can be applied to the other algebraic structures such 
  as abelian groups as shown in the article as well with the same formulation of rings.\par
  We need the following 3 steps required for precise arguments and formalization to construct the 
  target object $C$:
  \begin{description} 
  \item{Step 1.} prepare a set $X$ which does not meet $A$ and isomorphic to 
   $B \setminus \varphi(A)$ as set-theoretical. The step is coded in Theorem 1 and 2;
  \item{Step 2.} make a $X \setminus S$ a ring as $C$, corresponds to Theorem 7 and 12 
    for rings and for Abelian groups, respectively;
  \item{Step 3.} construct an isomorphism $G: A \stackrel{\sim}{\longrightarrow} C$ such 
    that $\iota = G \circ \varphi$ is an identity mapping. 
   Corresponding formal counterparts are Theorem 9 and 14 for rings and for Abelian groups, respectively.
  \end{description}
  As a consequence of the principle, taking $\mathrm{\textbf{Polynom-Ring}}(A)$ as $B$, we have a 
   polynomial ring over $A$ with indeterminate $X$ and includes $A$ as a subring, say $A[X] = C$. 
  Here $\mathrm{\textbf{Polynom-Ring}}(A)$ is existing formalized ring of polynomials, which is 
  constructed by sequences. 
  An indeterminate $X$ is defined by the image of $(0,1,0,0,\cdots) \in \mathrm{\textbf{Polynom-Ring}}(A)$ 
  by the map $G$ of Step 3.},
  MSC2010 = {13B25 03B35},
  KEYWORDS = {Abelian group; ring; embedding}}

@BOOK{Zariski1975,
 AUTHOR={Zariski, Oscar and Samuel, Pierre},
 TITLE={Commutative Algebra {I}},
 edition={2nd},
 publisher={Springer},
 year={1975}}

@BOOK{Goto2011,
 AUTHOR={Goto, Shiro and Watanabe, Keiichi},
 TITLE={Commutative Ring Theory (Japanese)},
 PUBLISHER={NIPPON HYORON SHA CO., LTD.},
 YEAR=2011}} 
