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→ρ 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.