begin
theorem Th1:
:: deftheorem Def1 defines ProjSet GROUP_12:def 1 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Subset of (product F) holds
( b4 = ProjSet (F,i) iff for x being set holds
( x in b4 iff ex g being Element of (F . i) st x = (1_ (product F)) +* (i,g) ) );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def2 defines ProjGroup GROUP_12:def 2 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being strict Subgroup of product F holds
( b4 = ProjGroup (F,i) iff the carrier of b4 = ProjSet (F,i) );
Lm1:
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I ex f being Homomorphism of (F . i),(ProjGroup (F,i)) st
( f is bijective & ( for x being Element of (F . i) holds f . x = (1_ (product F)) +* (i,x) ) )
definition
let I be non
empty set ;
let F be
Group-like associative multMagma-Family of
I;
let i be
Element of
I;
func 1ProdHom (
F,
i)
-> Homomorphism of
(F . i),
(ProjGroup (F,i)) means :
Def3:
for
x being
Element of
(F . i) holds
it . x = (1_ (product F)) +* (
i,
x);
existence
ex b1 being Homomorphism of (F . i),(ProjGroup (F,i)) st
for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x)
uniqueness
for b1, b2 being Homomorphism of (F . i),(ProjGroup (F,i)) st ( for x being Element of (F . i) holds b1 . x = (1_ (product F)) +* (i,x) ) & ( for x being Element of (F . i) holds b2 . x = (1_ (product F)) +* (i,x) ) holds
b1 = b2
end;
:: deftheorem Def3 defines 1ProdHom GROUP_12:def 3 :
for I being non empty set
for F being Group-like associative multMagma-Family of I
for i being Element of I
for b4 being Homomorphism of (F . i),(ProjGroup (F,i)) holds
( b4 = 1ProdHom (F,i) iff for x being Element of (F . i) holds b4 . x = (1_ (product F)) +* (i,x) );
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem