:: GRCAT_1 semantic presentation

theorem Th1: :: GRCAT_1:1

canceled;

theorem Th2: :: GRCAT_1:2

for b₁, b₂, b₃, b₄ being set st b₄ in b₃ & b₃ c= [:b₁,b₂:] holds
ex b₅ being Element of b₁ex b₆ being Element of b₂ st b₄ = [b₅,b₆]

proof end;

theorem Th3: :: GRCAT_1:3

for b₁ being Universe
for b₂, b₃, b₄, b₅ being Element of b₁ holds
( [b₂,b₃,b₄] is Element of b₁ & [b₂,b₃,b₄,b₅] is Element of b₁ )

proof end;

theorem Th4: :: GRCAT_1:4

for b₁ being Universe
for b₂, b₃ being set st b₂ in b₃ & b₃ in b₁ holds
b₂ in b₁

proof end;

scheme :: GRCAT_1:sch 1
s1{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

ex b₁ being PartFunc of [:F₁(),F₂():],F₃() st
( ( for b₂, b₃ being set holds
( [b₂,b₃] in dom b₁ iff ( b₂ in F₁() & b₃ in F₂() & P₁[b₂,b₃] ) ) ) & ( for b₂, b₃ being set st [b₂,b₃] in dom b₁ holds
b₁ . [b₂,b₃] = F₄(b₂,b₃) ) )

provided

E4: for b₁, b₂ being set st b₁ in F₁() & b₂ in F₂() & P₁[b₁,b₂] holds
F₄(b₁,b₂) in F₃()

proof end;

scheme :: GRCAT_1:sch 2
s2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> set , F₄( set , set ) -> set , P₁[ set , set ] } :

ex b₁ being PartFunc of [:F₁(),F₂():],F₃() st
( ( for b₂ being Element of F₁()
for b₃ being Element of F₂() holds
( [b₂,b₃] in dom b₁ iff P₁[b₂,b₃] ) ) & ( for b₂ being Element of F₁()
for b₃ being Element of F₂() st [b₂,b₃] in dom b₁ holds
b₁ . [b₂,b₃] = F₄(b₂,b₃) ) )

provided

E4: for b₁ being Element of F₁()
for b₂ being Element of F₂() st P₁[b₁,b₂] holds
F₄(b₁,b₂) in F₃()

proof end;

theorem Th5: :: GRCAT_1:5

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

proof end;

theorem Th6: :: GRCAT_1:6

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

proof end;

theorem Th7: :: GRCAT_1:7

LoopStr(# {{} },op2 ,(Extract {} ) #) is midpoint_operator

proof end;

registration

cluster L_Trivial -> midpoint_operator ;
coherence by Th7, ALGSTR_1:def 4;

end;

theorem Th8: :: GRCAT_1:8

( ( for b₁ being Element of L_Trivial holds b₁ = {} ) & ( for b₁, b₂ being Element of L_Trivial holds b₁ + b₂ = {} ) & ( for b₁ being Element of L_Trivial holds - b₁ = {} ) & 0. L_Trivial = {} ) by ALGSTR_1:def 4, TARSKI:def 1;

definition

let c₁ be Category;
let c₂ be non empty Subset of the Objects of c₁;
canceled;
canceled;
canceled;
canceled;
func Morphs c₂ -> Subset of the Morphisms of a₁ equals :: GRCAT_1:def 5
union { (Hom b₁,b₂) where B is Object of a₁, B is Object of a₁ : ( b₁ in a₂ & b₂ in a₂ ) } ;
coherence by CAT_2:28;

end;

:: deftheorem Def1 GRCAT_1:def 1 :

:: deftheorem Def2 GRCAT_1:def 2 :

:: deftheorem Def3 GRCAT_1:def 3 :

:: deftheorem Def4 GRCAT_1:def 4 :

:: deftheorem Def5 defines Morphs GRCAT_1:def 5 :

registration

let c₁ be Category;
let c₂ be non empty Subset of the Objects of c₁;
cluster Morphs a₂ -> non empty ;
coherence by CAT_2:28;

end;

definition

let c₁ be Category;
let c₂ be non empty Subset of the Objects of c₁;
func dom c₂ -> Function of Morphs a₂,a₂ equals :: GRCAT_1:def 6
the Dom of a₁ | (Morphs a₂);
coherence by CAT_2:29;
func cod c₂ -> Function of Morphs a₂,a₂ equals :: GRCAT_1:def 7
the Cod of a₁ | (Morphs a₂);
coherence by CAT_2:29;
func comp c₂ -> PartFunc of [:(Morphs a₂),(Morphs a₂):], Morphs a₂ equals :: GRCAT_1:def 8
the Comp of a₁ || (Morphs a₂);
coherence by CAT_2:29;
func ID c₂ -> Function of a₂, Morphs a₂ equals :: GRCAT_1:def 9
the Id of a₁ | a₂;
coherence by CAT_2:29;

end;

:: deftheorem Def6 defines dom GRCAT_1:def 6 :

:: deftheorem Def7 defines cod GRCAT_1:def 7 :

:: deftheorem Def8 defines comp GRCAT_1:def 8 :

:: deftheorem Def9 defines ID GRCAT_1:def 9 :

theorem Th9: :: GRCAT_1:9

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁ holds CatStr(# b₂,(Morphs b₂),(dom b₂),(cod b₂),(comp b₂),(ID b₂) #) is_full_subcategory_of b₁ by CAT_2:30;

definition

let c₁ be Category;
let c₂ be non empty Subset of the Objects of c₁;
func cat c₂ -> Subcategory of a₁ equals :: GRCAT_1:def 10
CatStr(# a₂,(Morphs a₂),(dom a₂),(cod a₂),(comp a₂),(ID a₂) #);
coherence

proof end;

end;

:: deftheorem Def10 defines cat GRCAT_1:def 10 :

registration

let c₁ be Category;
let c₂ be non empty Subset of the Objects of c₁;
cluster cat a₂ -> strict ;
coherence ;

end;

theorem Th10: :: GRCAT_1:10

for b₁ being Category
for b₂ being non empty Subset of the Objects of b₁ holds the Objects of (cat b₂) = b₂ ;

definition

let c₁ be 1-sorted ;
func id c₁ -> Function of a₁,a₁ equals :: GRCAT_1:def 11
id the carrier of a₁;
coherence ;

end;

:: deftheorem Def11 defines id GRCAT_1:def 11 :

theorem Th11: :: GRCAT_1:11

for b₁ being non empty 1-sorted
for b₂ being Element of b₁ holds (id b₁) . b₂ = b₂ by FUNCT_1:35;

theorem Th12: :: GRCAT_1:12

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂ holds
( b₃ * (id b₁) = b₃ & (id b₂) * b₃ = b₃ )

proof end;

definition

let c₁, c₂ be non empty ZeroStr ;
func ZeroMap c₁,c₂ -> Function of a₁,a₂ equals :: GRCAT_1:def 12
the carrier of a₁ --> (0. a₂);
coherence

proof end;

end;

:: deftheorem Def12 defines ZeroMap GRCAT_1:def 12 :

definition

let c₁, c₂ be non empty LoopStr ;
let c₃ be Function of c₁,c₂;
attr a₃ is additive means :Def13: :: GRCAT_1:def 13
for b₁, b₂ being Element of a₁ holds a₃ . (b₁ + b₂) = (a₃ . b₁) + (a₃ . b₂);

end;

:: deftheorem Def13 defines additive GRCAT_1:def 13 :

theorem Th13: :: GRCAT_1:13

comp L_Trivial = op1

proof end;

theorem Th14: :: GRCAT_1:14

for b₁, b₂, b₃ being non empty LoopStr
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is additive & b₅ is additive holds
b₅ * b₄ is additive

proof end;

theorem Th15: :: GRCAT_1:15

for b₁ being non empty ZeroStr
for b₂ being non empty LoopStr
for b₃ being Element of b₁ holds (ZeroMap b₁,b₂) . b₃ = 0. b₂ by FUNCOP_1:13;

theorem Th16: :: GRCAT_1:16

for b₁ being non empty LoopStr
for b₂ being non empty right_zeroed LoopStr holds ZeroMap b₁,b₂ is additive

proof end;

definition

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

end;

definition

let c₁ be GroupMorphismStr ;
func dom c₁ -> AddGroup equals :: GRCAT_1:def 14
the Dom of a₁;
coherence ;
func cod c₁ -> AddGroup equals :: GRCAT_1:def 15
the Cod of a₁;
coherence ;

end;

:: deftheorem Def14 defines dom GRCAT_1:def 14 :

:: deftheorem Def15 defines cod GRCAT_1:def 15 :

definition

let c₁ be GroupMorphismStr ;
func fun c₁ -> Function of (dom a₁),(cod a₁) equals :: GRCAT_1:def 16
the Fun of a₁;
coherence ;

end;

:: deftheorem Def16 defines fun GRCAT_1:def 16 :

theorem Th17: :: GRCAT_1:17

for b₁ being GroupMorphismStr
for b₂, b₃ being AddGroup
for b₄ being Function of b₂,b₃ st b₁ = GroupMorphismStr(# b₂,b₃,b₄ #) holds
( dom b₁ = b₂ & cod b₁ = b₃ & fun b₁ = b₄ ) ;

definition

let c₁, c₂ be AddGroup;
func ZERO c₁,c₂ -> GroupMorphismStr equals :: GRCAT_1:def 17
GroupMorphismStr(# a₁,a₂,(ZeroMap a₁,a₂) #);
coherence ;

end;

:: deftheorem Def17 defines ZERO GRCAT_1:def 17 :

registration

let c₁, c₂ be AddGroup;
cluster ZERO a₁,a₂ -> strict ;
coherence ;

end;

definition

let c₁ be GroupMorphismStr ;
attr a₁ is GroupMorphism-like means :Def18: :: GRCAT_1:def 18
fun a₁ is additive;

end;

:: deftheorem Def18 defines GroupMorphism-like GRCAT_1:def 18 :

registration

cluster strict GroupMorphism-like GroupMorphismStr ;
existence

proof end;

end;

definition

mode GroupMorphism is GroupMorphism-like GroupMorphismStr ;

end;

theorem Th18: :: GRCAT_1:18

for b₁ being GroupMorphism holds the Fun of b₁ is additive

proof end;

registration

let c₁, c₂ be AddGroup;
cluster ZERO a₁,a₂ -> strict GroupMorphism-like ;
coherence

proof end;

end;

definition

let c₁, c₂ be AddGroup;
mode Morphism of c₁,c₂ -> GroupMorphism means :Def19: :: GRCAT_1:def 19
( dom a₃ = a₁ & cod a₃ = a₂ );
existence

proof end;

end;

:: deftheorem Def19 defines Morphism GRCAT_1:def 19 :

registration

let c₁, c₂ be AddGroup;
cluster strict Morphism of a₁,a₂;
existence

proof end;

end;

theorem Th19: :: GRCAT_1:19

for b₁, b₂ being AddGroup
for b₃ being strict GroupMorphismStr st dom b₃ = b₁ & cod b₃ = b₂ & fun b₃ is additive holds
b₃ is strict Morphism of b₁,b₂

proof end;

theorem Th20: :: GRCAT_1:20

for b₁, b₂ being AddGroup
for b₃ being Function of b₁,b₂ st b₃ is additive holds
GroupMorphismStr(# b₁,b₂,b₃ #) is strict Morphism of b₁,b₂

proof end;

theorem Th21: :: GRCAT_1:21

for b₁ being non empty LoopStr holds id b₁ is additive

proof end;

definition

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

proof end;

end;

:: deftheorem Def20 defines ID GRCAT_1:def 20 :

registration

let c₁ be AddGroup;
cluster ID a₁ -> strict ;
coherence ;

end;

definition

let c₁, c₂ be AddGroup;
redefine func ZERO as ZERO c₁,c₂ -> strict Morphism of a₁,a₂;
coherence

proof end;

end;

theorem Th22: :: GRCAT_1:22

for b₁, b₂ being AddGroup
for b₃ being Morphism of b₁,b₂ ex b₄ being Function of b₁,b₂ st
( GroupMorphismStr(# the Dom of b₃,the Cod of b₃,the Fun of b₃ #) = GroupMorphismStr(# b₁,b₂,b₄ #) & b₄ is additive )

proof end;

theorem Th23: :: GRCAT_1:23

for b₁, b₂ being AddGroup
for b₃ being strict Morphism of b₁,b₂ ex b₄ being Function of b₁,b₂ st b₃ = GroupMorphismStr(# b₁,b₂,b₄ #)

proof end;

theorem Th24: :: GRCAT_1:24

for b₁ being GroupMorphism ex b₂, b₃ being AddGroup st b₁ is Morphism of b₂,b₃

proof end;

theorem Th25: :: GRCAT_1:25

for b₁ being strict GroupMorphism ex b₂, b₃ being AddGroupex b₄ being Function of b₂,b₃ st
( b₁ is Morphism of b₂,b₃ & b₁ = GroupMorphismStr(# b₂,b₃,b₄ #) & b₄ is additive )

proof end;

theorem Th26: :: GRCAT_1:26

for b₁, b₂ being GroupMorphism st dom b₁ = cod b₂ holds
ex b₃, b₄, b₅ being AddGroup st
( b₁ is Morphism of b₄,b₅ & b₂ is Morphism of b₃,b₄ )

proof end;

definition

let c₁, c₂ be GroupMorphism;
assume E25: dom c₁ = cod c₂ ;
func c₁ * c₂ -> strict GroupMorphism means :Def21: :: GRCAT_1:def 21
for b₁, b₂, b₃ being AddGroup
for b₄ being Function of b₂,b₃
for b₅ being Function of b₁,b₂ st GroupMorphismStr(# the Dom of a₁,the Cod of a₁,the Fun of a₁ #) = GroupMorphismStr(# b₂,b₃,b₄ #) & GroupMorphismStr(# the Dom of a₂,the Cod of a₂,the Fun of a₂ #) = GroupMorphismStr(# b₁,b₂,b₅ #) holds
a₃ = GroupMorphismStr(# b₁,b₃,(b₄ * b₅) #);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines * GRCAT_1:def 21 :

theorem Th27: :: GRCAT_1:27

canceled;

theorem Th28: :: GRCAT_1:28

for b₁, b₂, b₃ being AddGroup
for b₄ being Morphism of b₂,b₃
for b₅ being Morphism of b₁,b₂ holds b₄ * b₅ is Morphism of b₁,b₃

proof end;

definition

let c₁, c₂, c₃ be AddGroup;
let c₄ be Morphism of c₂,c₃;
let c₅ be Morphism of c₁,c₂;
redefine func * as c₄ * c₅ -> strict Morphism of a₁,a₃;
coherence by Th28;

end;

theorem Th29: :: GRCAT_1:29

for b₁, b₂, b₃ being AddGroup
for b₄ being Morphism of b₂,b₃
for b₅ being Morphism of b₁,b₂
for b₆ being Function of b₂,b₃
for b₇ being Function of b₁,b₂ st b₄ = GroupMorphismStr(# b₂,b₃,b₆ #) & b₅ = GroupMorphismStr(# b₁,b₂,b₇ #) holds
b₄ * b₅ = GroupMorphismStr(# b₁,b₃,(b₆ * b₇) #)

proof end;

theorem Th30: :: GRCAT_1:30

for b₁, b₂ being strict GroupMorphism st dom b₂ = cod b₁ holds
ex b₃, b₄, b₅ being AddGroupex b₆ being Function of b₃,b₄ex b₇ being Function of b₄,b₅ st
( b₁ = GroupMorphismStr(# b₃,b₄,b₆ #) & b₂ = GroupMorphismStr(# b₄,b₅,b₇ #) & b₂ * b₁ = GroupMorphismStr(# b₃,b₅,(b₇ * b₆) #) )

proof end;

theorem Th31: :: GRCAT_1:31

for b₁, b₂ being strict GroupMorphism st dom b₂ = cod b₁ holds
( dom (b₂ * b₁) = dom b₁ & cod (b₂ * b₁) = cod b₂ )

proof end;

theorem Th32: :: GRCAT_1:32

for b₁, b₂, b₃, b₄ being AddGroup
for b₅ being strict Morphism of b₁,b₂
for b₆ being strict Morphism of b₂,b₃
for b₇ being strict Morphism of b₃,b₄ holds b₇ * (b₆ * b₅) = (b₇ * b₆) * b₅

proof end;

theorem Th33: :: GRCAT_1:33

for b₁, b₂, b₃ being strict GroupMorphism st dom b₃ = cod b₂ & dom b₂ = cod b₁ holds
b₃ * (b₂ * b₁) = (b₃ * b₂) * b₁

proof end;

theorem Th34: :: GRCAT_1:34

for b₁ being AddGroup holds
( dom (ID b₁) = b₁ & cod (ID b₁) = b₁ & ( for b₂ being strict GroupMorphism st cod b₂ = b₁ holds
(ID b₁) * b₂ = b₂ ) & ( for b₂ being strict GroupMorphism st dom b₂ = b₁ holds
b₂ * (ID b₁) = b₂ ) )

proof end;

definition

let c₁ be set ;
attr a₁ is Group_DOMAIN-like means :Def22: :: GRCAT_1:def 22
for b₁ being set st b₁ in a₁ holds
b₁ is strict AddGroup;

end;

:: deftheorem Def22 defines Group_DOMAIN-like GRCAT_1:def 22 :

registration

cluster non empty Group_DOMAIN-like set ;
existence

proof end;

end;

definition

mode Group_DOMAIN is non empty Group_DOMAIN-like set ;

end;

definition

let c₁ be Group_DOMAIN;
redefine mode Element as Element of c₁ -> AddGroup;
coherence by Def22;

end;

registration

let c₁ be Group_DOMAIN;
cluster strict Element of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
attr a₁ is GroupMorphism_DOMAIN-like means :Def23: :: GRCAT_1:def 23
for b₁ being set st b₁ in a₁ holds
b₁ is strict GroupMorphism;

end;

:: deftheorem Def23 defines GroupMorphism_DOMAIN-like GRCAT_1:def 23 :

registration

cluster non empty GroupMorphism_DOMAIN-like set ;
existence

proof end;

end;

definition

mode GroupMorphism_DOMAIN is non empty GroupMorphism_DOMAIN-like set ;

end;

definition

let c₁ be GroupMorphism_DOMAIN;
redefine mode Element as Element of c₁ -> GroupMorphism;
coherence by Def23;

end;

registration

let c₁ be GroupMorphism_DOMAIN;
cluster strict Element of a₁;
existence

proof end;

end;

theorem Th35: :: GRCAT_1:35

canceled;

theorem Th36: :: GRCAT_1:36

canceled;

theorem Th37: :: GRCAT_1:37

for b₁ being strict GroupMorphism holds {b₁} is GroupMorphism_DOMAIN

proof end;

definition

let c₁, c₂ be AddGroup;
mode GroupMorphism_DOMAIN of c₁,c₂ -> GroupMorphism_DOMAIN means :Def24: :: GRCAT_1:def 24
for b₁ being Element of a₃ holds b₁ is strict Morphism of a₁,a₂;
existence

proof end;

end;

:: deftheorem Def24 defines GroupMorphism_DOMAIN GRCAT_1:def 24 :

theorem Th38: :: GRCAT_1:38

for b₁ being non empty set
for b₂, b₃ being AddGroup holds
( b₁ is GroupMorphism_DOMAIN of b₂,b₃ iff for b₄ being Element of b₁ holds b₄ is strict Morphism of b₂,b₃ )

proof end;

theorem Th39: :: GRCAT_1:39

for b₁, b₂ being AddGroup
for b₃ being strict Morphism of b₁,b₂ holds {b₃} is GroupMorphism_DOMAIN of b₁,b₂

proof end;

definition

let c₁, c₂ be 1-sorted ;
mode MapsSet of c₁,c₂ -> set means :Def25: :: GRCAT_1:def 25
for b₁ being set st b₁ in a₃ holds
b₁ is Function of a₁,a₂;
existence

proof end;

end;

:: deftheorem Def25 defines MapsSet GRCAT_1:def 25 :

definition

let c₁, c₂ be 1-sorted ;
func Maps c₁,c₂ -> MapsSet of a₁,a₂ equals :: GRCAT_1:def 26
Funcs the carrier of a₁,the carrier of a₂;
coherence

proof end;

end;

:: deftheorem Def26 defines Maps GRCAT_1:def 26 :

registration

let c₁ be 1-sorted ;
let c₂ be non empty 1-sorted ;
cluster Maps a₁,a₂ -> non empty ;
coherence ;

end;

registration

let c₁ be 1-sorted ;
let c₂ be non empty 1-sorted ;
cluster non empty MapsSet of a₁,a₂;
existence

proof end;

end;

definition

let c₁ be 1-sorted ;
let c₂ be non empty 1-sorted ;
let c₃ be non empty MapsSet of c₁,c₂;
redefine mode Element as Element of c₃ -> Function of a₁,a₂;
coherence by Def25;

end;

definition

let c₁, c₂ be AddGroup;
func Morphs c₁,c₂ -> GroupMorphism_DOMAIN of a₁,a₂ means :Def27: :: GRCAT_1:def 27
for b₁ being set holds
( b₁ in a₃ iff b₁ is strict Morphism of a₁,a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines Morphs GRCAT_1:def 27 :

definition

let c₁, c₂ be AddGroup;
let c₃ be GroupMorphism_DOMAIN of c₁,c₂;
redefine mode Element as Element of c₃ -> Morphism of a₁,a₂;
coherence by Def24;

end;

registration

let c₁, c₂ be AddGroup;
let c₃ be GroupMorphism_DOMAIN of c₁,c₂;
cluster strict Element of a₃;
existence

proof end;

end;

definition

let c₁, c₂ be set ;
pred GO c₁,c₂ means :Def28: :: GRCAT_1:def 28
ex b₁, b₂, b₃, b₄ being set st
( a₁ = [b₁,b₂,b₃,b₄] & ex b₅ being strict AddGroup st
( a₂ = b₅ & b₁ = the carrier of b₅ & b₂ = the add of b₅ & b₃ = comp b₅ & b₄ = the Zero of b₅ ) );

end;

:: deftheorem Def28 defines GO GRCAT_1:def 28 :

theorem Th40: :: GRCAT_1:40

for b₁, b₂, b₃ being set st GO b₁,b₂ & GO b₁,b₃ holds
b₂ = b₃

proof end;

theorem Th41: :: GRCAT_1:41

for b₁ being Universe ex b₂ being set st
( b₂ in b₁ & GO b₂, L_Trivial )

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines GroupObjects GRCAT_1:def 29 :

theorem Th42: :: GRCAT_1:42

for b₁ being Universe holds L_Trivial in GroupObjects b₁

proof end;

registration

let c₁ be Universe;
cluster GroupObjects a₁ -> non empty ;
coherence by Th42;

end;

theorem Th43: :: GRCAT_1:43

for b₁ being Universe
for b₂ being Element of GroupObjects b₁ holds b₂ is strict AddGroup

proof end;

registration

let c₁ be Universe;
cluster GroupObjects a₁ -> non empty Group_DOMAIN-like ;
coherence

proof end;

end;

definition

let c₁ be Group_DOMAIN;
func Morphs c₁ -> GroupMorphism_DOMAIN means :Def30: :: GRCAT_1:def 30
for b₁ being set holds
( b₁ in a₂ iff ex b₂, b₃ being strict Element of a₁ st b₁ is strict Morphism of b₂,b₃ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def30 defines Morphs GRCAT_1:def 30 :

definition

let c₁ be Group_DOMAIN;
let c₂ be Element of Morphs c₁;
redefine func dom as dom c₂ -> strict Element of a₁;
coherence

proof end;

redefine func cod as cod c₂ -> strict Element of a₁;
coherence

proof end;

end;

definition

let c₁ be Group_DOMAIN;
let c₂ be Element of c₁;
func ID c₂ -> strict Element of Morphs a₁ equals :: GRCAT_1:def 31
ID a₂;
coherence

proof end;

end;

:: deftheorem Def31 defines ID GRCAT_1:def 31 :

definition

let c₁ be Group_DOMAIN;
func dom c₁ -> Function of Morphs a₁,a₁ means :Def32: :: GRCAT_1:def 32
for b₁ being Element of Morphs a₁ holds a₂ . b₁ = dom b₁;
existence

proof end;

uniqueness

proof end;

func cod c₁ -> Function of Morphs a₁,a₁ means :Def33: :: GRCAT_1:def 33
for b₁ being Element of Morphs a₁ holds a₂ . b₁ = cod b₁;
existence

proof end;

uniqueness

proof end;

func ID c₁ -> Function of a₁, Morphs a₁ means :Def34: :: GRCAT_1:def 34
for b₁ being Element of a₁ holds a₂ . b₁ = ID b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def32 defines dom GRCAT_1:def 32 :

:: deftheorem Def33 defines cod GRCAT_1:def 33 :

:: deftheorem Def34 defines ID GRCAT_1:def 34 :

theorem Th44: :: GRCAT_1:44

for b₁ being Group_DOMAIN
for b₂, b₃ being Element of Morphs b₁ st dom b₂ = cod b₃ holds
ex b₄, b₅, b₆ being strict Element of b₁ st
( b₂ is Morphism of b₅,b₆ & b₃ is Morphism of b₄,b₅ )

proof end;

theorem Th45: :: GRCAT_1:45

for b₁ being Group_DOMAIN
for b₂, b₃ being Element of Morphs b₁ st dom b₂ = cod b₃ holds
b₂ * b₃ in Morphs b₁

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def35 defines comp GRCAT_1:def 35 :

definition

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

end;

:: deftheorem Def36 defines GroupCat GRCAT_1:def 36 :

registration

let c₁ be Universe;
cluster GroupCat a₁ -> strict ;
coherence ;

end;

theorem Th46: :: GRCAT_1:46

for b₁ being Universe
for b₂, b₃ being Morphism of (GroupCat b₁) holds
( [b₃,b₂] in dom the Comp of (GroupCat b₁) iff dom b₃ = cod b₂ )

proof end;

theorem Th47: :: GRCAT_1:47

for b₁ being Universe
for b₂ being Morphism of (GroupCat b₁)
for b₃ being Element of Morphs (GroupObjects b₁)
for b₄ being Object of (GroupCat b₁)
for b₅ being Element of GroupObjects b₁ holds
( b₂ is strict Element of Morphs (GroupObjects b₁) & b₃ is Morphism of (GroupCat b₁) & b₄ is strict Element of GroupObjects b₁ & b₅ is Object of (GroupCat b₁) )

proof end;

theorem Th48: :: GRCAT_1:48

for b₁ being Universe
for b₂ being Object of (GroupCat b₁)
for b₃ being Element of GroupObjects b₁ st b₂ = b₃ holds
id b₂ = ID b₃

proof end;

theorem Th49: :: GRCAT_1:49

for b₁ being Universe
for b₂ being Morphism of (GroupCat b₁)
for b₃ being Element of Morphs (GroupObjects b₁) st b₂ = b₃ holds
( dom b₂ = dom b₃ & cod b₂ = cod b₃ )

proof end;

theorem Th50: :: GRCAT_1:50

for b₁ being Universe
for b₂, b₃ being Morphism of (GroupCat b₁)
for b₄, b₅ being Element of Morphs (GroupObjects b₁) st b₂ = b₄ & b₃ = b₅ holds
( ( dom b₃ = cod b₂ implies dom b₅ = cod b₄ ) & ( dom b₅ = cod b₄ implies dom b₃ = cod b₂ ) & ( dom b₃ = cod b₂ implies [b₅,b₄] in dom (comp (GroupObjects b₁)) ) & ( [b₅,b₄] in dom (comp (GroupObjects b₁)) implies dom b₃ = cod b₂ ) & ( dom b₃ = cod b₂ implies b₃ * b₂ = b₅ * b₄ ) & ( dom b₂ = dom b₃ implies dom b₄ = dom b₅ ) & ( dom b₄ = dom b₅ implies dom b₂ = dom b₃ ) & ( cod b₂ = cod b₃ implies cod b₄ = cod b₅ ) & ( cod b₄ = cod b₅ implies cod b₂ = cod b₃ ) )

proof end;

Lemma58: for b₁ being Universe
for b₂, b₃ being Morphism of (GroupCat b₁) st dom b₃ = cod b₂ holds
( dom (b₃ * b₂) = dom b₂ & cod (b₃ * b₂) = cod b₃ )

proof end;

Lemma59: for b₁ being Universe
for b₂, b₃, b₄ being Morphism of (GroupCat b₁) st dom b₄ = cod b₃ & dom b₃ = cod b₂ holds
b₄ * (b₃ * b₂) = (b₄ * b₃) * b₂

proof end;

Lemma60: for b₁ being Universe
for b₂ being Object of (GroupCat b₁) holds
( dom (id b₂) = b₂ & cod (id b₂) = b₂ & ( for b₃ being Morphism of (GroupCat b₁) st cod b₃ = b₂ holds
(id b₂) * b₃ = b₃ ) & ( for b₃ being Morphism of (GroupCat b₁) st dom b₃ = b₂ holds
b₃ * (id b₂) = b₃ ) )

proof end;

registration

let c₁ be Universe;
cluster GroupCat a₁ -> strict Category-like ;
coherence

proof end;

end;

definition

let c₁ be Universe;
func AbGroupObjects c₁ -> Subset of the Objects of (GroupCat a₁) equals :: GRCAT_1:def 37
{ b₁ where B is Element of the Objects of (GroupCat a₁) : ex b₁ being AbGroup st b₁ = b₂ } ;
coherence

proof end;

end;

:: deftheorem Def37 defines AbGroupObjects GRCAT_1:def 37 :

theorem Th51: :: GRCAT_1:51

for b₁ being Universe holds L_Trivial in AbGroupObjects b₁

proof end;

registration

let c₁ be Universe;
cluster AbGroupObjects a₁ -> non empty ;
coherence by Th51;

end;

definition

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

end;

:: deftheorem Def38 defines AbGroupCat GRCAT_1:def 38 :

registration

let c₁ be Universe;
cluster AbGroupCat a₁ -> strict ;
coherence ;

end;

theorem Th52: :: GRCAT_1:52

for b₁ being Universe holds the Objects of (AbGroupCat b₁) = AbGroupObjects b₁ ;

definition

let c₁ be Universe;
func MidOpGroupObjects c₁ -> Subset of the Objects of (AbGroupCat a₁) equals :: GRCAT_1:def 39
{ b₁ where B is Element of the Objects of (AbGroupCat a₁) : ex b₁ being midpoint_operator AbGroup st b₁ = b₂ } ;
coherence

proof end;

end;

:: deftheorem Def39 defines MidOpGroupObjects GRCAT_1:def 39 :

registration

let c₁ be Universe;
cluster MidOpGroupObjects a₁ -> non empty ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def40 defines MidOpGroupCat GRCAT_1:def 40 :

registration

let c₁ be Universe;
cluster MidOpGroupCat a₁ -> strict ;
coherence ;

end;

theorem Th53: :: GRCAT_1:53

for b₁ being Universe holds the Objects of (MidOpGroupCat b₁) = MidOpGroupObjects b₁ ;

theorem Th54: :: GRCAT_1:54

for b₁ being Universe holds L_Trivial in MidOpGroupObjects b₁

proof end;