environ
vocabularies HIDDEN, XBOOLE_0, CLASSES2, TARSKI, ZFMISC_1, SUBSET_1, FUNCT_5, FUNCT_1, FUNCT_2, ALGSTR_0, MIDSP_2, ROBBINS1, SUPINF_2, ARYTM_3, ARYTM_1, CAT_1, STRUCT_0, RELAT_1, GRAPH_1, VECTSP_1, PARTFUN1, REALSET1, MIDSP_1, CAT_2, FUNCOP_1, MSSUBFAM, RLVECT_1, ENS_1, ALGSTR_1, GRCAT_1, MONOID_0, RELAT_2, BINOP_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FUNCT_1, MCART_1, REALSET1, PARTFUN1, FUNCT_2, ORDINAL1, CLASSES2, BINOP_1, FUNCOP_1, FUNCT_5, STRUCT_0, ALGSTR_0, GRAPH_1, CAT_1, TOPS_2, RLVECT_1, VECTSP_1, CAT_2, ALGSTR_1, MIDSP_2;
definitions VECTSP_1, CAT_1;
theorems CAT_1, CAT_2, CLASSES2, FUNCOP_1, FUNCT_1, FUNCT_2, MIDSP_2, VECTSP_1, TARSKI, ZFMISC_1, RLVECT_1, RELAT_1, ORDINAL1, XBOOLE_0, TOPS_2, BINOP_1, SUBSET_1, XTUPLE_0;
schemes FUNCT_2, BINOP_1, TARSKI, XBOOLE_0;
registrations XBOOLE_0, RELSET_1, FUNCT_2, CLASSES2, STRUCT_0, ALGSTR_1, MIDSP_2, ALGSTR_0, CAT_1;
constructors HIDDEN, PARTFUN1, CLASSES1, CLASSES2, REALSET1, TOPS_2, VECTSP_2, CAT_2, ALGSTR_1, MIDSP_2, FUNCOP_1, RELSET_1, FUNCT_5, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, STRUCT_0, ALGSTR_1, ALGSTR_0, GRAPH_1, CAT_1, XTUPLE_0, ORDINAL1;
expansions VECTSP_1;
definition
let G,
F be
GroupMorphism;
assume A1:
dom G = cod F
;
func G * F -> strict GroupMorphism means :
Def14:
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 Def14 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
object 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 )
Lm2:
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 ) )