:: Equivalent Expressions of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Copyright (c) 2015-2021 Association of Mizar Users

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
ex b1 being Group-Family of I st
for i being object st i in I holds
b1 . i is Subgroup of G
proof end;
end;

:: deftheorem Def1 defines Subgroup-Family GROUP_20:def 1 :
for I being set
for G being Group
for b3 being Group-Family of I holds
( b3 is Subgroup-Family of I,G iff for i being object st i in I holds
b3 . i is Subgroup of G );

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 :
for I being set
for G being Group
for F being Subgroup-Family of I,G holds
( F is component-commutative iff 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 ) ) );

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
( F is component-commutative iff 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 )
proof end;
end;

:: deftheorem Def2 defines component-commutative GROUP_20:def 3 :
for I being non empty set
for G being Group
for F being Subgroup-Family of I,G holds
( F is component-commutative iff 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 );

registration
let I be non empty set ;
let G be Group;
existence
ex b1 being Subgroup-Family of I,G st b1 is component-commutative
proof end;
end;

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 ())
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 = () * (x . i) & () * (x . i) = (x . i) * () )
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 = () * (x . i) & () * (x . i) = (x . i) * () )
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
() * g = g * ()
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 () 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 (() | (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 () 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 () 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 (() | (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 () & gr UF = G ) & ( for i being Element of I ex UFi being Subset of G st
( UFi = Union (() | (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;