:: Categories of Groups :: by Michal Muzalewski :: :: Received October 3, 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, TARSKI, ZFMISC_1, SUBSET_1, FUNCT_5, FUNCT_1, FUNCT_2, ALGSTR_0, MIDSP_2, ROBBINS1, SUPINF_2, ARYTM_3, ARYTM_1, CAT_1, STRUCT_0, RELAT_1, GRAPH_1, VECTSP_1, PARTFUN1, REALSET1, MIDSP_1, CAT_2, FUNCOP_1, MSSUBFAM, RLVECT_1, ENS_1, ALGSTR_1, GRCAT_1, MONOID_0, RELAT_2, BINOP_1; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, MCART_1, REALSET1, PARTFUN1, FUNCT_2, ORDINAL1, CLASSES2, BINOP_1, FUNCOP_1, FUNCT_5, STRUCT_0, ALGSTR_0, GRAPH_1, CAT_1, TOPS_2, RLVECT_1, VECTSP_1, CAT_2, ALGSTR_1, MIDSP_2; constructors PARTFUN1, CLASSES1, CLASSES2, REALSET1, TOPS_2, VECTSP_2, CAT_2, ALGSTR_1, MIDSP_2, FUNCOP_1, RELSET_1, FUNCT_5, XTUPLE_0; registrations XBOOLE_0, RELSET_1, FUNCT_2, CLASSES2, STRUCT_0, ALGSTR_1, MIDSP_2, ALGSTR_0, CAT_1; 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; theorem :: GRCAT_1:1 for u1,u2,u3,u4 being Element of UN holds [u1,u2,u3] in UN & [u1, u2,u3,u4] in UN; :: 0c. Auxiliary theorems: Trivial Group theorem :: GRCAT_1:2 op2.({},{}) = {} & op1.{} = {} & op0 = {}; theorem :: GRCAT_1:3 {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN; registration cluster Trivial-addLoopStr -> midpoint_operator; end; theorem :: GRCAT_1:4 (for x being Element of Trivial-addLoopStr holds x = {}) & (for x,y being Element of Trivial-addLoopStr holds x+y = {}) & (for x being Element of Trivial-addLoopStr holds -x = {}) & 0.Trivial-addLoopStr = {}; :: 0d. Auxiliary theorems: subcategories reserve C for Category; reserve O for non empty Subset of the carrier of C; definition let C,O; func Morphs(O) -> Subset of the carrier' of C equals :: GRCAT_1:def 1 union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O}; end; registration 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 2 (the Source of C)|Morphs(O); func cod(O) -> Function of Morphs(O),O equals :: GRCAT_1:def 3 (the Target of C)|Morphs(O); func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals :: GRCAT_1:def 4 (the Comp of C)||Morphs(O); ::$CD end; definition let C,O; func cat(O) -> Subcategory of C equals :: GRCAT_1:def 6 CatStr (# O,Morphs(O),dom(O),cod(O),comp(O)#); end; registration let C,O; cluster cat(O) -> strict; end; theorem :: GRCAT_1:5 the carrier of cat(O) = O; :: 1a. Maps of the carriers of groups definition let G be non empty 1-sorted, H be non empty ZeroStr; func ZeroMap(G,H) -> Function of G,H equals :: GRCAT_1:def 7 (the carrier of G) --> 0.H; end; theorem :: GRCAT_1:6 comp Trivial-addLoopStr = op1; registration let G be non empty addMagma, H being right_zeroed non empty addLoopStr; cluster ZeroMap(G,H) -> additive; end; registration let G be non empty addMagma, H be right_zeroed non empty addLoopStr; cluster additive for Function of G,H; end; theorem :: GRCAT_1:7 for G1,G2,G3 being non empty addMagma, f being Function of G1, G2, g being Function of G2,G3 st f is additive & g is additive holds g*f is additive; registration let G1 be non empty addMagma, G2,G3 being right_zeroed non empty addLoopStr, f being additive Function of G1, G2, g being additive Function of G2, G3; cluster g*f -> additive for Function of G1, G3; end; :: 1b. carrier of groups reserve G,H for AddGroup; definition struct GroupMorphismStr (# Source,Target -> AddGroup, Fun -> Function of the Source, the Target #); end; definition ::$CD let f be GroupMorphismStr; func dom(f) -> AddGroup equals :: GRCAT_1:def 9 the Source of f; func cod(f) -> AddGroup equals :: GRCAT_1:def 10 the Target of f; end; definition let f be GroupMorphismStr; func fun(f) -> Function of dom(f),cod(f) equals :: GRCAT_1:def 11 the Fun of f; end; theorem :: GRCAT_1:8 for f being GroupMorphismStr, G1,G2 being AddGroup, f0 being Function 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 12 GroupMorphismStr(# G,H,ZeroMap(G,H)#); end; registration let G,H; cluster ZERO(G,H) -> strict; end; definition let IT be GroupMorphismStr; attr IT is GroupMorphism-like means :: GRCAT_1:def 13 fun(IT) is additive; end; registration cluster strict GroupMorphism-like for GroupMorphismStr; end; definition mode GroupMorphism is GroupMorphism-like GroupMorphismStr; end; theorem :: GRCAT_1:9 for F being GroupMorphism holds the Fun of F is additive; registration let G,H; cluster ZERO(G,H) -> GroupMorphism-like; end; definition let G,H; mode Morphism of G,H -> GroupMorphism means :: GRCAT_1:def 14 dom(it) = G & cod(it) = H; end; registration let G,H; cluster strict for Morphism of G,H; end; theorem :: GRCAT_1:10 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:11 for f being Function of G,H st f is additive holds GroupMorphismStr (# G,H,f#) is strict Morphism of G,H; registration let G be non empty addMagma; cluster id G -> additive; end; definition let G; func ID G -> Morphism of G,G equals :: GRCAT_1:def 15 GroupMorphismStr(# G,G,id G#); end; registration 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:12 for F being Morphism of G,H ex f being Function of G,H st the GroupMorphismStr of F = GroupMorphismStr(# G,H,f#) & f is additive; theorem :: GRCAT_1:13 for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f#); theorem :: GRCAT_1:14 for F being GroupMorphism ex G,H st F is Morphism of G,H; theorem :: GRCAT_1:15 for F being strict GroupMorphism ex G,H being AddGroup, f being Function of G,H st F is Morphism of G,H & F = GroupMorphismStr(# G,H,f#) & f is additive; theorem :: GRCAT_1:16 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 16 for G1,G2,G3 being AddGroup, g being Function of G2,G3, f being Function 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; theorem :: GRCAT_1:17 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:18 for G1,G2,G3 being AddGroup, G being Morphism of G2,G3, F being Morphism of G1,G2, g being Function of G2,G3, f being Function 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:19 for f,g being strict GroupMorphism st dom g = cod f holds ex G1, G2,G3 being AddGroup, f0 being Function of G1,G2, g0 being Function of G2,G3 st f = GroupMorphismStr(# G1,G2,f0#) & g = GroupMorphismStr(# G2,G3,g0#) & g*f = GroupMorphismStr(# G1,G3,g0*f0#); theorem :: GRCAT_1:20 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:21 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:22 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:23 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. Sourceains of groups definition let IT be set; attr IT is Group_DOMAIN-like means :: GRCAT_1:def 17 for x being object st x in IT holds x is strict AddGroup; end; registration cluster Group_DOMAIN-like non empty for 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; registration let V; cluster strict for Element of V; end; :: 3. Domains of morphisms definition let IT be set; attr IT is GroupMorphism_DOMAIN-like means :: GRCAT_1:def 18 for x being object st x in IT holds x is strict GroupMorphism; end; registration cluster GroupMorphism_DOMAIN-like non empty for 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; registration let M be GroupMorphism_DOMAIN; cluster strict for Element of M; end; theorem :: GRCAT_1:24 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 19 for x being Element of it holds x is strict Morphism of G,H; end; theorem :: GRCAT_1:25 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:26 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 -> set means :: GRCAT_1:def 20 for x being set st x in it holds x is Function of G,H; end; definition let G,H be 1-sorted; func Maps(G,H) -> MapsSet of G,H equals :: GRCAT_1:def 21 Funcs(the carrier of G, the carrier of H); end; registration let G be 1-sorted, H be non empty 1-sorted; cluster Maps(G,H) -> non empty; end; registration let G be 1-sorted, H be non empty 1-sorted; cluster non empty for 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 -> Function of G,H; end; definition let G,H; func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means :: GRCAT_1:def 22 for x being object holds 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; registration let G,H; let M be GroupMorphism_DOMAIN of G,H; cluster strict for Element of M; end; :: 4a. Category of groups - objects definition let x,y be object; pred GO x,y means :: GRCAT_1:def 23 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 addF of G & x3 = comp G & x4 = 0.G; end; theorem :: GRCAT_1:27 for x,y1,y2 being object st GO x,y1 & GO x,y2 holds y1 = y2; theorem :: GRCAT_1:28 ex x st x in UN & GO x,Trivial-addLoopStr; definition let UN; func GroupObjects(UN) -> set means :: GRCAT_1:def 24 for y being object holds y in it iff ex x being object st x in UN & GO x,y; end; theorem :: GRCAT_1:29 Trivial-addLoopStr in GroupObjects(UN); registration let UN; cluster GroupObjects(UN) -> non empty; end; theorem :: GRCAT_1:30 for x being Element of GroupObjects(UN) holds x is strict AddGroup; registration 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 25 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 groups - dom,cod,id :: definition let V; let F be Element of Morphs(V); redefine func dom(F) -> strict Element of V; redefine 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 26 ID(G); end; definition let V; func dom(V) -> Function of Morphs(V),V means :: GRCAT_1:def 27 for f being Element of Morphs(V) holds it.f = dom(f); func cod(V) -> Function of Morphs(V),V means :: GRCAT_1:def 28 for f being Element of Morphs(V) holds it.f = cod(f); end; :: :: 4d. Category of groups - superposition :: theorem :: GRCAT_1:31 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:32 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 29 (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) -> non empty non void strict CatStr equals :: GRCAT_1:def 30 CatStr(# GroupObjects(UN),Morphs( GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp( GroupObjects(UN))#); end; registration let UN; cluster GroupCat(UN) -> strict non void non empty; end; theorem :: GRCAT_1:33 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:34 for f being (Morphism of GroupCat(UN)), f9 being Element of Morphs(GroupObjects(UN)), b being Object of GroupCat(UN), b9 being Element of GroupObjects(UN) holds f is strict Element of Morphs(GroupObjects(UN)) & f9 is Morphism of GroupCat(UN) & b is strict Element of GroupObjects(UN) & b9 is Object of GroupCat(UN); ::$CT theorem :: GRCAT_1:36 for f,g being (Morphism of GroupCat(UN)), f9,g9 being Element of Morphs(GroupObjects(UN)) 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(GroupObjects(UN))) & (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; cluster GroupCat UN -> reflexive Category-like; end; registration let UN; cluster GroupCat UN -> transitive associative with_identities; end; definition let UN; func AbGroupObjects(UN) -> Subset of the carrier of GroupCat(UN) equals :: GRCAT_1:def 31 {G where G is Element of GroupCat(UN) : ex H being AbGroup st G = H }; end; theorem :: GRCAT_1:37 Trivial-addLoopStr in AbGroupObjects(UN); registration let UN; cluster AbGroupObjects(UN) -> non empty; end; definition let UN; func AbGroupCat UN -> Subcategory of GroupCat(UN) equals :: GRCAT_1:def 32 cat AbGroupObjects UN; end; registration let UN; cluster AbGroupCat(UN) -> strict; end; theorem :: GRCAT_1:38 the carrier of AbGroupCat(UN) = AbGroupObjects(UN); :: 6. Subcategory of groups with the operator of 1/2 definition let UN; func MidOpGroupObjects(UN) -> Subset of the carrier of AbGroupCat(UN) equals :: GRCAT_1:def 33 {G where G is Element of AbGroupCat(UN) : ex H being midpoint_operator AbGroup st G = H}; end; registration let UN; cluster MidOpGroupObjects(UN) -> non empty; end; definition let UN; func MidOpGroupCat UN -> Subcategory of AbGroupCat(UN) equals :: GRCAT_1:def 34 cat MidOpGroupObjects UN; end; registration let UN; cluster MidOpGroupCat(UN) -> strict; end; theorem :: GRCAT_1:39 the carrier of MidOpGroupCat(UN) = MidOpGroupObjects(UN); theorem :: GRCAT_1:40 Trivial-addLoopStr in MidOpGroupObjects(UN); theorem :: GRCAT_1:41 :: WAYBEL29:1 for S, T being non empty 1-sorted for f being Function of S, T st f is one-to-one onto holds f*f" = id T & f"*f = id S & f" is one-to-one onto; theorem :: GRCAT_1:42 for a being Object of GroupCat(UN), aa being Element of GroupObjects(UN) st a = aa holds id a = ID aa;