<abstract xmlns="http://www.w3.org/1999/xhtml">

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: <italic>Mab </italic>for an Abelian group with a suffix “<italic>ab</italic>” and <italic>M</italic> without a suffix is used for left modules over a ring.
1. The endomorphism ring of an abelian group denoted by <bold>End</bold>(<italic>Mab</italic>).
2. A pair of an Abelian group <italic>Mab </italic>and a ring homomorphism <inline-formula>
<alternatives>
<inline-graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2022-0016_eq_001.png"></inline-graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"><mrow><mi>R</mi><mover><mo>→</mo><mi>ρ</mi></mover></mrow></math>
<tex-math>R\mathop \to \limits^\rho</tex-math>
</alternatives>
</inline-formula> <bold>End</bold> (<italic>Mab</italic>) determines a left <italic>R</italic>-module, formalized as a function <bold>AbGrLMod</bold>(<italic>Mab, ρ</italic>) in the article.
3. The set of all functions from <italic>M</italic> to <italic>N</italic> form <italic>R</italic>-module and denoted by <bold>Func_Mod</bold><italic>R</italic>(<italic>M, N</italic>).
4. The set <italic>R</italic>-module homomorphisms of <italic>M</italic> to <italic>N</italic>, denoted by <bold>Hom</bold><italic>R</italic>(<italic>M, N</italic>), forms <italic>R</italic>-module.
5. A formal proof of <bold>Hom</bold><italic>R</italic>(¯<italic>R, M</italic>) ≅<italic>M</italic> is given, where the ¯<italic>R</italic> denotes the regular representation of <italic>R</italic>, i.e. we regard <italic>R</italic> itself as a left <italic>R</italic>-module.
6. A formal proof of <bold>AbGrLMod</bold>(<italic>M</italic>′<italic>ab, ρ</italic>′) ≅ <italic>M</italic> where <italic>M</italic>′<italic>ab </italic>is an abelian group obtained by removing the scalar multiplication from <italic>M</italic>, and ρ′ is obtained by currying the scalar multiplication of <italic>M</italic>.
The removal of the multiplication from <italic>M</italic> has been done by the forgettable functor defined as <bold>AbGr</bold> in the article.
</abstract>

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: Mab 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(Mab).
2. A pair of an Abelian group Mab and a ring homomorphism 


R→ρ
R\mathop  \to \limits^\rho

 End (Mab) determines a left R-module, formalized as a function AbGrLMod(Mab, ρ) in the article.
3. The set of all functions from M to N form R-module and denoted by Func_ModR(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) ≅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.

Ring of Endomorphisms and Modules over a Ring

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"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...

Ring of Endomorphisms and Modules over a Ring

Publié en ligne: 30 déc. 2022

Pages: 211 - 221

Accepté: 30 sept. 2022

DOI: https://doi.org/10.2478/forma-2022-0016

Mots clés
module, endomorphism ring

© 2022 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Ring of Endomorphisms and Modules over a Ring

Publié en ligne: 30 déc. 2022

Pages: 211 - 221

Accepté: 30 sept. 2022

DOI: https://doi.org/10.2478/forma-2022-0016

Mots clésmodule, endomorphism ring

© 2022 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Mots clés
module, endomorphism ring