Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Category of Left Modules

**by****Michal Muzalewski**- Received December 12, 1991
- MML identifier: MODCAT_1

- [ Mizar article, MML identifier index ]

environ vocabulary CLASSES2, FUNCSDOM, VECTSP_2, MOD_2, CAT_1, MIDSP_1, GRCAT_1, ENS_1, INCSP_1, ORDINAL4, FUNCT_2, RELAT_1, PRE_TOPC, VECTSP_1, BOOLE, FUNCT_3, FUNCT_1, TARSKI, ARYTM_3, PARTFUN1, MODCAT_1, RLVECT_1, ALGSTR_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, RLVECT_1, VECTSP_1, FUNCSDOM, VECTSP_2, CAT_1, FRAENKEL, CLASSES2, PRE_TOPC, ALGSTR_1, GRCAT_1, MOD_2, FUNCT_3, MIDSP_1; constructors GRCAT_1, MOD_2, MIDSP_1, VECTSP_2, ALGSTR_1, MEMBERED, XBOOLE_0; clusters VECTSP_2, CAT_1, GRCAT_1, MOD_2, RELSET_1, STRUCT_0, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve x,y for set; reserve D for non empty set; reserve UN for Universe; reserve R for Ring; reserve G,H for LeftMod of R; :: :: 2. Domains of left modules :: definition let R; mode LeftMod_DOMAIN of R -> non empty set means :: MODCAT_1:def 1 for x being Element of it holds x is strict LeftMod of R; end; reserve V for LeftMod_DOMAIN of R; definition let R,V; redefine mode Element of V -> LeftMod of R; end; definition let R,V; cluster strict Element of V; end; definition let R; mode LModMorphism_DOMAIN of R -> non empty set means :: MODCAT_1:def 2 for x being Element of it holds x is strict LModMorphism of R; end; definition let R; let M be LModMorphism_DOMAIN of R; redefine mode Element of M -> LModMorphism of R; end; definition let R; let M be LModMorphism_DOMAIN of R; cluster strict Element of M; end; canceled 2; theorem :: MODCAT_1:3 for f being strict LModMorphism of R holds {f} is LModMorphism_DOMAIN of R; definition let R,G,H; mode LModMorphism_DOMAIN of G,H -> LModMorphism_DOMAIN of R means :: MODCAT_1:def 3 for x being Element of it holds x is strict Morphism of G,H; end; theorem :: MODCAT_1:4 D is LModMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H; theorem :: MODCAT_1:5 for f being strict Morphism of G,H holds {f} is LModMorphism_DOMAIN of G,H; definition let R,G,H; func Morphs(G,H) -> LModMorphism_DOMAIN of G,H means :: MODCAT_1:def 4 x in it iff x is strict Morphism of G,H; end; definition let R,G,H; let M be LModMorphism_DOMAIN of G,H; redefine mode Element of M -> Morphism of G,H; end; :: :: 4a. Category of left modules - objects :: definition let x,y,R; pred GO x,y,R means :: MODCAT_1:def 5 ex x1,x2 being set st x = [x1,x2] & ex G being strict LeftMod of R st y = G & x1 = the LoopStr of G & x2 = the lmult of G; end; theorem :: MODCAT_1:6 for x,y1,y2 being set st GO x,y1,R & GO x,y2,R holds y1 = y2; theorem :: MODCAT_1:7 for UN ex x st x in {[G,f] where G is Element of GroupObjects(UN), f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction} & GO x,TrivialLMod(R),R; definition let UN,R; func LModObjects(UN,R) -> set means :: MODCAT_1:def 6 for y holds y in it iff ex x st x in {[G,f] where G is Element of GroupObjects(UN), f is Element of Funcs([:the carrier of R,{{}}:],{{}}) : not contradiction} & GO x,y,R; end; theorem :: MODCAT_1:8 TrivialLMod(R) in LModObjects(UN,R); definition let UN,R; cluster LModObjects(UN,R) -> non empty; end; theorem :: MODCAT_1:9 for x being Element of LModObjects(UN,R) holds x is strict LeftMod of R; definition let UN,R; redefine func LModObjects(UN,R) -> LeftMod_DOMAIN of R; end; :: :: 4b. Category of left modules - morphisms :: definition let R,V; func Morphs(V) -> LModMorphism_DOMAIN of R means :: MODCAT_1:def 7 for x holds x in it iff ex G,H being strict Element of V st x is strict Morphism of G,H; end; :: :: 4c. Category of left modules - dom,cod,id :: definition let R,V; let F be Element of Morphs(V); func dom'(F) -> Element of V equals :: MODCAT_1:def 8 dom(F); func cod'(F) -> Element of V equals :: MODCAT_1:def 9 cod(F); end; definition let R,V; let G be Element of V; func ID(G) -> strict Element of Morphs(V) equals :: MODCAT_1:def 10 ID(G); end; definition let R,V; func dom(V) -> Function of Morphs(V),V means :: MODCAT_1:def 11 for f being Element of Morphs(V) holds it.f = dom'(f); func cod(V) -> Function of Morphs(V),V means :: MODCAT_1:def 12 for f being Element of Morphs(V) holds it.f = cod'(f); func ID(V) -> Function of V,Morphs(V) means :: MODCAT_1:def 13 for G being Element of V holds it.G = ID(G); end; :: :: 4d. Category of left modules - superposition :: theorem :: MODCAT_1:10 for g,f being Element of Morphs(V) st dom'(g) = cod'(f) ex G1,G2,G3 being strict Element of V st g is Morphism of G2,G3 & f is Morphism of G1,G2; theorem :: MODCAT_1:11 for g,f being Element of Morphs(V) st dom'(g) = cod'(f) holds g*f in Morphs(V); theorem :: MODCAT_1:12 for g,f being Element of Morphs(V) st dom(g) = cod(f) holds g*f in Morphs(V); definition let R,V; func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means :: MODCAT_1:def 14 (for g,f being Element of Morphs(V) holds [g,f] in dom it iff dom'(g) = cod'(f)) & (for g,f being Element of Morphs(V) st [g,f] in dom it holds it.[g,f] = g*f); end; theorem :: MODCAT_1:13 for g,f being Element of Morphs(V) holds [g,f] in dom comp(V) iff dom(g) = cod(f); :: :: 4e. Definition of Category of left modules :: definition let UN,R; func LModCat(UN,R) -> strict CatStr equals :: MODCAT_1:def 15 CatStr(#LModObjects(UN,R),Morphs(LModObjects(UN,R)), dom(LModObjects(UN,R)),cod(LModObjects(UN,R)), comp(LModObjects(UN,R)),ID(LModObjects(UN,R))#); end; theorem :: MODCAT_1:14 for f,g being Morphism of LModCat(UN,R) holds [g,f] in dom(the Comp of LModCat(UN,R)) iff dom g = cod f; theorem :: MODCAT_1:15 for f being (Morphism of LModCat(UN,R)), f' being Element of Morphs(LModObjects(UN,R)), b being Object of LModCat(UN,R), b' being Element of LModObjects(UN,R) holds f is strict Element of Morphs(LModObjects(UN,R)) & f' is Morphism of LModCat(UN,R) & b is strict Element of LModObjects(UN,R) & b' is Object of LModCat(UN,R); theorem :: MODCAT_1:16 for b being Object of LModCat(UN,R), b' being Element of LModObjects(UN,R) st b = b' holds id b = ID(b'); theorem :: MODCAT_1:17 for f being Morphism of LModCat(UN,R) for f' being Element of Morphs(LModObjects(UN,R)) st f = f' holds dom f = dom f' & cod f = cod f'; theorem :: MODCAT_1:18 for f,g being (Morphism of LModCat(UN,R)), f',g' being Element of Morphs(LModObjects(UN,R)) st f = f' & g = g' holds (dom g = cod f iff dom g' = cod f') & (dom g = cod f iff [g',f'] in dom comp(LModObjects(UN,R))) & (dom g = cod f implies g*f = g'*f') & (dom f = dom g iff dom f' = dom g') & (cod f = cod g iff cod f' = cod g'); definition let UN,R; cluster LModCat(UN,R) -> Category-like; end;

Back to top