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

begin

theorem :: GRCAT_1:1

canceled;

theorem :: GRCAT_1:2

canceled;

theorem Th3: :: GRCAT_1:3

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 )

proof end;

theorem :: GRCAT_1:4

canceled;

theorem Th5: :: GRCAT_1:5

( op2 . ({},{}) = {} & op1 . {} = {} & op0 = {} )

proof end;

theorem Th6: :: GRCAT_1:6

for UN being Universe holds
( {{}} in UN & [{{}},{{}}] in UN & [:{{}},{{}}:] in UN & op2 in UN & op1 in UN )

proof end;

registration

cluster Trivial-addLoopStr -> midpoint_operator ;
coherence
Trivial-addLoopStr is midpoint_operator

proof end;

end;

theorem :: GRCAT_1:7

canceled;

theorem :: GRCAT_1:8

( ( 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:87, TARSKI:def 1;

definition

let C be Category;
let O be non empty Subset of the carrier of C;
canceled;
canceled;
canceled;
canceled;
func Morphs O -> Subset of the carrier' of C equals :: GRCAT_1:def 5
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:28;

end;

:: deftheorem GRCAT_1:def 1 :
canceled;

:: deftheorem GRCAT_1:def 2 :
canceled;

:: deftheorem GRCAT_1:def 3 :
canceled;

:: deftheorem GRCAT_1:def 4 :
canceled;

:: deftheorem defines Morphs GRCAT_1:def 5 :
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:28;

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 6
the Source of C | (Morphs O);
coherence
the Source of C | (Morphs O) is Function of (Morphs O),O by CAT_2:29;
func cod O -> Function of (Morphs O),O equals :: GRCAT_1:def 7
the Target of C | (Morphs O);
coherence
the Target of C | (Morphs O) is Function of (Morphs O),O by CAT_2:29;
func comp O -> PartFunc of [:(Morphs O),(Morphs O):],(Morphs O) equals :: GRCAT_1:def 8
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:29;
func ID O -> Function of O,(Morphs O) equals :: GRCAT_1:def 9
the Id of C | O;
coherence
the Id of C | O is Function of O,(Morphs O) by CAT_2:29;

end;

:: deftheorem defines dom GRCAT_1:def 6 :
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 7 :
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 8 :
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 defines ID GRCAT_1:def 9 :
for C being Category
for O being non empty Subset of the carrier of C holds ID O = the Id of C | O;

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 10
CatStr(# O,(Morphs O),(dom O),(cod O),(comp O),(ID O) #);
coherence
CatStr(# O,(Morphs O),(dom O),(cod O),(comp O),(ID O) #) is Subcategory of C

proof end;

end;

:: deftheorem defines cat GRCAT_1:def 10 :
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),(ID 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:9

canceled;

theorem :: GRCAT_1:10

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

definition

let G be non empty 1-sorted ;
let H be non empty ZeroStr ;
canceled;
func ZeroMap (G,H) -> Function of G,H equals :: GRCAT_1:def 12
the carrier of G --> (0. H);
coherence
the carrier of G --> (0. H) is Function of G,H ;

end;

:: deftheorem GRCAT_1:def 11 :
canceled;

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

definition

let G, H be non empty addMagma ;
let f be Function of G,H;
attr f is additive means :Def13: :: GRCAT_1:def 13
for x, y being Element of G holds f . (x + y) = (f . x) + (f . y);

end;

:: deftheorem Def13 defines additive GRCAT_1:def 13 :
for G, H being non empty addMagma
for f being Function of G,H holds
( f is additive iff for x, y being Element of G holds f . (x + y) = (f . x) + (f . y) );

theorem :: GRCAT_1:11

canceled;

theorem :: GRCAT_1:12

canceled;

theorem Th13: :: GRCAT_1:13

comp Trivial-addLoopStr = op1

proof end;

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

proof end;

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 Element of bool [: the carrier of G, the carrier of H:];
existence
ex b₁ being Function of G,H st b₁ is additive

proof end;

end;

theorem Th14: :: GRCAT_1:14

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

proof end;

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;
cluster f * g -> additive Function of G1,G3;
coherence
for b₁ being Function of G1,G3 st b₁ = g * f holds
b₁ is additive by Th14;

end;

definition

attr c₁ is strict ;
struct GroupMorphismStr -> ;
aggr GroupMorphismStr(# Source, Target, Fun #) -> GroupMorphismStr ;
sel Source c₁ -> AddGroup;
sel Target c₁ -> AddGroup;
sel Fun c₁ -> Function of the Source of c₁, the Target of c₁;

end;

definition

let f be GroupMorphismStr ;
func dom f -> AddGroup equals :: GRCAT_1:def 14
the Source of f;
coherence
the Source of f is AddGroup ;
func cod f -> AddGroup equals :: GRCAT_1:def 15
the Target of f;
coherence
the Target of f is AddGroup ;

end;

:: deftheorem defines dom GRCAT_1:def 14 :
for f being GroupMorphismStr holds dom f = the Source of f;

:: deftheorem defines cod GRCAT_1:def 15 :
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 16
the Fun of f;
coherence
the Fun of f is Function of (dom f),(cod f) ;

end;

:: deftheorem defines fun GRCAT_1:def 16 :
for f being GroupMorphismStr holds fun f = the Fun of f;

theorem :: GRCAT_1:15

canceled;

theorem :: GRCAT_1:16

canceled;

theorem :: GRCAT_1:17

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 17
GroupMorphismStr(# G,H,(ZeroMap (G,H)) #);
coherence
GroupMorphismStr(# G,H,(ZeroMap (G,H)) #) is GroupMorphismStr ;

end;

:: deftheorem defines ZERO GRCAT_1:def 17 :
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 ;
attr IT is GroupMorphism-like means :Def18: :: GRCAT_1:def 18
fun IT is additive ;

end;

:: deftheorem Def18 defines GroupMorphism-like GRCAT_1:def 18 :
for IT being GroupMorphismStr holds
( IT is GroupMorphism-like iff fun IT is additive );

registration

cluster strict GroupMorphism-like GroupMorphismStr ;
existence
ex b₁ being GroupMorphismStr st
( b₁ is strict & b₁ is GroupMorphism-like )

proof end;

end;

definition

mode GroupMorphism is GroupMorphism-like GroupMorphismStr ;

end;

theorem Th18: :: GRCAT_1:18

for F being GroupMorphism holds the Fun of F is additive

proof end;

registration

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

proof end;

end;

definition

let G, H be AddGroup;
mode Morphism of G,H -> GroupMorphism means :Def19: :: GRCAT_1:def 19
( dom it = G & cod it = H );
existence
ex b₁ being GroupMorphism st
( dom b₁ = G & cod b₁ = H )

proof end;

end;

:: deftheorem Def19 defines Morphism GRCAT_1:def 19 :
for G, H being AddGroup
for b₃ being GroupMorphism holds
( b₃ is Morphism of G,H iff ( dom b₃ = G & cod b₃ = H ) );

registration

let G, H be AddGroup;
cluster strict GroupMorphism-like Morphism of G,H;
existence
ex b₁ being Morphism of G,H st b₁ is strict

proof end;

end;

theorem Th19: :: GRCAT_1:19

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

proof end;

theorem Th20: :: GRCAT_1:20

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

proof end;

registration

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

proof end;

end;

definition

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

proof end;

end;

:: deftheorem defines ID GRCAT_1:def 20 :
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

proof end;

end;

theorem :: GRCAT_1:21

canceled;

theorem Th22: :: GRCAT_1:22

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 )

proof end;

theorem Th23: :: GRCAT_1:23

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 #)

proof end;

theorem Th24: :: GRCAT_1:24

for F being GroupMorphism ex G, H being AddGroup st F is Morphism of G,H

proof end;

theorem :: GRCAT_1:25

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 )

proof end;

theorem Th26: :: GRCAT_1:26

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 )

proof end;

definition

let G, F be GroupMorphism;
assume A1: dom G = cod F ;
func G * F -> strict GroupMorphism means :Def21: :: GRCAT_1:def 21
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 b₁ 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
b₁ = GroupMorphismStr(# G1,G3,(g * f) #)

proof end;

uniqueness
for b₁, b₂ 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
b₁ = 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
b₂ = GroupMorphismStr(# G1,G3,(g * f) #) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines * GRCAT_1:def 21 :
for G, F being GroupMorphism st dom G = cod F holds
for b₃ being strict GroupMorphism holds
( b₃ = 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
b₃ = GroupMorphismStr(# G1,G3,(g * f) #) );

theorem :: GRCAT_1:27

canceled;

theorem Th28: :: GRCAT_1:28

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

proof end;

definition

let G1, G2, G3 be AddGroup;
let G be Morphism of G2,G3;
let F be Morphism of G1,G2;
:: original: *
redefine func G * F -> strict Morphism of G1,G3;
coherence
G * F is strict Morphism of G1,G3 by Th28;

end;

theorem Th29: :: GRCAT_1:29

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) #)

proof end;

theorem Th30: :: GRCAT_1:30

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) #) )

proof end;

theorem Th31: :: GRCAT_1:31

for f, g being strict GroupMorphism st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g )

proof end;

theorem Th32: :: GRCAT_1:32

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

proof end;

theorem Th33: :: GRCAT_1:33

for f, g, h being strict GroupMorphism st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f

proof end;

theorem Th34: :: GRCAT_1:34

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 ) )

proof end;

definition

let IT be set ;
attr IT is Group_DOMAIN-like means :Def22: :: GRCAT_1:def 22
for x being set st x in IT holds
x is strict AddGroup;

end;

:: deftheorem Def22 defines Group_DOMAIN-like GRCAT_1:def 22 :
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 set ;
existence
ex b₁ being set st
( b₁ is Group_DOMAIN-like & not b₁ is empty )

proof end;

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 b₁ being Element of V holds b₁ is AddGroup by Def22;

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 Element of V;
existence
ex b₁ being Element of V st b₁ is strict

proof end;

end;

definition

let IT be set ;
attr IT is GroupMorphism_DOMAIN-like means :Def23: :: GRCAT_1:def 23
for x being set st x in IT holds
x is strict GroupMorphism;

end;

:: deftheorem Def23 defines GroupMorphism_DOMAIN-like GRCAT_1:def 23 :
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 set ;
existence
ex b₁ being set st
( b₁ is GroupMorphism_DOMAIN-like & not b₁ is empty )

proof end;

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 b₁ being Element of M holds b₁ is GroupMorphism by Def23;

end;

registration

let M be GroupMorphism_DOMAIN;
cluster strict GroupMorphism-like Element of M;
existence
ex b₁ being Element of M st b₁ is strict

proof end;

end;

theorem :: GRCAT_1:35

canceled;

theorem :: GRCAT_1:36

canceled;

theorem Th37: :: GRCAT_1:37

for f being strict GroupMorphism holds {f} is GroupMorphism_DOMAIN

proof end;

definition

let G, H be AddGroup;
mode GroupMorphism_DOMAIN of G,H -> GroupMorphism_DOMAIN means :Def24: :: GRCAT_1:def 24
for x being Element of it holds x is strict Morphism of G,H;
existence
ex b₁ being GroupMorphism_DOMAIN st
for x being Element of b₁ holds x is strict Morphism of G,H

proof end;

end;

:: deftheorem Def24 defines GroupMorphism_DOMAIN GRCAT_1:def 24 :
for G, H being AddGroup
for b₃ being GroupMorphism_DOMAIN holds
( b₃ is GroupMorphism_DOMAIN of G,H iff for x being Element of b₃ holds x is strict Morphism of G,H );

theorem Th38: :: GRCAT_1:38

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 )

proof end;

theorem :: GRCAT_1:39

for G, H being AddGroup
for f being strict Morphism of G,H holds {f} is GroupMorphism_DOMAIN of G,H

proof end;

definition

let G, H be 1-sorted ;
mode MapsSet of G,H -> set means :Def25: :: GRCAT_1:def 25
for x being set st x in it holds
x is Function of G,H;
existence
ex b₁ being set st
for x being set st x in b₁ holds
x is Function of G,H

proof end;

end;

:: deftheorem Def25 defines MapsSet GRCAT_1:def 25 :
for G, H being 1-sorted
for b₃ being set holds
( b₃ is MapsSet of G,H iff for x being set st x in b₃ 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 26
Funcs ( the carrier of G, the carrier of H);
coherence
Funcs ( the carrier of G, the carrier of H) is MapsSet of G,H

proof end;

end;

:: deftheorem defines Maps GRCAT_1:def 26 :
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 MapsSet of G,H;
existence
not for b₁ being MapsSet of G,H holds b₁ is empty

proof end;

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 b₁ being Element of M holds b₁ is Function of G,H by Def25;

end;

definition

let G, H be AddGroup;
func Morphs (G,H) -> GroupMorphism_DOMAIN of G,H means :Def27: :: GRCAT_1:def 27
for x being set holds
( x in it iff x is strict Morphism of G,H );
existence
ex b₁ being GroupMorphism_DOMAIN of G,H st
for x being set holds
( x in b₁ iff x is strict Morphism of G,H )

proof end;

uniqueness
for b₁, b₂ being GroupMorphism_DOMAIN of G,H st ( for x being set holds
( x in b₁ iff x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b₂ iff x is strict Morphism of G,H ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def27 defines Morphs GRCAT_1:def 27 :
for G, H being AddGroup
for b₃ being GroupMorphism_DOMAIN of G,H holds
( b₃ = Morphs (G,H) iff for x being set holds
( x in b₃ 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 b₁ being Element of M holds b₁ is Morphism of G,H by Def24;

end;

registration

let G, H be AddGroup;
let M be GroupMorphism_DOMAIN of G,H;
cluster strict GroupMorphism-like Element of M;
existence
ex b₁ being Element of M st b₁ is strict

proof end;

end;

definition

let x, y be set ;
pred GO x,y means :Def28: :: GRCAT_1:def 28
ex x1, x2, x3, x4 being set st
( x = [x1,x2,x3,x4] & ex G being strict AddGroup st
( y = G & x1 = the carrier of G & x2 = the addF of G & x3 = comp G & x4 = 0. G ) );

end;

:: deftheorem Def28 defines GO GRCAT_1:def 28 :
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 Th40: :: GRCAT_1:40

for x, y1, y2 being set st GO x,y1 & GO x,y2 holds
y1 = y2

proof end;

theorem Th41: :: GRCAT_1:41

for UN being Universe ex x being set st
( x in UN & GO x, Trivial-addLoopStr )

proof end;

definition

let UN be Universe;
func GroupObjects UN -> set means :Def29: :: GRCAT_1:def 29
for y being set holds
( y in it iff ex x being set st
( x in UN & GO x,y ) );
existence
ex b₁ being set st
for y being set holds
( y in b₁ iff ex x being set st
( x in UN & GO x,y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for y being set holds
( y in b₁ iff ex x being set st
( x in UN & GO x,y ) ) ) & ( for y being set holds
( y in b₂ iff ex x being set st
( x in UN & GO x,y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def29 defines GroupObjects GRCAT_1:def 29 :
for UN being Universe
for b₂ being set holds
( b₂ = GroupObjects UN iff for y being set holds
( y in b₂ iff ex x being set st
( x in UN & GO x,y ) ) );

theorem Th42: :: GRCAT_1:42

for UN being Universe holds Trivial-addLoopStr in GroupObjects UN

proof end;

registration

let UN be Universe;
cluster GroupObjects UN -> non empty ;
coherence
not GroupObjects UN is empty by Th42;

end;

theorem Th43: :: GRCAT_1:43

for UN being Universe
for x being Element of GroupObjects UN holds x is strict AddGroup

proof end;

registration

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

proof end;

end;

definition

let V be Group_DOMAIN;
func Morphs V -> GroupMorphism_DOMAIN means :Def30: :: GRCAT_1:def 30
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 b₁ being GroupMorphism_DOMAIN st
for x being set holds
( x in b₁ iff ex G, H being strict Element of V st x is strict Morphism of G,H )

proof end;

uniqueness
for b₁, b₂ being GroupMorphism_DOMAIN st ( for x being set holds
( x in b₁ iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) & ( for x being set holds
( x in b₂ iff ex G, H being strict Element of V st x is strict Morphism of G,H ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def30 defines Morphs GRCAT_1:def 30 :
for V being Group_DOMAIN
for b₂ being GroupMorphism_DOMAIN holds
( b₂ = Morphs V iff for x being set holds
( x in b₂ iff ex G, H being strict Element of V st x is strict Morphism of G,H ) );

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

proof end;

:: original: cod
redefine func cod F -> strict Element of V;
coherence
cod F is strict Element of V

proof end;

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 31
ID G;
coherence
ID G is strict Element of Morphs V

proof end;

end;

:: deftheorem defines ID GRCAT_1:def 31 :
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 :Def32: :: GRCAT_1:def 32
for f being Element of Morphs V holds it . f = dom f;
existence
ex b₁ being Function of (Morphs V),V st
for f being Element of Morphs V holds b₁ . f = dom f

proof end;

uniqueness
for b₁, b₂ being Function of (Morphs V),V st ( for f being Element of Morphs V holds b₁ . f = dom f ) & ( for f being Element of Morphs V holds b₂ . f = dom f ) holds
b₁ = b₂

proof end;

func cod V -> Function of (Morphs V),V means :Def33: :: GRCAT_1:def 33
for f being Element of Morphs V holds it . f = cod f;
existence
ex b₁ being Function of (Morphs V),V st
for f being Element of Morphs V holds b₁ . f = cod f

proof end;

uniqueness
for b₁, b₂ being Function of (Morphs V),V st ( for f being Element of Morphs V holds b₁ . f = cod f ) & ( for f being Element of Morphs V holds b₂ . f = cod f ) holds
b₁ = b₂

proof end;

func ID V -> Function of V,(Morphs V) means :Def34: :: GRCAT_1:def 34
for G being Element of V holds it . G = ID G;
existence
ex b₁ being Function of V,(Morphs V) st
for G being Element of V holds b₁ . G = ID G

proof end;

uniqueness
for b₁, b₂ being Function of V,(Morphs V) st ( for G being Element of V holds b₁ . G = ID G ) & ( for G being Element of V holds b₂ . G = ID G ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def32 defines dom GRCAT_1:def 32 :
for V being Group_DOMAIN
for b₂ being Function of (Morphs V),V holds
( b₂ = dom V iff for f being Element of Morphs V holds b₂ . f = dom f );

:: deftheorem Def33 defines cod GRCAT_1:def 33 :
for V being Group_DOMAIN
for b₂ being Function of (Morphs V),V holds
( b₂ = cod V iff for f being Element of Morphs V holds b₂ . f = cod f );

:: deftheorem Def34 defines ID GRCAT_1:def 34 :
for V being Group_DOMAIN
for b₂ being Function of V,(Morphs V) holds
( b₂ = ID V iff for G being Element of V holds b₂ . G = ID G );

theorem Th44: :: GRCAT_1:44

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 )

proof end;

theorem Th45: :: GRCAT_1:45

for V being Group_DOMAIN
for g, f being Element of Morphs V st dom g = cod f holds
g * f in Morphs V

proof end;

definition

let V be Group_DOMAIN;
func comp V -> PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) means :Def35: :: GRCAT_1:def 35
( ( for g, f being Element of Morphs V holds
( [g,f] in dom it iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom it holds
it . (g,f) = g * f ) );
existence
ex b₁ being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st
( ( for g, f being Element of Morphs V holds
( [g,f] in dom b₁ iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b₁ holds
b₁ . (g,f) = g * f ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) st ( for g, f being Element of Morphs V holds
( [g,f] in dom b₁ iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b₁ holds
b₁ . (g,f) = g * f ) & ( for g, f being Element of Morphs V holds
( [g,f] in dom b₂ iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b₂ holds
b₂ . (g,f) = g * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def35 defines comp GRCAT_1:def 35 :
for V being Group_DOMAIN
for b₂ being PartFunc of [:(Morphs V),(Morphs V):],(Morphs V) holds
( b₂ = comp V iff ( ( for g, f being Element of Morphs V holds
( [g,f] in dom b₂ iff dom g = cod f ) ) & ( for g, f being Element of Morphs V st [g,f] in dom b₂ holds
b₂ . (g,f) = g * f ) ) );

definition

let UN be Universe;
func GroupCat UN -> CatStr equals :: GRCAT_1:def 36
CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)),(ID (GroupObjects UN)) #);
coherence
CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)),(ID (GroupObjects UN)) #) is CatStr ;

end;

:: deftheorem defines GroupCat GRCAT_1:def 36 :
for UN being Universe holds GroupCat UN = CatStr(# (GroupObjects UN),(Morphs (GroupObjects UN)),(dom (GroupObjects UN)),(cod (GroupObjects UN)),(comp (GroupObjects UN)),(ID (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 Th46: :: GRCAT_1:46

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 )

proof end;

theorem Th47: :: GRCAT_1:47

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) )

proof end;

theorem Th48: :: GRCAT_1:48

for UN being Universe
for b being Object of (GroupCat UN)
for b9 being Element of GroupObjects UN st b = b9 holds
id b = ID b9

proof end;

theorem :: GRCAT_1:49

canceled;

theorem Th50: :: GRCAT_1:50

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 ) )

proof end;

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 )

proof end;

Lm2: for UN being Universe
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 end;

Lm3: for UN being Universe
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 end;

registration

let UN be Universe;
cluster GroupCat UN -> Category-like ;
coherence
GroupCat UN is Category-like

proof end;

end;

definition

let UN be Universe;
func AbGroupObjects UN -> Subset of the carrier of (GroupCat UN) equals :: GRCAT_1:def 37
{ 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)

proof end;

end;

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

theorem Th51: :: GRCAT_1:51

for UN being Universe holds Trivial-addLoopStr in AbGroupObjects UN

proof end;

registration

let UN be Universe;
cluster AbGroupObjects UN -> non empty ;
coherence
not AbGroupObjects UN is empty by Th51;

end;

definition

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

end;

:: deftheorem defines AbGroupCat GRCAT_1:def 38 :
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:52

for UN being Universe holds the carrier of (AbGroupCat UN) = AbGroupObjects UN ;

definition

let UN be Universe;
func MidOpGroupObjects UN -> Subset of the carrier of (AbGroupCat UN) equals :: GRCAT_1:def 39
{ 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)

proof end;

end;

:: deftheorem defines MidOpGroupObjects GRCAT_1:def 39 :
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

proof end;

end;

definition

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

end;

:: deftheorem defines MidOpGroupCat GRCAT_1:def 40 :
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:53

for UN being Universe holds the carrier of (MidOpGroupCat UN) = MidOpGroupObjects UN ;

theorem :: GRCAT_1:54

for UN being Universe holds Trivial-addLoopStr in MidOpGroupObjects UN

proof end;

theorem :: GRCAT_1:55

canceled;

theorem :: GRCAT_1:56

for S, T being non empty 1-sorted
for f being Function of S,T st f is one-to-one & f is onto holds
( f * (f ") = id T & (f ") * f = id S & f " is one-to-one & f " is onto )

proof end;