:: Categories of Groups
:: by Michal Muzalewski
::
:: Received October 3, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

theorem Th1: :: GRCAT_1:1
for UN being Universe
for u1, u2, u3, u4 being Element of UN holds
( [u1,u2,u3] in UN & [u1,u2,u3,u4] in UN )
proofend;

:: 0c. Auxiliary theorems: Trivial Group
theorem Th2: :: GRCAT_1:2
( op2 . ({},{}) = {} & op1 . {} = {} & op0 = {} )
proofend;

theorem Th3: :: GRCAT_1:3
for UN being Universe holds
( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )
proofend;

registration
cluster Trivial-addLoopStr  ->  midpoint_operator ;
coherence
 Trivial-addLoopStr is midpoint_operator
proofend;
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 = {} ) by CARD_1:49, TARSKI:def_1;

definition
let C be Category;
let O be non empty Subset of the carrier of C;
func Morphs O ->  Subset of the carrier' of C equals :: GRCAT_1:def 1
 union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;
coherence
 union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  is Subset of the carrier' of C by CAT_2:19;
end;

:: deftheorem  defines Morphs GRCAT_1:def_1_:_
 for C being Category
for O being non empty Subset of the carrier of C holds Morphs O = union  {  (Hom (a,b)) where a, b is Object of C : ( a in O & b in O )  }  ;

registration
let C be Category;
let O be non empty Subset of the carrier of C;
cluster Morphs O ->  non empty ;
coherence
 not Morphs O is empty by CAT_2:19;
end;

definition
let C be Category;
let O be non empty Subset of the carrier of C;
func dom O ->  Function of (Morphs O),O equals :: GRCAT_1:def 2
 the Source of C | (Morphs O);
coherence
 the Source of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;
func cod O ->  Function of (Morphs O),O equals :: GRCAT_1:def 3
 the Target of C | (Morphs O);
coherence
 the Target of C | (Morphs O) is Function of (Morphs O),O by CAT_2:20;
func comp O ->  PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) equals :: GRCAT_1:def 4
 the Comp of C || (Morphs O);
coherence
 the Comp of C || (Morphs O) is PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) by CAT_2:20;
canceled;
end;

:: deftheorem  defines dom GRCAT_1:def_2_:_
 for C being Category
for O being non empty Subset of the carrier of C holds dom O = the Source of C | (Morphs O);

:: deftheorem  defines cod GRCAT_1:def_3_:_
 for C being Category
for O being non empty Subset of the carrier of C holds cod O = the Target of C | (Morphs O);

:: deftheorem  defines comp GRCAT_1:def_4_:_
 for C being Category
for O being non empty Subset of the carrier of C holds comp O = the Comp of C || (Morphs O);

:: deftheorem  GRCAT_1:def_5_:_
canceled;

definition
let C be Category;
let O be non empty Subset of the carrier of C;
func cat O ->  Subcategory of C equals :: GRCAT_1:def 6
 CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);
coherence
 CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #) is Subcategory of C
proofend;
end;

:: deftheorem  defines cat GRCAT_1:def_6_:_
 for C being Category
for O being non empty Subset of the carrier of C holds cat O = CatStr(# O,(Morphs O),(dom O),(cod O),(comp O) #);

registration
let C be Category;
let O be non empty Subset of the carrier of C;
cluster cat O ->  strict ;
coherence
 cat O is strict ;
end;

theorem :: GRCAT_1:5
for C being Category
for O being non empty Subset of the carrier of C holds the carrier of (cat O) = O ;

:: 1a. Maps of the carriers of groups
definition
let G be non empty 1-sorted ;
let H be non empty ZeroStr ;
func ZeroMap (G,H) ->  Function of G,H equals :: GRCAT_1:def 7
 the carrier of G --> (0. H);
coherence
 the carrier of G --> (0. H) is Function of G,H ;
end;

:: deftheorem  defines ZeroMap GRCAT_1:def_7_:_
 for G being non empty 1-sorted
for H being non empty ZeroStr holds ZeroMap (G,H) = the carrier of G --> (0. H);

theorem Th6: :: GRCAT_1:6
comp Trivial-addLoopStr = op1
proofend;

registration
let G be non empty addMagma ;
let H be non empty right_zeroed addLoopStr ;
cluster ZeroMap (G,H) ->  additive ;
coherence
 ZeroMap (G,H) is additive
proofend;
end;

registration
let G be non empty addMagma ;
let H be non empty right_zeroed addLoopStr ;
cluster Relation-like the carrier of G -defined the carrier of H -valued Function-like non empty total quasi_total additive for Element of bool [: the carrier of G, the carrier of H:];
existence
 ex b1 being Function of G,H st b1 is additive
proofend;
end;

theorem Th7: :: GRCAT_1:7
for G1, G2, G3 being non empty addMagma
for f being Function of G1,G2
for g being Function of G2,G3 st f is additive & g is additive holds
g * f is additive
proofend;

registration
let G1 be non empty addMagma ;
let G2, G3 be non empty right_zeroed addLoopStr ;
let f be additive Function of G1,G2;
let g be additive Function of G2,G3;
clusterf * g ->  additive for Function of G1,G3;
coherence
 for b1 being Function of G1,G3 st b1 = g * f holds
b1 is additive by Th7;
end;

definition
attrc1 is strict ;
struct GroupMorphismStr  -> ;
aggrGroupMorphismStr(# Source, Target, Fun #) ->  GroupMorphismStr ;
sel Source c1 ->  AddGroup;
sel Target c1 ->  AddGroup;
sel Fun c1 ->  Function of the Source of c1, the Target of c1;
end;

definition
canceled;
let f be GroupMorphismStr ;
func dom f ->  AddGroup equals :: GRCAT_1:def 9
 the Source of f;
coherence
 the Source of f is AddGroup ;
func cod f ->  AddGroup equals :: GRCAT_1:def 10
 the Target of f;
coherence
 the Target of f is AddGroup ;
end;

:: deftheorem  GRCAT_1:def_8_:_
canceled;

:: deftheorem  defines dom GRCAT_1:def_9_:_
 for f being GroupMorphismStr holds dom f = the Source of f;

:: deftheorem  defines cod GRCAT_1:def_10_:_
 for f being GroupMorphismStr holds cod f = the Target of f;

definition
let f be GroupMorphismStr ;
func fun f ->  Function of (dom f),(cod f) equals :: GRCAT_1:def 11
 the Fun of f;
coherence
 the Fun of f is Function of (dom f),(cod f) ;
end;

:: deftheorem  defines fun GRCAT_1:def_11_:_
 for f being GroupMorphismStr holds fun f = the Fun of f;

theorem :: GRCAT_1:8
for f being GroupMorphismStr
for G1, G2 being AddGroup
for 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 be AddGroup;
func ZERO (G,H) ->  GroupMorphismStr  equals :: GRCAT_1:def 12
 GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);
coherence
 GroupMorphismStr(# G,H,(ZeroMap (G,H)) #) is GroupMorphismStr ;
end;

:: deftheorem  defines ZERO GRCAT_1:def_12_:_
 for G, H being AddGroup holds ZERO (G,H) = GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);

registration
let G, H be AddGroup;
cluster ZERO (G,H) ->  strict ;
coherence
 ZERO (G,H) is strict ;
end;

definition
let IT be GroupMorphismStr ;
attrIT is GroupMorphism-like  means :Def13: :: GRCAT_1:def 13
 fun IT is additive ;
end;

:: deftheorem Def13 defines GroupMorphism-like GRCAT_1:def_13_:_
 for IT being GroupMorphismStr holds
( IT is GroupMorphism-like iff fun IT is additive );

registration
cluster strict GroupMorphism-like for GroupMorphismStr ;
existence
 ex b1 being GroupMorphismStr st
( b1 is strict & b1 is GroupMorphism-like )
proofend;
end;

definition
mode GroupMorphism is GroupMorphism-like GroupMorphismStr ;
end;

theorem Th9: :: GRCAT_1:9
for F being GroupMorphism holds the Fun of F is additive
proofend;

registration
let G, H be AddGroup;
cluster ZERO (G,H) ->  GroupMorphism-like ;
coherence
 ZERO (G,H) is GroupMorphism-like
proofend;
end;

definition
let G, H be AddGroup;
mode Morphism of G,H ->  GroupMorphism means :Def14: :: GRCAT_1:def 14
( dom it = G & cod it = H );
existence
 ex b1 being GroupMorphism st
( dom b1 = G & cod b1 = H )
proofend;
end;

:: deftheorem Def14 defines Morphism GRCAT_1:def_14_:_
 for G, H being AddGroup
for b3 being GroupMorphism holds
( b3 is Morphism of G,H iff ( dom b3 = G & cod b3 = H ) );

registration
let G, H be AddGroup;
cluster strict GroupMorphism-like for Morphism of G,H;
existence
 ex b1 being Morphism of G,H st b1 is strict
proofend;
end;

theorem Th10: :: GRCAT_1:10
for G, H being AddGroup
for f being strict GroupMorphismStr st dom f = G & cod f = H & fun f is additive holds
f is strict Morphism of G,H
proofend;

theorem Th11: :: GRCAT_1:11
for G, H being AddGroup
for f being Function of G,H st f is additive holds
GroupMorphismStr(# G,H,f #) is strict Morphism of G,H
proofend;

registration
let G be non empty addMagma ;
cluster id G ->  additive ;
coherence
 id G is additive
proofend;
end;

definition
let G be AddGroup;
func ID G ->  Morphism of G,G equals :: GRCAT_1:def 15
 GroupMorphismStr(# G,G,(id G) #);
coherence
 GroupMorphismStr(# G,G,(id G) #) is Morphism of G,G
proofend;
end;

:: deftheorem  defines ID GRCAT_1:def_15_:_
 for G being AddGroup holds ID G = GroupMorphismStr(# G,G,(id G) #);

registration
let G be AddGroup;
cluster ID G ->  strict ;
coherence
 ID G is strict ;
end;

definition
let G, H be AddGroup;
:: original:ZERO
redefine func ZERO (G,H) ->  strict Morphism of G,H;
coherence
 ZERO (G,H) is strict Morphism of G,H
proofend;
end;

theorem Th12: :: GRCAT_1:12
for G, H being AddGroup
for F being Morphism of G,H ex f being Function of G,H st
( GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G,H,f #) & f is additive )
proofend;

theorem Th13: :: GRCAT_1:13
for G, H being AddGroup
for F being strict Morphism of G,H ex f being Function of G,H st F = GroupMorphismStr(# G,H,f #)
proofend;

theorem Th14: :: GRCAT_1:14
for F being GroupMorphism ex G, H being AddGroup st F is Morphism of G,H
proofend;

theorem :: GRCAT_1:15
for F being strict GroupMorphism ex G, H being AddGroup ex f being Function of G,H st
( F is Morphism of G,H & F = GroupMorphismStr(# G,H,f #) & f is additive )
proofend;

theorem Th16: :: GRCAT_1:16
for g, f being GroupMorphism st dom g = cod f holds
ex G1, G2, G3 being AddGroup st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proofend;

definition
let G, F be GroupMorphism;
assume A1: dom G = cod F ;
funcG * F ->  strict GroupMorphism means :Def16: :: GRCAT_1:def 16
 for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
it = GroupMorphismStr(# G1,G3,(g * f) #);
existence
 ex b1 being strict GroupMorphism st
for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b1 = GroupMorphismStr(# G1,G3,(g * f) #)
proofend;
uniqueness
 for b1, b2 being strict GroupMorphism st ( for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b1 = GroupMorphismStr(# G1,G3,(g * f) #) ) & ( for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b2 = GroupMorphismStr(# G1,G3,(g * f) #) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines * GRCAT_1:def_16_:_
 for G, F being GroupMorphism st dom G = cod F holds
for b3 being strict GroupMorphism holds
( b3 = G * F iff for G1, G2, G3 being AddGroup
for g being Function of G2,G3
for f being Function of G1,G2 st GroupMorphismStr(# the Source of G, the Target of G, the Fun of G #) = GroupMorphismStr(# G2,G3,g #) & GroupMorphismStr(# the Source of F, the Target of F, the Fun of F #) = GroupMorphismStr(# G1,G2,f #) holds
b3 = GroupMorphismStr(# G1,G3,(g * f) #) );

theorem Th17: :: GRCAT_1:17
for G1, G2, G3 being AddGroup
for G being Morphism of G2,G3
for F being Morphism of G1,G2 holds G * F is Morphism of G1,G3
proofend;

definition
let G1, G2, G3 be AddGroup;
let G be Morphism of G2,G3;
let F be Morphism of G1,G2;
:: original:*
redefine funcG * F ->  strict Morphism of G1,G3;
coherence
 G * F is strict Morphism of G1,G3 by Th17;
end;

theorem Th18: :: GRCAT_1:18
for G1, G2, G3 being AddGroup
for G being Morphism of G2,G3
for F being Morphism of G1,G2
for g being Function of G2,G3
for 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) #)
proofend;

theorem Th19: :: GRCAT_1:19
for f, g being strict GroupMorphism st dom g = cod f holds
ex G1, G2, G3 being AddGroup ex f0 being Function of G1,G2 ex g0 being Function of G2,G3 st
( f = GroupMorphismStr(# G1,G2,f0 #) & g = GroupMorphismStr(# G2,G3,g0 #) & g * f = GroupMorphismStr(# G1,G3,(g0 * f0) #) )
proofend;

theorem Th20: :: 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 )
proofend;

theorem Th21: :: GRCAT_1:21
for G1, G2, G3, G4 being AddGroup
for f being strict Morphism of G1,G2
for g being strict Morphism of G2,G3
for h being strict Morphism of G3,G4 holds h * (g * f) = (h * g) * f
proofend;

theorem Th22: :: 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
proofend;

theorem :: GRCAT_1:23
for G being AddGroup holds
( 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 ) )
proofend;

:: 2. Sourceains of groups
definition
let IT be set ;
attrIT is Group_DOMAIN-like  means :Def17: :: GRCAT_1:def 17
 for x being set st x in IT holds
x is strict AddGroup;
end;

:: deftheorem Def17 defines Group_DOMAIN-like GRCAT_1:def_17_:_
 for IT being set holds
( IT is Group_DOMAIN-like iff for x being set st x in IT holds
x is strict AddGroup );

registration
cluster non empty Group_DOMAIN-like for set ;
existence
 ex b1 being set st
( b1 is Group_DOMAIN-like & not b1 is empty )
proofend;
end;

definition
mode Group_DOMAIN is non empty Group_DOMAIN-like set ;
end;

definition
let V be Group_DOMAIN;
:: original:Element
redefine mode Element of V ->  AddGroup;
coherence
 for b1 being Element of V holds b1 is AddGroup by Def17;
end;

registration
let V be Group_DOMAIN;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable strict right_complementable add-associative right_zeroed left_zeroed add-left-invertible add-right-invertible Loop-like for Element of V;
existence
 ex b1 being Element of V st b1 is strict
proofend;
end;

:: 3. Domains of morphisms
definition
let IT be set ;
attrIT is GroupMorphism_DOMAIN-like  means :Def18: :: GRCAT_1:def 18
 for x being set st x in IT holds
x is strict GroupMorphism;
end;

:: deftheorem Def18 defines GroupMorphism_DOMAIN-like GRCAT_1:def_18_:_
 for IT being set holds
( IT is GroupMorphism_DOMAIN-like iff for x being set st x in IT holds
x is strict GroupMorphism );

registration
cluster non empty GroupMorphism_DOMAIN-like for set ;
existence
 ex b1 being set st
( b1 is GroupMorphism_DOMAIN-like & not b1 is empty )
proofend;
end;

definition
mode GroupMorphism_DOMAIN is non empty GroupMorphism_DOMAIN-like set ;
end;

definition
let M be GroupMorphism_DOMAIN;
:: original:Element
redefine mode Element of M ->  GroupMorphism;
coherence
 for b1 being Element of M holds b1 is GroupMorphism by Def18;
end;

registration
let M be GroupMorphism_DOMAIN;
cluster strict GroupMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proofend;
end;

theorem Th24: :: GRCAT_1:24
for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN
proofend;

definition
let G, H be AddGroup;
mode GroupMorphism_DOMAIN of G,H ->  GroupMorphism_DOMAIN means :Def19: :: GRCAT_1:def 19
 for x being Element of it holds x is strict Morphism of G,H;
existence
 ex b1 being GroupMorphism_DOMAIN st
for x being Element of b1 holds x is strict Morphism of G,H
proofend;
end;

:: deftheorem Def19 defines GroupMorphism_DOMAIN GRCAT_1:def_19_:_
 for G, H being AddGroup
for b3 being GroupMorphism_DOMAIN holds
( b3 is GroupMorphism_DOMAIN of G,H iff for x being Element of b3 holds x is strict Morphism of G,H );

theorem Th25: :: GRCAT_1:25
for D being non empty set
for G, H being AddGroup holds
( D is GroupMorphism_DOMAIN of G,H iff for x being Element of D holds x is strict Morphism of G,H )
proofend;

theorem :: GRCAT_1:26
for G, H being AddGroup
for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H
proofend;

definition
let G, H be 1-sorted ;
mode MapsSet of G,H ->  set  means :Def20: :: GRCAT_1:def 20
 for x being set st x in it holds
x is Function of G,H;
existence
 ex b1 being set st
for x being set st x in b1 holds
x is Function of G,H
proofend;
end;

:: deftheorem Def20 defines MapsSet GRCAT_1:def_20_:_
 for G, H being 1-sorted
for b3 being set holds
( b3 is MapsSet of G,H iff for x being set st x in b3 holds
x is Function of G,H );

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);
coherence
 Funcs ( the carrier of G, the carrier of H) is MapsSet of G,H
proofend;
end;

:: deftheorem  defines Maps GRCAT_1:def_21_:_
 for G, H being 1-sorted holds Maps (G,H) = Funcs ( the carrier of G, the carrier of H);

registration
let G be 1-sorted ;
let H be non empty 1-sorted ;
cluster Maps (G,H) ->  non empty ;
coherence
 not Maps (G,H) is empty ;
end;

registration
let G be 1-sorted ;
let H be non empty 1-sorted ;
cluster non empty for MapsSet of G,H;
existence
 not for b1 being MapsSet of G,H holds b1 is empty
proofend;
end;

definition
let G be 1-sorted ;
let H be non empty 1-sorted ;
let M be non empty MapsSet of G,H;
:: original:Element
redefine mode Element of M ->  Function of G,H;
coherence
 for b1 being Element of M holds b1 is Function of G,H by Def20;
end;

definition
let G, H be AddGroup;
func Morphs (G,H) ->  GroupMorphism_DOMAIN of G,H means :Def22: :: GRCAT_1:def 22
 for x being set holds
( x in it iff x is strict Morphism of G,H );
existence
 ex b1 being GroupMorphism_DOMAIN of G,H st
for x being set holds
( x in b1 iff x is strict Morphism of G,H )
proofend;
uniqueness
 for b1, b2 being GroupMorphism_DOMAIN of G,H st ( for x being set holds
( x in b1 iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff x is strict Morphism of G,H ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines Morphs GRCAT_1:def_22_:_
 for G, H being AddGroup
for b3 being GroupMorphism_DOMAIN of G,H holds
( b3 = Morphs (G,H) iff for x being set holds
( x in b3 iff x is strict Morphism of G,H ) );

definition
let G, H be AddGroup;
let M be GroupMorphism_DOMAIN of G,H;
:: original:Element
redefine mode Element of M ->  Morphism of G,H;
coherence
 for b1 being Element of M holds b1 is Morphism of G,H by Def19;
end;

registration
let G, H be AddGroup;
let M be GroupMorphism_DOMAIN of G,H;
cluster strict GroupMorphism-like for Element of M;
existence
 ex b1 being Element of M st b1 is strict
proofend;
end;

:: 4a. Category of groups - objects
definition
let x, y be set ;
pred GO x,y means :Def23: :: 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;

:: deftheorem Def23 defines GO GRCAT_1:def_23_:_
 for x, y being set holds
( GO x,y iff 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 ) ) );

theorem Th27: :: GRCAT_1:27
for x, y1, y2 being set st GO x,y1 & GO x,y2 holds
y1 = y2
proofend;

theorem Th28: :: GRCAT_1:28
for UN being Universe ex x being set st
( x in UN & GO x, Trivial-addLoopStr )
proofend;

definition
let UN be Universe;
func GroupObjects UN ->  set  means :Def24: :: GRCAT_1:def 24
 for y being set holds
( y in it iff ex x being set st
( x in UN & GO x,y ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex x being set st
( x in UN & GO x,y ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being set holds
( y in b2 iff ex x being set st
( x in UN & GO x,y ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def24 defines GroupObjects GRCAT_1:def_24_:_
 for UN being Universe
for b2 being set holds
( b2 = GroupObjects UN iff for y being set holds
( y in b2 iff ex x being set st
( x in UN & GO x,y ) ) );

theorem Th29: :: GRCAT_1:29
for UN being Universe holds Trivial-addLoopStr in GroupObjects UN
proofend;

registration
let UN be Universe;
cluster GroupObjects UN ->  non empty ;
coherence
 not GroupObjects UN is empty by Th29;
end;

theorem Th30: :: GRCAT_1:30
for UN being Universe
for x being Element of GroupObjects UN holds x is strict AddGroup
proofend;

registration
let UN be Universe;
cluster GroupObjects UN ->  Group_DOMAIN-like ;
coherence
 GroupObjects UN is Group_DOMAIN-like
proofend;
end;

:: 4b. Category of groups - morphisms
definition
let V be Group_DOMAIN;
func Morphs V ->  GroupMorphism_DOMAIN means :Def25: :: GRCAT_1:def 25
 for x being set holds
( x in it iff ex G, H being strict Element of V st x is strict Morphism of G,H );
existence
 ex b1 being GroupMorphism_DOMAIN st
for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H )
proofend;
uniqueness
 for b1, b2 being GroupMorphism_DOMAIN st ( for x being set holds
( x in b1 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def25 defines Morphs GRCAT_1:def_25_:_
 for V being Group_DOMAIN
for b2 being GroupMorphism_DOMAIN holds
( b2 = Morphs V iff for x being set holds
( x in b2 iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

::
:: 4c. Category of groups - dom,cod,id
::
definition
let V be Group_DOMAIN;
let F be Element of Morphs V;
:: original:dom
redefine func dom F ->  strict Element of V;
coherence
 dom F is strict Element of V
proofend;
:: original:cod
redefine func cod F ->  strict Element of V;
coherence
 cod F is strict Element of V
proofend;
end;

definition
let V be Group_DOMAIN;
let G be Element of V;
func ID G ->  strict Element of Morphs V equals :: GRCAT_1:def 26
 ID G;
coherence
 ID G is strict Element of Morphs V
proofend;
end;

:: deftheorem  defines ID GRCAT_1:def_26_:_
 for V being Group_DOMAIN
for G being Element of V holds ID G = ID G;

definition
let V be Group_DOMAIN;
func dom V ->  Function of (Morphs V),V means :Def27: :: GRCAT_1:def 27
 for f being Element of Morphs V holds it . f = dom f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = dom f
proofend;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = dom f ) & ( for f being Element of Morphs V holds b2 . f = dom f ) holds
b1 = b2
proofend;
func cod V ->  Function of (Morphs V),V means :Def28: :: GRCAT_1:def 28
 for f being Element of Morphs V holds it . f = cod f;
existence
 ex b1 being Function of (Morphs V),V st
for f being Element of Morphs V holds b1 . f = cod f
proofend;
uniqueness
 for b1, b2 being Function of (Morphs V),V st ( for f being Element of Morphs V holds b1 . f = cod f ) & ( for f being Element of Morphs V holds b2 . f = cod f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def27 defines dom GRCAT_1:def_27_:_
 for V being Group_DOMAIN
for b2 being Function of (Morphs V),V holds
( b2 = dom V iff for f being Element of Morphs V holds b2 . f = dom f );

:: deftheorem Def28 defines cod GRCAT_1:def_28_:_
 for V being Group_DOMAIN
for b2 being Function of (Morphs V),V holds
( b2 = cod V iff for f being Element of Morphs V holds b2 . f = cod f );

::
:: 4d. Category of groups - superposition
::
theorem Th31: :: GRCAT_1:31
for V being Group_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
ex G1, G2, G3 being strict Element of V st
( g is Morphism of G2,G3 & f is Morphism of G1,G2 )
proofend;

theorem Th32: :: GRCAT_1:32
for V being Group_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V
proofend;

definition
let V be Group_DOMAIN;
func comp V ->  PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def30: :: 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 ) );
existence
 ex b1 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b1 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b1 holds
b1 . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) holds
b1 = b2
proofend;
end;

:: deftheorem Def30 defines comp GRCAT_1:def_29_:_
 for V being Group_DOMAIN
for b2 being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b2 = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b2 iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b2 holds
b2 . (g,f) = g * f ) ) );

::
:: 4e. Definition of Category of groups
::
definition
let UN be Universe;
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)) #);
coherence
 CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #) is non empty non void strict CatStr ;
end;

:: deftheorem  defines GroupCat GRCAT_1:def_30_:_
 for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)) #);

registration
let UN be Universe;
cluster GroupCat UN ->  non empty non void strict ;
coherence
 ( GroupCat UN is strict & not GroupCat UN is void & not GroupCat UN is empty ) ;
end;

theorem Th33: :: GRCAT_1:33
for UN being Universe
for f, g being Morphism of (GroupCat UN) holds
( [g,f] in dom the Comp of (GroupCat UN) iff dom g = cod f )
proofend;

theorem Th34: :: GRCAT_1:34
for UN being Universe
for f being Morphism of (GroupCat UN)
for f9 being Element of Morphs (GroupObjects UN)
for b being Object of (GroupCat UN)
for 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) )
proofend;

theorem :: GRCAT_1:35
canceled;

theorem Th36: :: GRCAT_1:36
for UN being Universe
for f, g being Morphism of (GroupCat UN)
for f9, g9 being Element of Morphs (GroupObjects UN) st f = f9 & g = g9 holds
( ( dom g = cod f implies dom g9 = cod f9 ) & ( dom g9 = cod f9 implies dom g = cod f ) & ( dom g = cod f implies [g9,f9] in dom (comp (GroupObjects UN)) ) & ( [g9,f9] in dom (comp (GroupObjects UN)) implies dom g = cod f ) & ( dom g = cod f implies g (*) f = g9 * f9 ) & ( dom f = dom g implies dom f9 = dom g9 ) & ( dom f9 = dom g9 implies dom f = dom g ) & ( cod f = cod g implies cod f9 = cod g9 ) & ( cod f9 = cod g9 implies cod f = cod g ) )
proofend;

Lm1:  for UN being Universe
for f, g being Morphism of (GroupCat UN) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
proofend;

registration
let UN be Universe;
cluster GroupCat UN ->  non empty non void strict Category-like reflexive ;
coherence
 ( GroupCat UN is reflexive & GroupCat UN is Category-like )
proofend;
end;

Lm3:  for UN being Universe
for a being Element of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
for i being Morphism of a,a st i = ID aa holds
for b being Element of (GroupCat UN) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) &amp; ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proofend;

registration
let UN be Universe;
cluster GroupCat UN ->  non empty non void strict transitive associative with_identities ;
coherence
 ( GroupCat UN is transitive &amp; GroupCat UN is associative &amp; GroupCat UN is with_identities )
proofend;
end;

definition
let UN be Universe;
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  }  ;
coherence
  {  G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H  }  is Subset of the carrier of (GroupCat UN)
proofend;
end;

:: deftheorem  defines AbGroupObjects GRCAT_1:def_31_:_
 for UN being Universe holds AbGroupObjects UN =  {  G where G is Element of (GroupCat UN) : ex H being AbGroup st G = H  }  ;

theorem Th37: :: GRCAT_1:37
for UN being Universe holds Trivial-addLoopStr in AbGroupObjects UN
proofend;

registration
let UN be Universe;
cluster AbGroupObjects UN ->  non empty ;
coherence
 not AbGroupObjects UN is empty by Th37;
end;

definition
let UN be Universe;
func AbGroupCat UN ->  Subcategory of GroupCat UN equals :: GRCAT_1:def 32
 cat (AbGroupObjects UN);
coherence
 cat (AbGroupObjects UN) is Subcategory of GroupCat UN ;
end;

:: deftheorem  defines AbGroupCat GRCAT_1:def_32_:_
 for UN being Universe holds AbGroupCat UN = cat (AbGroupObjects UN);

registration
let UN be Universe;
cluster AbGroupCat UN ->  strict ;
coherence
 AbGroupCat UN is strict ;
end;

theorem :: GRCAT_1:38
for UN being Universe holds the carrier of (AbGroupCat UN) = AbGroupObjects UN ;

:: 6. Subcategory of groups with the operator of 1/2
definition
let UN be Universe;
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  }  ;
coherence
  {  G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  is Subset of the carrier of (AbGroupCat UN)
proofend;
end;

:: deftheorem  defines MidOpGroupObjects GRCAT_1:def_33_:_
 for UN being Universe holds MidOpGroupObjects UN =  {  G where G is Element of (AbGroupCat UN) : ex H being midpoint_operator AbGroup st G = H  }  ;

registration
let UN be Universe;
cluster MidOpGroupObjects UN ->  non empty ;
coherence
 not MidOpGroupObjects UN is empty
proofend;
end;

definition
let UN be Universe;
func MidOpGroupCat UN ->  Subcategory of AbGroupCat UN equals :: GRCAT_1:def 34
 cat (MidOpGroupObjects UN);
coherence
 cat (MidOpGroupObjects UN) is Subcategory of AbGroupCat UN ;
end;

:: deftheorem  defines MidOpGroupCat GRCAT_1:def_34_:_
 for UN being Universe holds MidOpGroupCat UN = cat (MidOpGroupObjects UN);

registration
let UN be Universe;
cluster MidOpGroupCat UN ->  strict ;
coherence
 MidOpGroupCat UN is strict ;
end;

theorem :: GRCAT_1:39
for UN being Universe holds the carrier of (MidOpGroupCat UN) = MidOpGroupObjects UN ;

theorem :: GRCAT_1:40
for UN being Universe holds Trivial-addLoopStr in MidOpGroupObjects UN
proofend;

theorem :: GRCAT_1:41
for S, T being non empty 1-sorted
for f being Function of S,T st f is one-to-one &amp; f is onto holds
( f * (f ") = id T &amp; (f ") * f = id S &amp; f " is one-to-one &amp; f " is onto )
proofend;

theorem :: GRCAT_1:42
for UN being Universe
for a being Object of (GroupCat UN)
for aa being Element of GroupObjects UN st a = aa holds
id a = ID aa
proofend;