### The Mizar article:

### Categories of Groups

**by****Michal Muzalewski**

- Received October 3, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: GRCAT_1
- [ 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; theorems BINOP_1, CAT_1, CAT_2, CLASSES2, FUNCOP_1, FUNCT_1, FUNCT_2, MIDSP_2, MCART_1, PARTFUN1, VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, RELAT_1, RELSET_1, ORDINAL1, XBOOLE_0, ALGSTR_1; schemes FUNCT_2, PARTFUN1, TARSKI, XBOOLE_0; begin :: 0a. Auxiliary theorems: sets and universums reserve x, y for set; reserve D for non empty set; reserve UN for Universe; canceled; theorem Th2: 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] proof let X,Y,A be set, z be set; assume z in A & A c= [:X,Y:]; then consider x,y such that A1: x in X & y in Y & z = [x,y] by ZFMISC_1:103; reconsider x as Element of X by A1; reconsider y as Element of Y by A1; take x,y; thus thesis by A1; end; theorem Th3: 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 proof let u1,u2,u3,u4 be Element of UN; A1: [u1,u2,u3] = [[u1,u2],u3] by MCART_1:def 3; [u1,u2,u3,u4] = [[u1,u2,u3],u4] by MCART_1:def 4; hence thesis by A1,CLASSES2:64; end; theorem Th4: for x,y st x in y & y in UN holds x in UN proof let x,y; assume A1: x in y & y in UN; then y c= UN by ORDINAL1:def 2; hence thesis by A1; end; :: 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 A1: for x,y st x in X() & y in Y() & P[x,y] holds F(x,y) in Z() proof defpred R[set,set] means $1 in X() & $2 in Y() & P[$1,$2]; deffunc G(set,set) = F($1,$2); A2: for x,y st R[x,y] holds G(x,y) in Z() by A1; consider f being PartFunc of [:X(),Y():],Z() such that A3: (for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y]) and A4: (for x,y st [x,y] in dom f holds f.[x,y] = G(x,y)) from LambdaR2(A2); take f; thus for x,y holds [x,y] in dom f iff x in X() & y in Y() & P[x,y] by A3; thus for x,y st [x,y] in dom f holds f.[x,y] = F(x,y) by A4; end; 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 A1: for x being Element of X(), y being Element of Y() st P[x,y] holds F(x,y) in Z() proof defpred R[set,set] means P[$1,$2]; deffunc G(set,set) = F($1,$2); A2: for x,y st x in X() & y in Y() & R[x,y] holds G(x,y) in Z() by A1; consider f being PartFunc of [:X(),Y():],Z() such that A3: for x,y holds [x,y] in dom f iff x in X() & y in Y() & R[x,y] and A4: for x,y st [x,y] in dom f holds f.[x,y] = G(x,y) from PartLambda2(A2); take f; thus for x being Element of X(), y being Element of Y() holds [x,y] in dom f iff P[x,y] by A3; thus for x being Element of X(), y being Element of Y() st [x,y] in dom f holds f.[x,y] = F(x,y) by A4; end; :: 0c. Auxiliary theorems: Trivial Group theorem Th5: op2.({},{}) = {} & op1.{} = {} & op0 = {} proof A1: {} in {{}} by TARSKI:def 1; [{},{}] in [:{{}},{{}}:] by ZFMISC_1:34; then op2.[{},{}] = {} by FUNCT_2:65; hence op2.({},{}) = {} by BINOP_1:def 1; thus op1.{} = {} by A1,FUNCT_2:65; thus op0 = {} by TARSKI:def 1; end; theorem Th6: {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN proof set D = {{}}; {} in UN by CLASSES2:62; hence A1: D in UN by CLASSES2:63; hence [D,D] in UN by CLASSES2:64; thus A2: [:D,D:] in UN by A1,CLASSES2:67; A3: Funcs(D,D) in UN by A1,CLASSES2:67; A4: Funcs([:D,D:],D) in UN by A1,A2,CLASSES2:67; op2 in Funcs([:D,D:],D) by FUNCT_2:11; hence op2 in UN by A4,Th4; op1 in Funcs(D,D) by FUNCT_2:11; hence op1 in UN by A3,Th4; end; theorem Th7: LoopStr (# {{}},op2,Extract {} #) is midpoint_operator proof set G = LoopStr (# {{}}, op2, Extract {} #); A1: for a being Element of G ex x being Element of G st Double x = a proof let a be Element of G; consider x being Element of G; take x; thus Double x = {} by TARSKI:def 1 .= a by TARSKI:def 1; end; now let a be Element of G; assume Double a = 0.G; thus a = {} by TARSKI:def 1 .= 0.G by TARSKI:def 1;end; hence thesis by A1,MIDSP_2:def 5; end; definition cluster L_Trivial -> midpoint_operator; coherence by Th7,ALGSTR_1:def 4; end; theorem (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 = {} by ALGSTR_1:def 4,TARSKI:def 1; :: 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 :Def5: union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O}; coherence by CAT_2:28; end; definition let C,O; cluster Morphs(O) -> non empty; coherence proof union{Hom(a,b) where a is Object of C,b is Object of C : a in O & b in O} = Morphs O by Def5; hence thesis by CAT_2:28; end; end; definition let C,O; func dom(O) -> Function of Morphs(O),O equals :Def6: (the Dom of C)|Morphs(O); coherence proof set M = Morphs(O); M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} by Def5; hence (the Dom of C)|M is Function of M,O by CAT_2:29; end; func cod(O) -> Function of Morphs(O),O equals :Def7: (the Cod of C)|Morphs(O); coherence proof set M = Morphs(O); M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} by Def5; hence (the Cod of C)|M is Function of M,O by CAT_2:29; end; func comp(O) -> PartFunc of [:Morphs(O),(Morphs(O)):],Morphs(O) equals :Def8: (the Comp of C)|([:Morphs(O),Morphs(O):] qua set); coherence proof set M = Morphs(O); M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} by Def5; hence (the Comp of C)|([:M,M:] qua set) is PartFunc of [:M,M:],M by CAT_2:29; end; func ID(O) -> Function of O,Morphs(O) equals :Def9: (the Id of C)|O; coherence proof set M = Morphs(O); M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} by Def5; hence (the Id of C)|O is Function of O,M by CAT_2:29; end; end; theorem Th9: CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) is_full_subcategory_of C proof set M = Morphs(O); A1: M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} by Def5; A2: dom(O) = (the Dom of C)|M by Def6; A3: cod(O) = (the Cod of C)|M by Def7; A4: comp(O) = (the Comp of C)|([:M,M:] qua set) by Def8; ID(O) = (the Id of C)|O by Def9; hence thesis by A1,A2,A3,A4,CAT_2:30; end; definition let C,O; func cat(O) -> Subcategory of C equals :Def10: CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#); coherence proof CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) is_full_subcategory_of C by Th9; hence thesis by CAT_2:def 6; end; end; definition let C,O; cluster cat(O) -> strict; coherence proof CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) = cat O by Def10; hence thesis; end; end; theorem Th10: the Objects of cat(O) = O proof cat(O) = CatStr (# O,Morphs(O),dom(O),cod(O),comp(O),ID(O)#) by Def10; hence thesis; end; :: 1a. Maps of the carriers of groups definition let G be 1-sorted; func id G -> map of G,G equals :Def11: id the carrier of G; coherence; end; theorem Th11: for G being non empty 1-sorted, x being Element of G holds (id G).x = x proof let G be non empty 1-sorted; let x be Element of G; id G = id the carrier of G by Def11; hence thesis by FUNCT_1:35; end; theorem Th12: 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 proof let G be 1-sorted, H be non empty 1-sorted; let f be map of G,H; set u = id G, v = id H, X = the carrier of G, Y = the carrier of H; A1: u = id X & v = id Y by Def11; A2: dom f = X by FUNCT_2:def 1; rng f c= Y by RELSET_1:12; hence f*u = f & v*f = f by A1,A2,RELAT_1:77,79; end; definition let G,H be non empty ZeroStr; func ZeroMap(G,H) -> map of G,H equals :Def12: (the carrier of G) --> 0.H; coherence proof set i = (the carrier of G) --> 0.H; dom i = the carrier of G & rng i = {0.H} by FUNCOP_1:14,19; then i is Function of the carrier of G, the carrier of H by FUNCT_2:4; hence i is map of G,H; end; end; definition let G,H be non empty LoopStr; let f be map of G,H; attr f is additive means :Def13: for x,y being Element of G holds f.(x+y) = f.x+f.y; end; theorem Th13: comp L_Trivial = op1 proof reconsider f = comp L_Trivial as Function of {{}}, {{}} by ALGSTR_1:def 4; for x being set st x in {{}} holds op1.x = f.x proof let x be set; assume A1: x in {{}}; then reconsider x as Element of L_Trivial by ALGSTR_1:def 4; x = {} by A1,TARSKI:def 1; then op1.x = -x by Th5,ALGSTR_1:def 4,TARSKI:def 1 .= f.x by VECTSP_1:def 25; hence thesis; end; hence thesis by FUNCT_2:18; end; theorem Th14: 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 proof let G1,G2,G3 be non empty LoopStr, f be map of G1,G2, g be map of G2,G3 such that A1: f is additive and A2: g is additive; set h = g*f; now let x,y be Element of G1; A3: g.(f.x) = h.x & g.(f.y) = h.y by FUNCT_2:21; thus h.(x+y) = g.(f.(x+y)) by FUNCT_2:21 .= g.(f.x+f.y) by A1,Def13 .= h.x+h.y by A2,A3,Def13;end; hence thesis by Def13; end; theorem Th15: for G being non empty ZeroStr, H being non empty LoopStr, x being Element of G holds ZeroMap(G,H).x = 0.H proof let G be non empty ZeroStr, H be non empty LoopStr; let x be Element of G; (ZeroMap(G,H)) = (the carrier of G) --> 0.H by Def12; hence thesis by FUNCOP_1:13; end; theorem Th16: for G being non empty LoopStr, H being right_zeroed (non empty LoopStr) holds ZeroMap(G,H) is additive proof let G be non empty LoopStr, H be right_zeroed (non empty LoopStr); set f = ZeroMap(G,H); for x,y being Element of G holds f.(x+y) = f.x+f.y proof let x,y be Element of G; f.(x+y) = 0.H & f.x = 0.H & f.y = 0.H by Th15; hence f.(x+y) = f.x+f.y by RLVECT_1:def 7; end; hence thesis by Def13; end; :: 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 :Def14: the Dom of f; coherence; func cod(f) -> AddGroup equals :Def15: the Cod of f; coherence; end; definition let f be GroupMorphismStr; func fun(f) -> map of dom(f),cod(f) equals :Def16: the Fun of f; coherence proof dom(f) = the Dom of f & cod(f) = the Cod of f by Def14,Def15; hence the Fun of f is map of dom(f),cod(f); end; end; theorem 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 by Def14,Def15,Def16; definition let G,H; func ZERO(G,H) -> GroupMorphismStr equals :Def17: GroupMorphismStr(# G,H,ZeroMap(G,H)#); coherence; end; definition let G,H; cluster ZERO(G,H) -> strict; coherence proof ZERO(G,H) = GroupMorphismStr(# G,H,ZeroMap(G,H)#) by Def17; hence thesis; end; end; Lm1: dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H & fun(ZERO(G,H)) = ZeroMap(G,H) proof ZERO(G,H) = GroupMorphismStr(# G,H,ZeroMap(G,H)#) by Def17; hence thesis by Def14,Def15,Def16; end; definition let IT be GroupMorphismStr; attr IT is GroupMorphism-like means :Def18: fun(IT) is additive; end; definition cluster strict GroupMorphism-like GroupMorphismStr; existence proof consider G,H; set z = ZERO(G,H); dom(z) = G & cod(z) = H & fun(z) = ZeroMap(G,H) by Lm1; then fun(z) is additive by Th16; then z is GroupMorphism-like by Def18; hence thesis; end; end; definition mode GroupMorphism is GroupMorphism-like GroupMorphismStr; end; theorem Th18: for F being GroupMorphism holds the Fun of F is additive proof let F be GroupMorphism; A1: the Fun of F = fun(F) by Def16; the Dom of F = dom(F) & the Cod of F = cod(F) by Def14,Def15; hence thesis by A1,Def18; end; definition let G,H; cluster ZERO(G,H) -> GroupMorphism-like; coherence proof set z = ZERO(G,H); dom(z) = G & cod(z) = H & fun(z) = ZeroMap(G,H) by Lm1; then fun(z) is additive by Th16; hence thesis by Def18; end; end; definition let G,H; mode Morphism of G,H -> GroupMorphism means :Def19: dom(it) = G & cod(it) = H; existence proof take ZERO(G,H); thus thesis by Lm1; end; end; definition let G,H; cluster strict Morphism of G,H; existence proof dom(ZERO(G,H)) = G & cod(ZERO(G,H)) = H by Lm1; then ZERO(G,H) is Morphism of G,H by Def19; hence thesis; end; end; theorem Th19: for f being strict GroupMorphismStr st dom(f) = G & cod(f) = H & fun(f) is additive holds f is strict Morphism of G,H proof let f be strict GroupMorphismStr; assume A1: dom(f) = G & cod(f) = H & fun(f) is additive; then reconsider f' = f as strict GroupMorphism by Def18; f' is strict Morphism of G,H by A1,Def19; hence thesis; end; theorem Th20: for f being map of G,H st f is additive holds GroupMorphismStr (# G,H,f#) is strict Morphism of G,H proof let f be map of G,H such that A1: f is additive; set F = GroupMorphismStr (# G,H,f#); dom(F) = G & cod(F) = H & fun(F) = f by Def14,Def15,Def16; hence thesis by A1,Th19; end; theorem Th21: for G being non empty LoopStr holds id G is additive proof let G be non empty LoopStr; set f = id G; for x,y being Element of G holds f.(x+y) = f.x+f.y proof let x,y be Element of G; f.(x+y) = x+y & f.x = x & f.y = y by Th11; hence f.(x+y) = f.x+f.y; end; hence thesis by Def13; end; definition let G; func ID G -> Morphism of G,G equals :Def20: GroupMorphismStr(# G,G,id G#); coherence proof set i = GroupMorphismStr(# G,G,id G#); A1: dom(i) = G & cod(i) = G & fun(i) = id G by Def14,Def15,Def16; id G is additive by Th21; hence i is Morphism of G,G by A1,Th19; end; end; definition let G; cluster ID G -> strict; coherence proof ID G = GroupMorphismStr(# G,G,id G#) by Def20; hence thesis; end; end; definition let G,H; redefine func ZERO(G,H) -> strict Morphism of G,H; coherence proof set i = ZERO(G,H); A1: dom(i) = G & cod(i) = H & fun(i) = ZeroMap(G,H) by Lm1; ZeroMap(G,H) is additive by Th16; hence thesis by A1,Th19; end; end; theorem Th22: 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 proof let F be Morphism of G,H; A1: the Dom of F = dom(F) by Def14 .= G by Def19; A2: the Cod of F = cod(F) by Def15 .= H by Def19; then reconsider f = the Fun of F as map of G,H by A1; take f; thus thesis by A1,A2,Th18; end; theorem Th23: for F being strict Morphism of G,H ex f being map of G,H st F = GroupMorphismStr(# G,H,f#) proof let F be strict Morphism of G,H; consider f being map of G,H such that A1: F = GroupMorphismStr(# G,H,f#) & f is additive by Th22; take f; thus thesis by A1; end; theorem Th24: for F being GroupMorphism ex G,H st F is Morphism of G,H proof let F be GroupMorphism; take G = the Dom of F,H = the Cod of F; dom(F) = G & cod(F) = H by Def14,Def15; hence thesis by Def19; end; theorem 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 proof let F be strict GroupMorphism; consider G,H such that A1: F is Morphism of G,H by Th24; reconsider F' = F as Morphism of G,H by A1; consider f being map of G,H such that A2: F' = GroupMorphismStr(# G,H,f#) & f is additive by Th22; take G,H,f; thus thesis by A2; end; theorem Th26: 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 proof defpred P[GroupMorphism,GroupMorphism] means dom($1) = cod($2); let g,f be GroupMorphism such that A1: P[g,f]; consider G2,G3 being AddGroup such that A2: g is Morphism of G2,G3 by Th24; A3: G2 = dom(g) by A2,Def19; consider G1,G2' being AddGroup such that A4: f is Morphism of G1,G2' by Th24; G2' = cod(f) by A4,Def19; hence thesis by A1,A2,A3,A4; end; definition let G,F be GroupMorphism; assume A1: dom(G) = cod(F); func G*F -> strict GroupMorphism means :Def21: 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#); existence proof consider G1',G2',G3' being AddGroup such that A2: G is Morphism of G2',G3' and A3: F is Morphism of G1',G2' by A1,Th26; consider g' being map of G2',G3' such that A4: the GroupMorphismStr of G = GroupMorphismStr(# G2',G3',g'#)and A5: g' is additive by A2,Th22; consider f' being map of G1',G2' such that A6: the GroupMorphismStr of F = GroupMorphismStr(# G1',G2',f'#)and A7: f' is additive by A3,Th22; g'*f' is additive by A5,A7,Th14; then reconsider T' = (GroupMorphismStr(# G1',G3',g'*f'#)) as strict GroupMorphism by Th20; take T'; thus thesis by A4,A6; end; uniqueness proof let S1,S2 be strict GroupMorphism such that A8: 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 S1 = GroupMorphismStr(# G1,G3,g*f#)and A9: 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 S2 = GroupMorphismStr(# G1,G3,g*f#); consider G2',G3' being AddGroup such that A10: G is Morphism of G2',G3' by Th24; reconsider G' = G as Morphism of G2',G3' by A10; A11: G2' = dom(G) by A10,Def19; consider G1',G2'' being AddGroup such that A12: F is Morphism of G1',G2'' by Th24; reconsider F' = F as Morphism of G1',G2'' by A12; reconsider F' as Morphism of G1',G2' by A1,A11,Def19; consider g' being map of G2',G3' such that A13: the GroupMorphismStr of G' = GroupMorphismStr(# G2',G3',g'#) and g' is additive by Th22; consider f' being map of G1',G2' such that A14: the GroupMorphismStr of F' = GroupMorphismStr(# G1',G2',f'#) and f' is additive by Th22; thus S1 = (GroupMorphismStr(# G1',G3',g'*f'#)) by A8,A13,A14 .= S2 by A9,A13,A14; end; end; canceled; theorem Th28: 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 proof let G1,G2,G3 be AddGroup, G be Morphism of G2,G3, F be Morphism of G1,G2; consider g being map of G2,G3 such that A1: the GroupMorphismStr of G = GroupMorphismStr(# G2,G3,g#) and g is additive by Th22; consider f being map of G1,G2 such that A2: the GroupMorphismStr of F = GroupMorphismStr(# G1,G2,f#) and f is additive by Th22; dom(G) = G2 by Def19 .= cod(F) by Def19; then G*F = GroupMorphismStr(# G1,G3,g*f#) by A1,A2,Def21; then dom(G*F) = G1 & cod(G*F) = G3 by Def14,Def15; hence thesis by Def19; end; 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; coherence by Th28; end; theorem Th29: 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#) proof let G1,G2,G3 be AddGroup, G be Morphism of G2,G3, F be Morphism of G1,G2, g be map of G2,G3, f be map of G1,G2 such that A1: G = GroupMorphismStr(# G2,G3,g#) & F = GroupMorphismStr(# G1,G2,f#); dom(G) = G2 by Def19 .= cod(F) by Def19; hence thesis by A1,Def21; end; theorem Th30: 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#) proof let f,g be strict GroupMorphism such that A1: dom g = cod f; set G1 = dom f,G2 = cod f, G3 = cod g; reconsider f' = f as strict Morphism of G1,G2 by Def19; reconsider g' = g as strict Morphism of G2,G3 by A1,Def19; consider f0 being map of G1,G2 such that A2: f' = GroupMorphismStr(# G1,G2,f0#) by Th23; consider g0 being map of G2,G3 such that A3: g' = GroupMorphismStr(# G2,G3,g0#) by Th23; take G1,G2,G3,f0,g0; thus thesis by A2,A3,Th29; end; theorem Th31: for f,g being strict GroupMorphism st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g proof let f,g be strict GroupMorphism; assume dom g = cod f; then consider G1,G2,G3 being AddGroup, f0 being map of G1,G2, g0 being map of G2,G3 such that A1: f = GroupMorphismStr(# G1,G2,f0#) & g = GroupMorphismStr(# G2,G3,g0#) & g*f = GroupMorphismStr(# G1,G3,g0*f0#) by Th30; thus dom(g*f) = G1 by A1,Def14 .= dom f by A1,Def14; thus cod(g*f) = G3 by A1,Def15 .= cod g by A1,Def15; end; theorem Th32: 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 proof let G1,G2,G3,G4 be AddGroup, f be strict Morphism of G1,G2, g be strict Morphism of G2,G3, h be strict Morphism of G3,G4; consider f0 being map of G1,G2 such that A1: f = GroupMorphismStr(# G1,G2,f0#) by Th23; consider g0 being map of G2,G3 such that A2: g = GroupMorphismStr(# G2,G3,g0#) by Th23; consider h0 being map of G3,G4 such that A3: h = GroupMorphismStr(# G3,G4,h0#) by Th23; A4: g*f = GroupMorphismStr(# G1,G3,g0*f0#) by A1,A2,Th29; A5: h*g = GroupMorphismStr(# G2,G4,h0*g0#) by A2,A3,Th29; h*(g*f) = GroupMorphismStr(# G1,G4,h0*(g0*f0)#) by A3,A4,Th29 .= GroupMorphismStr(# G1,G4,(h0*g0)*f0#) by RELAT_1:55 .= (h*g)*f by A1,A5,Th29; hence thesis; end; theorem Th33: for f,g,h being strict GroupMorphism st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f proof let f,g,h be strict GroupMorphism such that A1: dom h = cod g & dom g = cod f; set G2 = cod f, G3 = cod g; reconsider f' = f as Morphism of (dom f),G2 by Def19; reconsider g' = g as Morphism of G2,G3 by A1,Def19; reconsider h' = h as Morphism of G3,(cod h) by A1,Def19; h'*(g'*f') = (h'*g')*f' by Th32; hence thesis; end; theorem Th34: 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) proof set i = ID G; thus dom i = G by Def19; thus cod i = G by Def19; thus for f being strict GroupMorphism st cod f = G holds i*f = f proof let f be strict GroupMorphism such that A1: cod f = G; set H = dom(f); reconsider f' = f as Morphism of H,G by A1,Def19; A2: dom(i) = G by Def19; A3: i = GroupMorphismStr(# G,G,id G#) by Def20; consider m being map of H,G such that A4: f' = GroupMorphismStr(# H,G,m#) by Th23; (id G)*m = m by Th12; hence i*f = f by A1,A2,A3,A4,Def21; end; thus for g being strict GroupMorphism st dom g = G holds g*(ID G) = g proof let f be strict GroupMorphism such that A5: dom f = G; set H = cod(f); reconsider f' = f as Morphism of G,H by A5,Def19; A6: cod(i) = G by Def19; A7: i = GroupMorphismStr(# G,G,id G#) by Def20; consider m being map of G,H such that A8: f' = GroupMorphismStr(# G,H,m#) by Th23; m*(id G) = m by Th12; hence f*i = f by A5,A6,A7,A8,Def21; end; end; :: 2. Domains of groups definition let IT be set; attr IT is Group_DOMAIN-like means :Def22: for x being set st x in IT holds x is strict AddGroup; end; definition cluster Group_DOMAIN-like non empty set; existence proof set D = {L_Trivial}; A1: for x be set st x in D holds x is strict AddGroup by TARSKI:def 1; take D; thus thesis by A1,Def22; end; 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; coherence by Def22; end; definition let V; cluster strict Element of V; existence proof consider v being Element of V; v is strict AddGroup by Def22; hence thesis; end; end; :: 3. Domains of morphisms definition let IT be set; attr IT is GroupMorphism_DOMAIN-like means :Def23: for x being set st x in IT holds x is strict GroupMorphism; end; definition cluster GroupMorphism_DOMAIN-like non empty set; existence proof consider G; take {ID G}; for x being set st x in {ID G} holds x is strict GroupMorphism by TARSKI:def 1; hence thesis by Def23; end; 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; coherence by Def23; end; definition let M be GroupMorphism_DOMAIN; cluster strict Element of M; existence proof consider m being Element of M; m is strict GroupMorphism by Def23; hence thesis; end; end; canceled 2; theorem Th37: for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN proof let f be strict GroupMorphism; for x being set st x in {f} holds x is strict GroupMorphism by TARSKI:def 1 ; hence thesis by Def23; end; definition let G,H; mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means :Def24: for x being Element of it holds x is strict Morphism of G,H; existence proof reconsider D = {ZERO(G,H)} as GroupMorphism_DOMAIN by Th37; take D; thus thesis by TARSKI:def 1; end; end; theorem Th38: D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H proof thus D is GroupMorphism_DOMAIN of G,H implies for x being Element of D holds x is strict Morphism of G,H by Def24; thus (for x being Element of D holds x is strict Morphism of G,H) implies D is GroupMorphism_DOMAIN of G,H proof assume A1: for x being Element of D holds x is strict Morphism of G,H; then for x being set st x in D holds x is strict GroupMorphism; then reconsider D' = D as GroupMorphism_DOMAIN by Def23; for x being Element of D' holds x is strict Morphism of G,H by A1; hence thesis by Def24; end; end; theorem for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H proof let f be strict Morphism of G,H; for x being Element of {f} holds x is strict Morphism of G,H by TARSKI:def 1; hence thesis by Th38; end; definition let G,H be 1-sorted; mode MapsSet of G,H means :Def25: for x being set st x in it holds x is map of G,H; existence proof take {}; thus thesis; end; end; definition let G,H be 1-sorted; func Maps(G,H) -> MapsSet of G,H equals :Def26: Funcs(the carrier of G, the carrier of H); coherence proof let x be set; assume x in Funcs(the carrier of G, the carrier of H); then x is Function of the carrier of G, the carrier of H by FUNCT_2:121; hence thesis; end; end; definition let G be 1-sorted, H be non empty 1-sorted; cluster Maps(G,H) -> non empty; coherence proof Maps(G,H) = Funcs(the carrier of G, the carrier of H) by Def26; hence thesis; end; end; definition let G be 1-sorted, H be non empty 1-sorted; cluster non empty MapsSet of G,H; existence proof Maps(G,H) is non empty; hence thesis; end; 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; coherence by Def25; end; definition let G,H; func Morphs(G,H) -> GroupMorphism_DOMAIN of G,H means :Def27: x in it iff x is strict Morphism of G,H; existence proof set D = { GroupMorphismStr(# G,H,f#) where f is Element of Maps(G,H) : f is additive }; ZeroMap(G,H) is Element of Funcs(the carrier of G, the carrier of H) by FUNCT_2:11; then reconsider f0 = ZeroMap(G,H) as Element of Maps(G,H) by Def26; f0 is additive by Th16; then GroupMorphismStr(# G,H,f0#) in D; then reconsider D as non empty set; A1: x in D implies x is strict Morphism of G,H proof assume x in D; then ex f being Element of Maps(G,H) st x = GroupMorphismStr (# G,H,f#) & f is additive; hence thesis by Th20; end; then A2: for x being Element of D holds x is strict Morphism of G,H; A3: x is strict Morphism of G,H implies x in D proof assume x is strict Morphism of G,H; then reconsider x as strict Morphism of G,H; dom(x) = G & cod(x) = H by Def19; then A4: the Dom of x = G & the Cod of x = H by Def14,Def15; A5: (the Fun of x) is additive by Th18; reconsider f = the Fun of x as map of G,H by A4; f is Element of Funcs(the carrier of G, the carrier of H) by FUNCT_2:11; then reconsider g = f as Element of Maps(G,H) by Def26; x = GroupMorphismStr(# G,H,g #) by A4; hence thesis by A5; end; reconsider D as GroupMorphism_DOMAIN of G,H by A2,Th38; take D; thus thesis by A1,A3; end; uniqueness proof let D1,D2 be GroupMorphism_DOMAIN of G,H such that A6: x in D1 iff x is strict Morphism of G,H and A7: x in D2 iff x is strict Morphism of G,H; x in D1 iff x in D2 proof thus x in D1 implies x in D2 proof assume x in D1; then x is strict Morphism of G,H by A6; hence thesis by A7; end; thus x in D2 implies x in D1 proof assume x in D2; then x is strict Morphism of G,H by A7; hence thesis by A6; end; end; hence thesis by TARSKI:2; end; end; definition let G,H; let M be GroupMorphism_DOMAIN of G,H; redefine mode Element of M -> Morphism of G,H; coherence by Def24; end; definition let G,H; let M be GroupMorphism_DOMAIN of G,H; cluster strict Element of M; existence proof consider m being Element of M; m is strict Morphism of G,H by Def24; hence thesis; end; end; :: 4a. Category of groups - objects definition let x,y; pred GO x,y means :Def28: 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 Th40: for x,y1,y2 being set st GO x,y1 & GO x,y2 holds y1 = y2 proof let x,y1,y2 be set such that A1: GO x,y1 and A2: GO x,y2; consider a1,a2,a3,a4 being set such that A3: x = [a1,a2,a3,a4]and A4: ex G being strict AddGroup st y1 = G & a1 = the carrier of G & a2 = the add of G & a3 = comp G & a4 = the Zero of G by A1,Def28; consider b1,b2,b3,b4 being set such that A5: x = [b1,b2,b3,b4]and A6: ex G being strict AddGroup st y2 = G & b1 = the carrier of G & b2 = the add of G & b3 = comp G & b4 = the Zero of G by A2,Def28; consider G1 being strict AddGroup such that A7: y1 = G1 & a1 = the carrier of G1 & a2 = the add of G1 & a3 = comp G1 & a4 = the Zero of G1 by A4; consider G2 being strict AddGroup such that A8: y2 = G2 & b1 = the carrier of G2 & b2 = the add of G2 & b3 = comp G2 & b4 = the Zero of G2 by A6; the carrier of G1 = the carrier of G2 & the add of G1 = the add of G2 & comp G1 = comp G2 & the Zero of G1 = the Zero of G2 by A3,A5,A7,A8,MCART_1:33; hence thesis by A7,A8; end; theorem Th41: ex x st x in UN & GO x,L_Trivial proof reconsider u = {} as Element of UN by CLASSES2:62; set x1 = {u}; Extract {} = u by ALGSTR_1:def 3; then reconsider x4 = Extract {} as Element of UN; reconsider x3 = comp L_Trivial as Element of UN by Th6,Th13; reconsider x2 = op2 as Element of UN by Th6; set x = [x1,x2,x3,x4]; A1: x is Element of UN by Th3; take x; thus thesis by A1,Def28,ALGSTR_1:def 4; end; definition let UN; func GroupObjects(UN) -> set means :Def29: for y holds y in it iff ex x st x in UN & GO x,y; existence proof defpred P[set,set] means GO $1,$2; A1: for x,y1,y2 being set st P[x,y1] & P[x,y2] holds y1 = y2 by Th40; consider Y being set such that A2: for y holds y in Y iff ex x st x in UN & P[x,y] from Fraenkel(A1); take Y; thus thesis by A2; end; uniqueness proof defpred P[set] means ex x st x in UN & GO x,$1; for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq; hence thesis; end; end; theorem Th42: L_Trivial in GroupObjects(UN) proof ex x st x in UN & GO x,L_Trivial by Th41; hence thesis by Def29; end; definition let UN; cluster GroupObjects(UN) -> non empty; coherence by Th42; end; theorem Th43: for x being Element of GroupObjects(UN) holds x is strict AddGroup proof let x be Element of GroupObjects(UN); consider u being set such that A1: u in UN & GO u,x by Def29; ex x1,x2,x3,x4 being set st u = [x1,x2,x3,x4] & ex G being strict AddGroup st x = G & x1 = the carrier of G & x2 = the add of G & x3 = comp G & x4 = the Zero of G by A1,Def28; hence thesis; end; definition let UN; cluster GroupObjects(UN) -> Group_DOMAIN-like; coherence proof for x being set st x in GroupObjects(UN) holds x is strict AddGroup by Th43; hence thesis by Def22; end; end; :: 4b. Category of groups - morphisms definition let V; func Morphs(V) -> GroupMorphism_DOMAIN means :Def30: for x holds x in it iff ex G,H being strict Element of V st x is strict Morphism of G,H; existence proof consider G0,H0 being strict Element of V; set M = Morphs(G0,H0), S = { Morphs(G,H) where G is strict Element of V, H is strict Element of V : not contradiction }; A1: (ZERO(G0,H0)) is Element of M by Def27; M in S; then reconsider T = union S as non empty set by A1,TARSKI:def 4; A2: for x holds x in T iff ex G,H being strict Element of V st x is strict Morphism of G,H proof let x; thus x in T implies ex G,H being strict Element of V st x is strict Morphism of G,H proof assume x in T; then consider Y being set such that A3: x in Y and A4: Y in S by TARSKI:def 4; consider G,H being strict Element of V such that A5: Y = Morphs(G,H) by A4; take G,H; thus thesis by A3,A5,Def27; end; thus (ex G,H being strict Element of V st x is strict Morphism of G,H) implies x in T proof given G,H being strict Element of V such that A6: x is strict Morphism of G,H; set M = Morphs(G,H); A7: x in M by A6,Def27; M in S; hence thesis by A7,TARSKI:def 4; end; end; now let x be set; assume x in T; then ex G,H being strict Element of V st x is strict Morphism of G,H by A2; hence x is strict GroupMorphism;end; then reconsider T' = T as GroupMorphism_DOMAIN by Def23; take T'; thus thesis by A2; end; uniqueness proof let D1,D2 be GroupMorphism_DOMAIN such that A8: for x holds x in D1 iff ex G,H being strict Element of V st x is strict Morphism of G,H and A9: for x holds x in D2 iff ex G,H being strict Element of V st x is strict Morphism of G,H; now let x; x in D1 iff ex G,H being strict Element of V st x is strict Morphism of G,H by A8; hence x in D1 iff x in D2 by A9;end; hence thesis by TARSKI:2; end; 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; coherence proof consider G,H being strict Element of V such that A1: F is strict Morphism of G,H by Def30; reconsider F' = F as Morphism of G,H by A1; dom(F') = G by Def19; hence thesis; end; func cod(F) -> strict Element of V; coherence proof consider G,H being strict Element of V such that A2: F is strict Morphism of G,H by Def30; reconsider F' = F as Morphism of G,H by A2; cod(F') = H by Def19; hence thesis; end; end; definition let V; let G be Element of V; func ID(G) -> strict Element of Morphs(V) equals :Def31: ID(G); coherence proof reconsider G' = G as strict Element of V by Def22; ID(G') is strict Element of Morphs(V) by Def30; hence thesis; end; end; definition let V; func dom(V) -> Function of Morphs(V),V means :Def32: for f being Element of Morphs(V) holds it.f = dom(f); existence proof deffunc F(Element of Morphs(V)) = dom $1; consider F being Function of Morphs(V),V such that A1: for f being Element of Morphs(V) holds F.f = F(f) from LambdaD; take F; thus thesis by A1; end; uniqueness proof let F1,F2 be Function of Morphs(V),V such that A2: for f being Element of Morphs(V) holds F1.f = dom(f) and A3: for f being Element of Morphs(V) holds F2.f = dom(f); now let f be Element of Morphs(V); F1.f = dom(f) by A2; hence F1.f = F2.f by A3;end; hence thesis by FUNCT_2:113; end; func cod(V) -> Function of Morphs(V),V means :Def33: for f being Element of Morphs(V) holds it.f = cod(f); existence proof deffunc F(Element of Morphs(V)) = cod $1; consider F being Function of Morphs(V),V such that A4: for f being Element of Morphs(V) holds F.f = F(f) from LambdaD; take F; thus thesis by A4; end; uniqueness proof let F1,F2 be Function of Morphs(V),V such that A5: for f being Element of Morphs(V) holds F1.f = cod(f) and A6: for f being Element of Morphs(V) holds F2.f = cod(f); now let f be Element of Morphs(V); F1.f = cod(f) by A5; hence F1.f = F2.f by A6;end; hence thesis by FUNCT_2:113; end; func ID(V) -> Function of V,Morphs(V) means :Def34: for G being Element of V holds it.G = ID(G); existence proof deffunc F(Element of V) = ID $1; consider F being Function of V,Morphs(V) such that A7: for G being Element of V holds F.G = F(G) from LambdaD; take F; thus thesis by A7; end; uniqueness proof let F1,F2 be Function of V,Morphs(V) such that A8: for G being Element of V holds F1.G = ID(G) and A9: for G being Element of V holds F2.G = ID(G); now let G be Element of V; F1.G = ID(G) by A8; hence F1.G = F2.G by A9;end; hence thesis by FUNCT_2:113; end; end; :: :: 4d. Category of groups - superposition :: theorem Th44: 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 proof set X = Morphs(V); defpred P[Element of X,Element of X] means dom($1) = cod($2); let g,f be Element of X such that A1: P[g,f]; consider G2,G3 being strict Element of V such that A2: g is strict Morphism of G2,G3 by Def30; A3: G2 = dom(g) by A2,Def19; consider G1,G2' being strict Element of V such that A4: f is strict Morphism of G1,G2' by Def30; G2' = cod(f) by A4,Def19; hence thesis by A1,A2,A3,A4; end; theorem Th45: for g,f being Element of Morphs(V) st dom(g) = cod(f) holds g*f in Morphs(V) proof set X = Morphs(V); defpred P[Element of X,Element of X] means dom($1) = cod($2); let g,f be Element of X; assume P[g,f]; then consider G1,G2,G3 being strict Element of V such that A1: g is Morphism of G2,G3 & f is Morphism of G1,G2 by Th44; reconsider g' = g as Morphism of G2,G3 by A1; reconsider f' = f as Morphism of G1,G2 by A1; g'*f' is Morphism of G1,G3; hence thesis by Def30; end; definition let V; func comp(V) -> PartFunc of [:Morphs(V),Morphs(V):],Morphs(V) means :Def35: (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); existence proof set X = Morphs(V); defpred P[Element of X,Element of X] means dom($1) = cod($2); deffunc F(Element of X,Element of X) = $1*$2; A1: for g,f being Element of X st P[g,f] holds F(g,f) in X by Th45; consider c being PartFunc of [:X,X:],X such that A2: for g,f being Element of X holds [g,f] in dom c iff P[g,f] and A3: for g,f being Element of X st [g,f] in dom c holds c.[g,f] = F(g,f) from PartLambda2D(A1); take c; thus thesis by A2,A3; end; uniqueness proof set X = Morphs(V); defpred P[Element of X,Element of X] means dom($1) = cod($2); let c1,c2 be PartFunc of [:X,X:],X such that A4: for g,f being Element of X holds [g,f] in dom c1 iff P[g,f] and A5: for g,f being Element of X st [g,f] in dom c1 holds c1.[g,f] = g*f and A6: for g,f being Element of X holds [g,f] in dom c2 iff P[g,f] and A7: for g,f being Element of X st [g,f] in dom c2 holds c2.[g,f] = g*f; A8: dom c1 c= [:X,X:] & dom c2 c= [:X,X:] by RELSET_1:12; A9: dom c1 = dom c2 proof now let x; assume A10: x in dom c1; then consider g,f being Element of X such that A11: x = [g,f] by A8,Th2; P[g,f] by A4,A10,A11; hence x in dom c2 by A6,A11;end; then A12: dom c1 c= dom c2 by TARSKI:def 3; now let x; assume A13: x in dom c2; then consider g,f being Element of X such that A14: x = [g,f] by A8,Th2; P[g,f] by A6,A13,A14; hence x in dom c1 by A4,A14;end; then dom c2 c= dom c1 by TARSKI:def 3; hence thesis by A12,XBOOLE_0:def 10; end; set V' = dom c1; for x,y st [x,y] in V' holds c1.[x,y]=c2.[x,y] proof let x,y;assume A15: [x,y] in V'; then reconsider x,y as Element of X by A8,ZFMISC_1:106; c1.[x,y] = x*y by A5,A15; hence thesis by A7,A9,A15; end; hence thesis by A9,PARTFUN1:35; end; end; :: :: 4e. Definition of Category of groups :: definition let UN; func GroupCat(UN) -> CatStr equals :Def36: CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp(GroupObjects(UN)),ID(GroupObjects(UN))#); coherence; end; definition let UN; cluster GroupCat(UN) -> strict; coherence proof GroupCat UN = CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp(GroupObjects(UN)),ID(GroupObjects(UN))#) by Def36; hence thesis; end; end; theorem Th46: for f,g being Morphism of GroupCat(UN) holds [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f proof set C = GroupCat(UN), V = GroupObjects(UN); A1: C = CatStr(# V,Morphs(V),dom(V),cod(V),comp(V),ID(V)#) by Def36; let f,g be Morphism of C; reconsider f' = f as Element of Morphs(V) by A1; reconsider g' = g as Element of Morphs(V) by A1; A2: dom g = dom(V).g' by A1,CAT_1:def 2 .= dom(g') by Def32; cod f = cod(V).f' by A1,CAT_1:def 3 .= cod(f') by Def33; hence thesis by A1,A2,Def35; end; theorem Th47: 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) proof set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V); A1: C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36; let f be (Morphism of C), f' be Element of X, b be Object of C, b' be Element of V; ex G,H being strict Element of V st f is strict Morphism of G,H by A1,Def30; hence f is strict Element of X by A1; thus f' is Morphism of C by A1; consider x such that A2: x in UN & GO x,b by A1,Def29; ex x1,x2,x3,x4 being set st x = [x1,x2,x3,x4] & ex G being strict AddGroup st b = G & x1 = the carrier of G & x2 = the add of G & x3 = comp G & x4 = the Zero of G by A2,Def28; hence b is strict Element of V by A1; thus b' is Object of C by A1; end; theorem Th48: for b being Object of GroupCat(UN), b' being Element of GroupObjects(UN) st b = b' holds id b = ID(b') proof set C = GroupCat(UN), V = GroupObjects(UN); A1: C = CatStr(# V,(Morphs(V)),dom(V),cod(V),comp(V),ID(V)#) by Def36; let b be Object of C, b' be Element of V; assume b = b'; hence id b = (ID(V)).b' by A1,CAT_1:def 5 .= ID(b') by Def34; end; theorem Th49: 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' proof set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V); A1: C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36; let f be (Morphism of C), f' be Element of X; assume A2: f = f'; hence dom f = dom(V).f' by A1,CAT_1:def 2 .= dom f' by Def32; thus cod f = cod(V).f' by A1,A2,CAT_1:def 3 .= cod f' by Def33; end; theorem Th50: 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') proof set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V); A1: C = CatStr(# V,X,dom(V),cod(V),comp(V),ID(V)#) by Def36; let f,g be Morphism of C; let f',g' be Element of X; assume A2: f = f' & g = g'; then A3: dom g = dom g' by Th49; A4: cod f = cod f' by A2,Th49; A5: dom f = dom f' by A2,Th49; A6: cod g = cod g' by A2,Th49; thus dom g = cod f iff dom g' = cod f' by A2,A4,Th49; thus A7: dom g = cod f iff [g',f'] in dom comp(V) by A3,A4,Def35; thus dom g = cod f implies g*f = g'*f' proof assume A8: dom g = cod f; then [g,f] in dom (the Comp of C) by Th46; hence g*f = (comp(V)).[g',f'] by A1,A2,CAT_1:def 4 .= g'*f' by A7,A8,Def35; end; thus dom f = dom g iff dom f' = dom g' by A2,A5,Th49; thus cod f = cod g iff cod f' = cod g' by A2,A6,Th49; end; Lm2: for f,g being Morphism of GroupCat(UN) st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g proof set X = Morphs(GroupObjects(UN)); let f,g be Morphism of GroupCat(UN) such that A1: dom g = cod f; reconsider f' = f as strict Element of X by Th47; reconsider g' = g as strict Element of X by Th47; A2: dom g' = cod f' by A1,Th50; then A3: dom(g'*f') = dom f' & cod (g'*f') = cod g' by Th31; reconsider gf = g'*f' as Element of X by A2,Th45; gf = g*f by A1,Th50; hence thesis by A3,Th50; end; Lm3: for f,g,h being Morphism of GroupCat(UN) st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f proof set X = Morphs( (GroupObjects(UN))); let f,g,h be Morphism of (GroupCat(UN)) such that A1: dom h = cod g & dom g = cod f; reconsider f'=f, g'=g, h'=h as strict Element of X by Th47; A2: dom h' = cod g' & dom g' = cod f' by A1,Th50; A3: g'*f' = g*f & h'*g' = h*g by A1,Th50; reconsider gf = g'*f', hg = h'*g' as Element of X by A2,Th45; A4: dom(h) = cod(g*f) by A1,Lm2; A5: dom(h*g) = cod(f) by A1,Lm2; h*(g*f) = h'*gf by A3,A4,Th50 .= hg*f' by A2,Th33 .= (h*g)*f by A3,A5,Th50; hence thesis; end; Lm4: for b being Object of GroupCat(UN) holds dom id b = b & cod id b = b & (for f being Morphism of GroupCat(UN) st cod f = b holds (id b)*f = f) & (for g being Morphism of GroupCat(UN) st dom g = b holds g*(id b) = g) proof set C = GroupCat(UN), V = GroupObjects(UN); set X = Morphs(V); let b be Object of C; reconsider b' = b as Element of V by Th47; reconsider b'' = b' as AddGroup; A1: id b = ID(b') by Th48; hence A2: dom id b = dom ID(b') by Th49 .= dom ID(b'') by Def31 .= b by Th34; thus A3: cod id b = cod ID(b') by A1,Th49 .= cod ID(b'') by Def31 .= b by Th34; thus for f being Morphism of C st cod f = b holds (id b)*f = f proof let f be Morphism of C such that A4: cod f = b; reconsider f1 = f as strict Element of X by Th47; reconsider f' = f1 as strict GroupMorphism; A5: cod f' = b'' by A4,Th49; thus (id b)*f = ID(b')*f' by A1,A2,A4,Th50 .= ID(b'')*f' by Def31 .= f by A5,Th34; end; thus for g being Morphism of C st dom g = b holds g*(id b) = g proof let f be Morphism of C such that A6: dom f = b; reconsider f1 = f as strict Element of X by Th47; reconsider f' = f1 as strict GroupMorphism; A7: dom f' = b'' by A6,Th49; thus f*(id b) = f'*ID(b') by A1,A3,A6,Th50 .= f'*ID(b'') by Def31 .= f by A7,Th34; end; end; definition let UN; cluster GroupCat(UN) -> Category-like; coherence proof ( for f,g being Morphism of GroupCat(UN) holds [g,f] in dom(the Comp of GroupCat(UN)) iff dom g = cod f ) & ( for f,g being Morphism of GroupCat(UN) st dom g = cod f holds dom(g*f) = dom f & cod (g*f) = cod g ) & ( for f,g,h being Morphism of GroupCat(UN) st dom h = cod g & dom g = cod f holds h*(g*f) = (h*g)*f ) & ( for b being Object of GroupCat(UN) holds dom id b = b & cod id b = b & (for f being Morphism of GroupCat(UN) st cod f = b holds (id b)*f = f) & (for g being Morphism of GroupCat(UN) st dom g = b holds g*(id b) = g) ) by Lm2,Lm3,Lm4,Th46; hence thesis by CAT_1:29; end; end; definition let UN; func AbGroupObjects(UN) -> Subset of the Objects of GroupCat(UN) equals :Def37: {G where G is Element of the Objects of GroupCat(UN) : ex H being AbGroup st G = H}; coherence proof set D2 = the Objects of GroupCat(UN); now let x be set; assume x in {G where G is Element of D2 : ex H being AbGroup st G = H}; then ex G being Element of D2 st x = G & ex H being AbGroup st G = H; hence x in D2;end; hence thesis by TARSKI:def 3; end; end; theorem Th51: L_Trivial in AbGroupObjects(UN) proof set D2 = the Objects of GroupCat(UN); set T = L_Trivial; GroupCat(UN) = CatStr(# GroupObjects(UN),Morphs(GroupObjects(UN)), dom(GroupObjects(UN)),cod(GroupObjects(UN)), comp(GroupObjects(UN)),ID(GroupObjects(UN))#) by Def36; then T in D2 by Th42; then T in {G where G is Element of D2 : ex H being AbGroup st G = H}; hence thesis by Def37; end; definition let UN; cluster AbGroupObjects(UN) -> non empty; coherence by Th51; end; definition let UN; func AbGroupCat(UN) -> Subcategory of GroupCat(UN) equals :Def38: cat(AbGroupObjects(UN)); coherence; end; definition let UN; cluster AbGroupCat(UN) -> strict; coherence proof AbGroupCat(UN) = cat(AbGroupObjects(UN)) by Def38; hence thesis; end; end; theorem Th52: the Objects of AbGroupCat(UN) = AbGroupObjects(UN) proof AbGroupCat(UN) = cat(AbGroupObjects(UN)) by Def38; hence thesis by Th10; end; :: 6. Subcategory of groups with the operator of 1/2 definition let UN; func MidOpGroupObjects(UN) -> Subset of the Objects of AbGroupCat(UN) equals :Def39: {G where G is Element of the Objects of AbGroupCat(UN) : ex H being midpoint_operator AbGroup st G = H}; coherence proof set D2 = the Objects of AbGroupCat(UN); now let x be set; assume x in {G where G is Element of D2 : ex H being midpoint_operator AbGroup st G = H}; then ex G being Element of D2 st x = G & ex H being midpoint_operator AbGroup st G = H; hence x in D2;end; hence thesis by TARSKI:def 3; end; end; definition let UN; cluster MidOpGroupObjects(UN) -> non empty; coherence proof set D2 = the Objects of AbGroupCat(UN); set D1 = {G where G is Element of D2 : ex H being midpoint_operator AbGroup st G = H}; set T = L_Trivial; D2 = AbGroupObjects(UN) by Th52; then T in D2 by Th51; then T in D1; then reconsider D1 as non empty set; now let x be set; assume x in D1; then ex G being Element of D2 st x = G & ex H being midpoint_operator AbGroup st G = H; hence x in D2;end; hence thesis by Def39; end; end; definition let UN; func MidOpGroupCat(UN) -> Subcategory of AbGroupCat(UN) equals :Def40: cat(MidOpGroupObjects(UN)); coherence; end; definition let UN; cluster MidOpGroupCat(UN) -> strict; coherence proof MidOpGroupCat(UN) = cat(MidOpGroupObjects(UN)) by Def40; hence thesis; end; end; theorem the Objects of MidOpGroupCat(UN) = MidOpGroupObjects(UN) proof MidOpGroupCat(UN) = cat(MidOpGroupObjects(UN)) by Def40; hence thesis by Th10; end; theorem L_Trivial in MidOpGroupObjects(UN) proof set D2 = the Objects of AbGroupCat(UN); set T = L_Trivial; D2 = AbGroupObjects(UN) by Th52; then T in D2 by Th51; then T in {G where G is Element of D2 : ex H being midpoint_operator AbGroup st G = H}; hence thesis by Def39; end;

Back to top