GROUP_20: Equivalent Expressions of Direct Sum Decomposition of Groups

definition

let I be set ;
let G be Group;

mode Subgroup-Family of I,G -> Group-Family of I means :Def1: :: GROUP_20:def 1
for i being object st i in I holds
it . i is Subgroup of G;

existence

proof end;

end;

:: deftheorem Def1 defines Subgroup-Family GROUP_20:def 1 :

definition

let I be set ;
let G be Group;
let F be Subgroup-Family of I,G;

attr F is component-commutative means :: GROUP_20:def 2
for i, j being object
for gi, gj being Element of G st i in I & j in I & i <> j holds
ex Fi, Fj being Subgroup of G st
( Fi = F . i & Fj = F . j & ( gi in Fi & gj in Fj implies gi * gj = gj * gi ) );

end;

:: deftheorem defines component-commutative GROUP_20:def 2 :

definition

let I be non empty set ;
let G be Group;
let F be Subgroup-Family of I,G;

redefine attr F is component-commutative means :Def2: :: GROUP_20:def 3
for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi;

compatibility

proof end;

end;

:: deftheorem Def2 defines component-commutative GROUP_20:def 3 :

theorem Th1: :: GROUP_20:1

for G being Group
for H being normal Subgroup of G
for x, y being Element of G st y in H holds
( (x * y) * (x ") in H & x * (y * (x ")) in H )

proof end;

theorem Th2: :: GROUP_20:2

for I being non empty set
for G being Group
for F being Group-Family of I
for x being Function of I,G st x in product F holds
x is Function of I,(Union (Carrier F))

proof end;

theorem Th3: :: GROUP_20:3

for I being non empty set
for G being Group
for H being Subgroup of G
for x being Function of I,G
for y being Function of I,H st x = y holds
support x = support y

proof end;

theorem Th4: :: GROUP_20:4

for I being non empty set
for G being Group
for H being Subgroup of G
for y being finite-support Function of I,H holds y is finite-support Function of I,G

proof end;

theorem Th5: :: GROUP_20:5

for I being non empty set
for G being Group
for H being Subgroup of G
for x being finite-support Function of I,G st rng x c= [#] H holds
x is finite-support Function of I,H

proof end;

theorem Th6: :: GROUP_20:6

for I being non empty set
for G being Group
for H being Subgroup of G
for x being finite-support Function of I,G
for y being finite-support Function of I,H st x = y holds
Product x = Product y

proof end;

theorem Th7: :: GROUP_20:7

for f being Function
for i, x being set holds f = (f +* (i,x)) +* (i,(f . i))

proof end;

theorem Th8: :: GROUP_20:8

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for x, y being finite-support Function of I,G
for i being Element of I st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

proof end;

theorem Th9: :: GROUP_20:9

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G
for i being Element of I
for x, y being finite-support Function of I,(gr UF) st y = x +* (i,(1_ (F . i))) & x in product F holds
( Product x = (Product y) * (x . i) & (Product y) * (x . i) = (x . i) * (Product y) )

proof end;

theorem Th10: :: GROUP_20:10

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G
for y being finite-support Function of I,(gr UF)
for i being Element of I
for g being Element of (gr UF) st y in product F & y . i = 1_ (F . i) & g in F . i holds
(Product y) * g = g * (Product y)

proof end;

theorem Th11: :: GROUP_20:11

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G
for H being FinSequence of G
for K being FinSequence of INT st len H = len K & rng H c= UF & Product (H |^ K) = g holds
ex f being finite-support Function of I,G st
( f in product F & g = Product f )

proof end;

theorem Th12: :: GROUP_20:12

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G
for h, h0 being finite-support Function of I,G
for i being Element of I
for UFi being Subset of G st UFi = Union ((Carrier F) | (I \ {i})) & h0 = h +* (i,(1_ (F . i))) & h in product F holds
Product h0 in gr UFi

proof end;

theorem Th13: :: GROUP_20:13

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for g being Element of G st g in gr UF holds
ex f being finite-support Function of I,(gr UF) st
( f in sum F & g = Product f )

proof end;

theorem Th14: :: GROUP_20:14

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G
for UF being Subset of G st UF = Union (Carrier F) holds
for i being Element of I holds F . i is normal Subgroup of gr UF

proof end;

theorem Th15: :: GROUP_20:15

for I being non empty set
for G being Group
for F being component-commutative Subgroup-Family of I,G st ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) holds
for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2

proof end;

theorem :: GROUP_20:16

for I being non empty set
for G being strict Group
for F being Group-Family of I holds
( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is normal Subgroup of G ) & ex UF being Subset of G st
( UF = Union (Carrier F) & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union ((Carrier F) | (I \ {i})) & ([#] (gr UFi)) /\ ([#] (F . i)) = {(1_ G)} ) ) ) )

proof end;

theorem :: GROUP_20:17

for I being non empty set
for G being commutative Group
for F being Group-Family of I holds
( F is internal DirectSumComponents of G,I iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ( for i, j being Element of I st i <> j holds
([#] (F . i)) /\ ([#] (F . j)) = {(1_ G)} ) & ( for y being Element of G ex x being finite-support Function of I,G st
( x in sum F & y = Product x ) ) & ( for x1, x2 being finite-support Function of I,G st x1 in sum F & x2 in sum F & Product x1 = Product x2 holds
x1 = x2 ) ) )

proof end;

theorem Th19: :: GROUP_20:18

for I being non empty set
for G being Group
for F being Subgroup-Family of I,G
for h being Homomorphism of (sum F),G
for a being finite-support Function of I,G st a in sum F & ( for i being Element of I
for x being Element of (F . i) holds h . ((1ProdHom (F,i)) . x) = x ) holds
h . a = Product a

proof end;

theorem :: GROUP_20:19

for I being non empty set
for G being Group
for M being DirectSumComponents of G,I ex f being Homomorphism of (sum M),G ex N being internal DirectSumComponents of G,I st
( f is bijective & ( for i being Element of I ex qi being Homomorphism of (M . i),(N . i) st
( qi = f * (1ProdHom (M,i)) & qi is bijective ) ) )

proof end;