REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU

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: moduleendomorphism 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 RozmiarFormat