Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

### The abstract of the Mizar article:

### Categories of Groups

**by****Michal Muzalewski**- Received October 3, 1991
- MML identifier: GRCAT_1

- [ Mizar article, MML identifier index ]

environ vocabulary CLASSES2, PARTFUN1, RELAT_1, FUNCT_1, MIDSP_1, BOOLE, VECTSP_2, FUNCT_2, VECTSP_1, MIDSP_2, RLVECT_1, ARYTM_1, CAT_1, TARSKI, CAT_2, PRE_TOPC, ORDINAL4, FUNCOP_1, MOD_1, ENS_1, GRCAT_1, ALGSTR_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MOD_1, RELAT_1, FUNCT_1, MCART_1, STRUCT_0, BINOP_1, RLVECT_1, VECTSP_1, VECTSP_2, PARTFUN1, CAT_1, CLASSES2, PRE_TOPC, FUNCT_2, CAT_2, ALGSTR_1, MIDSP_1, MIDSP_2; constructors BINOP_1, VECTSP_2, CLASSES2, CAT_2, MIDSP_2, TOPS_2, ALGSTR_1, CLASSES1, MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0; clusters RELSET_1, GROUP_1, STRUCT_0, SUBSET_1, CLASSES2, ALGSTR_1, MIDSP_2, MEMBERED, ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0; requirements SUBSET, BOOLE; begin :: 0a. Auxiliary theorems: sets and universums reserve x, y for set; reserve D for non empty set; reserve UN for Universe; canceled; theorem :: GRCAT_1:2 for X,Y,A being set, z being set st z in A & A c= [:X,Y:] ex x being Element of X, y being Element of Y st z = [x,y]; theorem :: GRCAT_1:3 for u1,u2,u3,u4 being Element of UN holds [u1,u2,u3] is Element of UN & [u1,u2,u3,u4] is Element of UN; theorem :: GRCAT_1:4 for x,y st x in y & y in UN holds x in UN; :: 0b. Auxiliary schemes: partial functions scheme PartLambda2{X,Y,Z()->set,F(set,set)->set,P[set,set]}: ex f being PartFunc of [:X(),Y():],Z() st (for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y]) & (for x,y st [x,y] in dom f holds f.[x,y] = F(x,y)) provided for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z(); scheme PartLambda2D{X,Y()->non empty set,Z()->set,F(set,set)->set, P[set,set]}: ex f being PartFunc of [:X(),Y():],Z() st (for x being Element of X(), y being Element of Y() holds [x,y] in dom f iff P[x,y]) & (for x being Element of X(), y being Element of Y() st [x,y] in dom f holds f.[x,y] = F(x,y)) provided for x being Element of X(), y being Element of Y() st P[x,y] holds F(x,y) in Z(); :: 0c. Auxiliary theorems: Trivial Group theorem :: GRCAT_1:5 op2.({},{}) = {} & op1.{} = {} & op0 = {}; theorem :: GRCAT_1:6 {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN; theorem :: GRCAT_1:7 LoopStr (# {{}},op2,Extract {} #) is midpoint_operator; definition cluster L_Trivial -> midpoint_operator; end; theorem :: GRCAT_1:8 (for x being Element of L_Trivial holds x = {}) & (for x,y being Element of L_Trivial holds x+y = {}) & (for x being Element of L_Trivial holds -x = {}) & 0.L_Trivial = {}; :: 0d. Auxiliary theorems: subcategories reserve C for Category; reserve O for non empty Subset of the Objects of C; definition let C,O; canceled 4; func Morphs(O) -> Subset of the Morphisms of C equals :: GRCAT_1:def 5 union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O}; end; definition let C,O; cluster Morphs(O) -> non empty; end; definition let C,O; func dom(O) -> Function of Morphs(O),O equals :: GRCAT_1:def 6 (the Dom of C)|Morphs(O); func cod(O) -> Function of Morphs(O),O equals :: GRCAT_1:def 7 (the Cod of C)|Morphs(O); func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals :: GRCAT_1:def 8 (the Comp of C)|([:Morphs(O),Morphs(O):] qua set); func ID(O) -> Function of O,Morphs(O) equals :: GRCAT_1:def 9 (the Id of C)|O; end; theorem :: GRCAT_1:9 CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) is_full_subcategory_of C; definition let C,O; func cat(O) -> Subcategory of C equals :: GRCAT_1:def 10 CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#); end; definition let C,O; cluster cat(O) -> strict; end; theorem :: GRCAT_1:10 the Objects of cat(O) = O; :: 1a. Maps of the carriers of groups definition let G be 1-sorted; func id G -> map of G,G equals :: GRCAT_1:def 11 id the carrier of G; end; theorem :: GRCAT_1:11 for G being non empty 1-sorted, x being Element of G holds (id G).x = x; theorem :: GRCAT_1:12 for G being 1-sorted, H being non empty 1-sorted, f being map of G, H holds f*(id G) = f & (id H)*f = f; definition let G,H be non empty ZeroStr; func ZeroMap(G,H) -> map of G,H equals :: GRCAT_1:def 12 (the carrier of G) --> 0.H; end; definition let G,H be non empty LoopStr; let f be map of G,H; attr f is additive means :: GRCAT_1:def 13 for x,y being Element of G holds f.(x+y) = f.x+f.y; end; theorem :: GRCAT_1:13 comp L_Trivial = op1; theorem :: GRCAT_1:14 for G1,G2,G3 being non empty LoopStr, f being map of G1,G2, g being map of G2,G3 st f is additive & g is additive holds g*f is additive; theorem :: GRCAT_1:15 for G being non empty ZeroStr, H being non empty LoopStr, x being Element of G holds ZeroMap(G,H).x = 0.H; theorem :: GRCAT_1:16 for G being non empty LoopStr, H being right_zeroed (non empty LoopStr) holds ZeroMap(G,H) is additive; :: 1b. Morphisms of groups reserve G,H for AddGroup; definition struct GroupMorphismStr (# Dom,Cod -> AddGroup, Fun -> map of the Dom, the Cod #); end; definition let f be GroupMorphismStr; func dom(f) -> AddGroup equals :: GRCAT_1:def 14 the Dom of f; func cod(f) -> AddGroup equals :: GRCAT_1:def 15 the Cod of f; end; definition let f be GroupMorphismStr; func fun(f) -> map of dom(f),cod(f) equals :: GRCAT_1:def 16 the Fun of f; end; theorem :: GRCAT_1:17 for f being GroupMorphismStr, G1,G2 being AddGroup, f0 being map of G1,G2 st f = GroupMorphismStr(# G1,G2,f0#) holds dom f = G1 & cod f = G2 & fun f = f0; definition let G,H; func ZERO(G,H) -> GroupMorphismStr equals :: GRCAT_1:def 17 GroupMorphismStr(# G,H,ZeroMap(G,H)#); end; definition let G,H; cluster ZERO(G,H) -> strict; end; definition let IT be GroupMorphismStr; attr IT is GroupMorphism-like means :: GRCAT_1:def 18 fun(IT) is additive; end; definition cluster strict GroupMorphism-like GroupMorphismStr; end; definition mode GroupMorphism is GroupMorphism-like GroupMorphismStr; end; theorem :: GRCAT_1:18 for F being GroupMorphism holds the Fun of F is additive; definition let G,H; cluster ZERO(G,H) -> GroupMorphism-like; end; definition let G,H; mode Morphism of G,H -> GroupMorphism means :: GRCAT_1:def 19 dom(it) = G & cod(it) = H; end; definition let G,H; cluster strict Morphism of G,H; end; theorem :: GRCAT_1:19 for f being strict GroupMorphismStr st dom(f) = G & cod(f) = H & fun(f) is additive holds f is strict Morphism of G,H; theorem :: GRCAT_1:20 for f being map of G,H st f is additive holds GroupMorphismStr (# G,H,f#) is strict Morphism of G,H; theorem :: GRCAT_1:21 for G being non empty LoopStr holds id G is additive; definition let G; func ID G -> Morphism of G,G equals :: GRCAT_1:def 20 GroupMorphismStr(# G,G,id G#); end; definition let G; cluster ID G -> strict; end; definition let G,H; redefine func ZERO(G,H) -> strict Morphism of G,H; end; theorem :: GRCAT_1:22 for F being Morphism of G,H ex f being map of G,H st the GroupMorphismStr of F = GroupMorphismStr(# G,H,f#) & f is additive; theorem :: GRCAT_1:23 for F being strict Morphism of G,H ex f being map of G,H st F = GroupMorphismStr(# G,H,f#); theorem :: GRCAT_1:24 for F being GroupMorphism ex G,H st F is Morphism of G,H; theorem :: GRCAT_1:25 for F being strict GroupMorphism ex G,H being AddGroup, f being map of G,H st F is Morphism of G,H & F = GroupMorphismStr(# G,H,f#) & f is additive; theorem :: GRCAT_1:26 for g,f being GroupMorphism st dom(g) = cod(f) ex G1,G2,G3 being AddGroup st g is Morphism of G2,G3 & f is Morphism of G1,G2; definition let G,F be GroupMorphism; assume dom(G) = cod(F); func G*F -> strict GroupMorphism means :: GRCAT_1:def 21 for G1,G2,G3 being AddGroup, g being map of G2,G3, f being map of G1,G2 st the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) & the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#) holds it = GroupMorphismStr(# G1,G3,g*f#); end; canceled; theorem :: GRCAT_1:28 for G1,G2,G3 being AddGroup, G being Morphism of G2,G3, F being Morphism of G1,G2 holds G*F is Morphism of G1,G3; definition let G1,G2,G3 be AddGroup, G be Morphism of G2,G3, F be Morphism of G1,G2; redefine func G*F -> strict Morphism of G1,G3; end; theorem :: GRCAT_1:29 for G1,G2,G3 being AddGroup, G being Morphism of G2,G3, F being Morphism of G1,G2, g being map of G2,G3, f being map of G1,G2 st G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#) holds G*F = GroupMorphismStr(# G1,G3,g*f#); theorem :: GRCAT_1:30 for f,g being strict GroupMorphism st dom g = cod f holds ex G1,G2,G3 being AddGroup, f0 being map of G1,G2, g0 being map of G2,G3 st f = GroupMorphismStr(# G1,G2,f0#) & g = GroupMorphismStr(# G2,G3,g0#) & g*f = GroupMorphismStr(# G1,G3,g0*f0#); theorem :: GRCAT_1:31 for f,g being strict GroupMorphism st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g; theorem :: GRCAT_1:32 for G1,G2,G3,G4 being AddGroup, f being strict Morphism of G1,G2, g being strict Morphism of G2,G3, h being strict Morphism of G3,G4 holds h*(g*f) = (h*g)*f; theorem :: GRCAT_1:33 for f,g,h being strict GroupMorphism st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f; theorem :: GRCAT_1:34 dom ID(G) = G & cod ID(G) = G & (for f being strict GroupMorphism st cod f = G holds (ID G)*f = f) & (for g being strict GroupMorphism st dom g = G holds g*(ID G) = g); :: 2. Domains of groups definition let IT be set; attr IT is Group_DOMAIN-like means :: GRCAT_1:def 22 for x being set st x in IT holds x is strict AddGroup; end; definition cluster Group_DOMAIN-like non empty set; end; definition mode Group_DOMAIN is Group_DOMAIN-like non empty set; end; reserve V for Group_DOMAIN; definition let V; redefine mode Element of V -> AddGroup; end; definition let V; cluster strict Element of V; end; :: 3. Domains of morphisms definition let IT be set; attr IT is GroupMorphism_DOMAIN-like means :: GRCAT_1:def 23 for x being set st x in IT holds x is strict GroupMorphism; end; definition cluster GroupMorphism_DOMAIN-like non empty set; end; definition mode GroupMorphism_DOMAIN is GroupMorphism_DOMAIN-like non empty set; end; definition let M be GroupMorphism_DOMAIN; redefine mode Element of M -> GroupMorphism; end; definition let M be GroupMorphism_DOMAIN; cluster strict Element of M; end; canceled 2; theorem :: GRCAT_1:37 for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN; definition let G,H; mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means :: GRCAT_1:def 24 for x being Element of it holds x is strict Morphism of G,H; end; theorem :: GRCAT_1:38 D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H; theorem :: GRCAT_1:39 for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H; definition let G,H be 1-sorted; mode MapsSet of G,H means :: GRCAT_1:def 25 for x being set st x in it holds x is map of G,H; end; definition let G,H be 1-sorted; func Maps(G,H) -> MapsSet of G,H equals :: GRCAT_1:def 26 Funcs(the carrier of G, the carrier of H); end; definition let G be 1-sorted, H be non empty 1-sorted; cluster Maps(G,H) -> non empty; end; definition let G be 1-sorted, H be non empty 1-sorted; cluster non empty MapsSet of G,H; end; definition let G be 1-sorted, H be non empty 1-sorted; let M be non empty MapsSet of G,H; redefine mode Element of M -> map of G,H; end; definition let G,H; func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means :: GRCAT_1:def 27 x in it iff x is strict Morphism of G,H; end; definition let G,H; let M be GroupMorphism_DOMAIN of G,H; redefine mode Element of M -> Morphism of G,H; end; definition let G,H; let M be GroupMorphism_DOMAIN of G,H; cluster strict Element of M; end; :: 4a. Category of groups - objects definition let x,y; pred GO x,y means :: GRCAT_1:def 28 ex x1,x2,x3,x4 being set st x = [x1,x2,x3,x4] & ex G being strict AddGroup st y = G & x1 = the carrier of G & x2 = the add of G & x3 = comp G & x4 = the Zero of G; end; theorem :: GRCAT_1:40 for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2; theorem :: GRCAT_1:41 ex x st x in UN & GO x,L_Trivial; definition let UN; func GroupObjects(UN) -> set means :: GRCAT_1:def 29 for y holds y in it iff ex x st x in UN & GO x,y; end; theorem :: GRCAT_1:42 L_Trivial in GroupObjects(UN); definition let UN; cluster GroupObjects(UN) -> non empty; end; theorem :: GRCAT_1:43 for x being Element of GroupObjects(UN) holds x is strict AddGroup; definition let UN; cluster GroupObjects(UN) -> Group_DOMAIN-like; end; :: 4b. Category of groups - morphisms definition let V; func Morphs(V) -> GroupMorphism_DOMAIN means :: GRCAT_1:def 30 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 groups - dom,cod,id :: definition let V; let F be Element of Morphs(V); redefine func dom(F) -> strict Element of V; func cod(F) -> strict Element of V; end; definition let V; let G be Element of V; func ID(G) -> strict Element of Morphs(V) equals :: GRCAT_1:def 31 ID(G); end; definition let V; func dom(V) -> Function of Morphs(V),V means :: GRCAT_1:def 32 for f being Element of Morphs(V) holds it.f = dom(f); func cod(V) -> Function of Morphs(V),V means :: GRCAT_1:def 33 for f being Element of Morphs(V) holds it.f = cod(f); func ID(V) -> Function of V,Morphs(V) means :: GRCAT_1:def 34 for G being Element of V holds it.G = ID(G); end; :: :: 4d. Category of groups - superposition :: theorem :: GRCAT_1:44 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 :: GRCAT_1:45 for g,f being Element of Morphs(V) st dom(g) = cod(f) holds g*f in Morphs(V); definition let V; func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means :: GRCAT_1:def 35 (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; :: :: 4e. Definition of Category of groups :: definition let UN; func GroupCat(UN) -> CatStr equals :: GRCAT_1:def 36 CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp(GroupObjects(UN)),ID(GroupObjects(UN))#); end; definition let UN; cluster GroupCat(UN) -> strict; end; theorem :: GRCAT_1:46 for f,g being Morphism of GroupCat(UN) holds [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f; theorem :: GRCAT_1:47 for f being (Morphism of GroupCat(UN)), f' being Element of Morphs(GroupObjects(UN)), b being Object of GroupCat(UN), b' being Element of GroupObjects(UN) holds f is strict Element of Morphs(GroupObjects(UN)) & f' is Morphism of GroupCat(UN) & b is strict Element of GroupObjects(UN) & b' is Object of GroupCat(UN); theorem :: GRCAT_1:48 for b being Object of GroupCat(UN), b' being Element of GroupObjects(UN) st b = b' holds id b = ID(b'); theorem :: GRCAT_1:49 for f being Morphism of GroupCat(UN) for f' being Element of Morphs(GroupObjects(UN)) st f = f' holds dom f = dom f' & cod f = cod f'; theorem :: GRCAT_1:50 for f,g being (Morphism of GroupCat(UN)), f',g' being Element of Morphs(GroupObjects(UN)) 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(GroupObjects(UN))) & (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; cluster GroupCat(UN) -> Category-like; end; definition let UN; func AbGroupObjects(UN) -> Subset of the Objects of GroupCat(UN) equals :: GRCAT_1:def 37 {G where G is Element of the Objects of GroupCat(UN) : ex H being AbGroup st G = H}; end; theorem :: GRCAT_1:51 L_Trivial in AbGroupObjects(UN); definition let UN; cluster AbGroupObjects(UN) -> non empty; end; definition let UN; func AbGroupCat(UN) -> Subcategory of GroupCat(UN) equals :: GRCAT_1:def 38 cat(AbGroupObjects(UN)); end; definition let UN; cluster AbGroupCat(UN) -> strict; end; theorem :: GRCAT_1:52 the Objects of AbGroupCat(UN) = AbGroupObjects(UN); :: 6. Subcategory of groups with the operator of 1/2 definition let UN; func MidOpGroupObjects(UN) -> Subset of the Objects of AbGroupCat(UN) equals :: GRCAT_1:def 39 {G where G is Element of the Objects of AbGroupCat(UN) : ex H being midpoint_operator AbGroup st G = H}; end; definition let UN; cluster MidOpGroupObjects(UN) -> non empty; end; definition let UN; func MidOpGroupCat(UN) -> Subcategory of AbGroupCat(UN) equals :: GRCAT_1:def 40 cat(MidOpGroupObjects(UN)); end; definition let UN; cluster MidOpGroupCat(UN) -> strict; end; theorem :: GRCAT_1:53 the Objects of MidOpGroupCat(UN) = MidOpGroupObjects(UN); theorem :: GRCAT_1:54 L_Trivial in MidOpGroupObjects(UN);

Back to top