:: Category of Left Modules :: by Micha{\l} Muzalewski :: :: Received December 12, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, CLASSES2, FUNCSDOM, VECTSP_2, SUBSET_1, STRUCT_0, MOD_2, MIDSP_1, CAT_1, GRCAT_1, FUNCT_2, ENS_1, RELAT_1, GRAPH_1, FUNCT_1, ALGSTR_0, VECTSP_1, ZFMISC_1, MCART_1, TARSKI, ARYTM_3, PARTFUN1, MODCAT_1, MSSUBFAM, UNIALG_1, MONOID_0, RELAT_2, BINOP_1, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, RELSET_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_5, STRUCT_0, ALGSTR_0, VECTSP_1, VECTSP_2, GRAPH_1, CAT_1, CLASSES2, GRCAT_1, MOD_2; constructors GRCAT_1, MOD_2, RELSET_1, FUNCT_5; registrations XBOOLE_0, RELSET_1, STRUCT_0, CAT_1, VECTSP_2, GRCAT_1, MOD_2; 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; registration let R,V; cluster strict for 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; registration let R; let M be LModMorphism_DOMAIN of R; cluster strict for Element of M; end; theorem :: MODCAT_1:1 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:2 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:3 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 for x being object holds 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 be object; let R; pred GO x,y,R means :: MODCAT_1:def 5 ex x1,x2 being object st x = [x1,x2] & ex G being strict LeftMod of R st y = G & x1 = the addLoopStr of G & x2 = the lmult of G; end; theorem :: MODCAT_1:4 for x,y1,y2 being object st GO x,y1,R & GO x,y2,R holds y1 = y2; theorem :: MODCAT_1:5 for UN ex x being object st x in the set of all [G,f] where G is Element of GroupObjects(UN) , f is Element of Funcs([:the carrier of R,{{}}:],{{}}) & GO x, TrivialLMod(R),R; definition let UN,R; func LModObjects(UN,R) -> set means :: MODCAT_1:def 6 for y being object holds y in it iff ex x st x in the set of all [G,f] where G is Element of GroupObjects(UN), f is Element of Funcs([:the carrier of R,the carrier of G:], the carrier of G) & GO x,y,R; end; theorem :: MODCAT_1:6 TrivialLMod(R) in LModObjects(UN,R); registration let UN,R; cluster LModObjects(UN,R) -> non empty; end; theorem :: MODCAT_1:7 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 being object 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); ::$CD end; :: :: 4d. Category of left modules - superposition :: theorem :: MODCAT_1:8 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:9 for g,f being Element of Morphs(V) st dom'(g) = cod'(f) holds g* f in Morphs(V); theorem :: MODCAT_1:10 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:11 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)) #); end; registration let UN,R; cluster LModCat(UN,R) -> non void non empty; end; theorem :: MODCAT_1:12 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; registration let UN,R; cluster -> strict for Element of Morphs LModObjects(UN,R); end; ::$CT 2 theorem :: MODCAT_1:15 for f being Morphism of LModCat(UN,R) for f9 being Element of Morphs(LModObjects(UN,R)) st f = f9 holds dom f = dom f9 & cod f = cod f9; theorem :: MODCAT_1:16 for f,g being (Morphism of LModCat(UN,R)), f9,g9 being Element of Morphs(LModObjects(UN,R)) st f = f9 & g = g9 holds (dom g = cod f iff dom g9 = cod f9) & (dom g = cod f iff [g9,f9] in dom comp(LModObjects(UN,R))) & (dom g = cod f implies g(*)f = g9*f9) & (dom f = dom g iff dom f9 = dom g9) & (cod f = cod g iff cod f9 = cod g9); registration let UN,R; cluster LModCat(UN,R) -> Category-like transitive associative reflexive; end;