begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem
canceled;
theorem Th5:
theorem Th6:
theorem
canceled;
theorem
:: 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 :
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
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
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
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
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 :
:: deftheorem defines cod GRCAT_1:def 7 :
:: deftheorem defines comp GRCAT_1:def 8 :
:: deftheorem defines ID GRCAT_1:def 9 :
definition
let C be
Category;
let O be non
empty Subset of the
carrier of
C;
func cat O -> Subcategory of
C equals
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
end;
:: deftheorem defines cat GRCAT_1:def 10 :
theorem
canceled;
theorem
:: deftheorem GRCAT_1:def 11 :
canceled;
:: deftheorem defines ZeroMap GRCAT_1:def 12 :
:: deftheorem Def13 defines additive GRCAT_1:def 13 :
theorem
canceled;
theorem
canceled;
theorem Th13:
theorem Th14:
:: deftheorem defines dom GRCAT_1:def 14 :
:: deftheorem defines cod GRCAT_1:def 15 :
:: deftheorem defines fun GRCAT_1:def 16 :
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines ZERO GRCAT_1:def 17 :
:: deftheorem Def18 defines GroupMorphism-like GRCAT_1:def 18 :
theorem Th18:
:: deftheorem Def19 defines Morphism GRCAT_1:def 19 :
theorem Th19:
theorem Th20:
:: deftheorem defines ID GRCAT_1:def 20 :
theorem
canceled;
theorem Th22:
theorem Th23:
theorem Th24:
theorem
theorem Th26:
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 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) #)
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
end;
:: deftheorem Def21 defines * GRCAT_1:def 21 :
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
canceled;
theorem Th28:
theorem Th29:
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) #)
theorem Th30:
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) #) )
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: deftheorem Def22 defines Group_DOMAIN-like GRCAT_1:def 22 :
:: deftheorem Def23 defines GroupMorphism_DOMAIN-like GRCAT_1:def 23 :
theorem
canceled;
theorem
canceled;
theorem Th37:
:: deftheorem Def24 defines GroupMorphism_DOMAIN GRCAT_1:def 24 :
theorem Th38:
theorem
:: deftheorem Def25 defines MapsSet GRCAT_1:def 25 :
:: deftheorem defines Maps GRCAT_1:def 26 :
definition
let G,
H be
AddGroup;
func Morphs G,
H -> GroupMorphism_DOMAIN of
G,
H means :
Def27:
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 )
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
end;
:: deftheorem Def27 defines Morphs GRCAT_1:def 27 :
:: deftheorem Def28 defines GO GRCAT_1:def 28 :
theorem Th40:
for
x,
y1,
y2 being
set st
GO x,
y1 &
GO x,
y2 holds
y1 = y2
theorem Th41:
:: deftheorem Def29 defines GroupObjects GRCAT_1:def 29 :
theorem Th42:
theorem Th43:
:: deftheorem Def30 defines Morphs GRCAT_1:def 30 :
:: deftheorem defines ID GRCAT_1:def 31 :
definition
let V be
Group_DOMAIN;
func dom V -> Function of
(Morphs V),
V means :
Def32:
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
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
func cod V -> Function of
(Morphs V),
V means :
Def33:
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
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
func ID V -> Function of
V,
(Morphs V) means :
Def34:
for
G being
Element of
V holds
it . G = ID G;
existence
ex b1 being Function of V,(Morphs V) st
for G being Element of V holds b1 . G = ID G
uniqueness
for b1, b2 being Function of V,(Morphs V) st ( for G being Element of V holds b1 . G = ID G ) & ( for G being Element of V holds b2 . G = ID G ) holds
b1 = b2
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:
theorem Th45:
definition
let V be
Group_DOMAIN;
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
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 ) )
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
end;
:: deftheorem Def35 defines comp GRCAT_1:def 35 :
definition
let UN be
Universe;
func GroupCat UN -> CatStr equals
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 :
theorem Th46:
theorem Th47:
theorem Th48:
theorem
canceled;
theorem Th50:
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 )
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
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 ) )
:: deftheorem defines AbGroupObjects GRCAT_1:def 37 :
theorem Th51:
:: deftheorem defines AbGroupCat GRCAT_1:def 38 :
theorem
:: deftheorem defines MidOpGroupObjects GRCAT_1:def 39 :
:: deftheorem defines MidOpGroupCat GRCAT_1:def 40 :
theorem
theorem
theorem
canceled;
theorem