Ring of Endomorphisms and Modules over a Ring
Yasushige Watase · Formalized Mathematics · 2022
Summary 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 → ρ R\mathop \to \limits^\rho 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 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, M ) ≅ M is given, where the ¯ R 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 , ρ ′) ≅ 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 AbGr in the article.