@MISC{LMOD_XX1.MIZ,
  AUTHOR = {Watase, Yasushige},
  TITLE = {Ring of {E}ndomorphisms \& {M}odules over a {R}ing},
  SECTION1 = {The Endomorphism Ring of an Abelian Group},
  SECTION2 = {Abelian Group $M$ turns to be a Module over Ring $R$ by the Ring 
    of Endmorphism \& a Ringhomomorphism},
  SECTION3 = {The set of all $R$-module Homomorphisms of $M$,$N$ form $R$-Module},
  SECTION4 = {Formal proof of $Hom(R,M) \cong M$},
  SECTION5 = {Correspondence between Abelian Group and Left $R$-Module},
  DAY = {30},
  MONTH = {September},
  YEAR = {2022},
  ADDRESS1 = {Suginami-ku Matsunoki 6, 3-21 Tokyo\\Japan},
  SUMMARY = {We formalize in the Mizar System \cite{Mizar-State-2015} some basic properties on   left module over a ring such as constructing a module via a ring of endomorphism of an abelian   group and the set of all homomorphisms of modules form a module along with Ch.2 set.1 of 
   \cite{AM}. \par
  The formalized items are shown in the below list with notations: 
  $M_{ab}$ for an Abelian group with a suffix "$_{ab}"$ and $M$ 
  without a suffix is used for left modules over a ring.
  \begin{enumerate}
  \item the endomorphism ring of an abelian group denoted by $\mathrm{\textbf{End}}(M_{ab})$.,
  \item A pair of an ableian group $M_{ab}$ and a ring homomorphism $R \stackrel{\rho}{\to}   \mathrm{\textbf{End}}(M_{ab})$ determines a left $R$-module, formalized as a function $\mathrm  {\textbf{AbGrLMod}}(M_{ab},\rho)$ in the article.
  \item the set of all functions from $M$ to $N$ form $R$-module and denoted by $\mathrm{\textbf  {Func\_Mod}}_{R}(M,N)$, 
  \item the set $R$-module homomorphisms of $M$ to $N$, denoted by $\mathrm{\textbf{Hom}}_{R}  (M,N)$, forms $R$-module. 
  \item A formal proof of $\mathrm{\textbf{Hom}}_{R}(\bar{R},M) \cong M$ is given, where the $  \bar{R}$ denotes the regular representation of $R$, i.e. we regard $R$ itself as a left $R$-  module. 
  \item A formal proof of $\mathrm{\textbf{AbGrLMod}}(M^{\prime}_{ab},\rho^{\prime}) \cong M$   where $M^{\prime}_{ab}$ is an abelian group obtained by removing the scalar multiplication from   $M$, and $\rho^{\prime}$ is obtained by currying the scalar multiplication of $M$. 
  How to remove the multiplication from $M$ has been done by a kind forgettable funcotor defined   as $\mathrm{\textbf{AbGr}}$ in the article.},
  MSC2010 = {13C05 13C60},
  KEYWORDS = {Module; Endomorphism Ring}}

@BOOK{AM,
 AUTHOR={M.F. ATIYAH and I.G. MACDONALD},
 TITLE={Introduction to Commutative Algebra},
 PUBLISHER={Addison-Wesley Publishing Company, Inc.},
 YEAR=1969}

@BOOK{FAKF,
 AUTHOR={Frank W. Anderson and Kent R. Fuller},
 TITLE={Rings and Categories of Modules Second Edition},
 PUBLISHER={Springer-Verlag},
 YEAR=1992}
} 
