Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/14675
Tytuł: | Ring of Endomorphisms and Modules over a Ring |
Autorzy: | Watase, Yasushige |
Słowa kluczowe: | module endomorphism ring |
Data wydania: | 2022 |
Data dodania: | 16-lut-2023 |
Wydawca: | DeGruyter Open |
Źródło: | Formalized Mathematics, Volume 30, Issue 3, Pages 211-221 |
Abstrakt: | 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. |
Afiliacja: | Suginami-ku Matsunoki, 3-21-6 Tokyo, Japan |
URI: | http://hdl.handle.net/11320/14675 |
DOI: | 10.2478/forma-2022-0016 |
ISSN: | 1426-2630 |
e-ISSN: | 1898-9934 |
Typ Dokumentu: | Article |
metadata.dc.rights.uri: | https://creativecommons.org/licenses/by-sa/3.0/ |
Właściciel praw: | © 2022 The Author(s) CC BY-SA 3.0 license |
Występuje w kolekcji(ach): | Formalized Mathematics, 2022, Volume 30, Issue 3 |
Pliki w tej pozycji:
Plik | Opis | Rozmiar | Format | |
---|---|---|---|---|
10.2478_forma-2022-0016.pdf | 272,81 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL