begin
definition
let G,
F be
GroupMorphism;
assume A1:
dom G = cod F
;
func G * F -> strict GroupMorphism means :
Def16:
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 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 Th18:
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 Th19:
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 Th27:
for
x,
y1,
y2 being
set st
GO x,
y1 &
GO x,
y2 holds
y1 = y2
definition
let V be
Group_DOMAIN;
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;
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 )
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 ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )