Ring of Endomorphisms and Modules over a Ring

Abstract

We formalize in the Mizar system [3], [4] some basic propertieson left module over a ring such as constructing a module via a ring of endomor-phism of an abelian group and the set of all homomorphisms of modules form amodule [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ρ→End (M ab) determines a left R-module, formalized as a function AbGrLMod(M ab,ρ) in the article. 3. The set of all functions from MtoNformR-module and denoted by FuncModR(M,N). 4. The set R-module homomorphisms of M to N, denoted by HomR (M,N),forms R-module. 5. A formal proof of HomR( ̄R,M)∼=Mis given, where the ̄Rdenotes theregular representation of R, i.e. we regard R it self as a left R-module. 6. A formal proof of AbGrLMod(M′ab,ρ′)∼=M where M′ab is an abelian group obtained by removing the scalar multiplication from M, and ρ′ 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 AbGrin the article.