Ring of Endomorphisms and Modules over a Ring

We formalize in the Mizar system [3], [4] 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 [1] along with Ch. 2 set. 1 of [2]. 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. 1. The endomorphism ring of an abelian group denoted by End(M-ab).2. A pair of an Abelian group M-ab and a ring homomorphism R ->rho End (M-ab) determines a left R-module, formalized as a function AbGrLMod(M-ab, rho) in the article. 3. The set of all functions from M to N form R-module and denoted by Func_Mod(R)(M, N). 4. The set R-module homomorphisms of M to N, denoted by Hom(R)(M, N), forms R-module. 5. A formal proof of Hom(R)( (R) over bar, M) congruent to M is given, where the (R) over bar denotes the regular representation of R, i.e. we regard R itself as a left R-module. 6. A formal proof of AbGrLMod(M'(ab), rho ') congruent to M where M'(ab) is an abelian group obtained by removing the scalar multiplication from M, and rho ' is obtained by currying the scalar multiplication of M. The removal of the multiplication from M has been done by the forgettable functor defined as AbGr in the article.