:: Definition and Properties of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama
::
:: Copyright (c) 2014-2017 Association of Mizar Users

definition
let D be non empty set ;
let x be Element of D;
:: original: <*
redefine func <*x*> -> FinSequence of D;
coherence
<*x*> is FinSequence of D
proof end;
end;

definition end;

registration
let G be Group;
correctness
existence
ex b1 being Subgroup of G st b1 is commutative
;
proof end;
end;

theorem Th1: :: GROUP_19:1
for I being set
for F being Group-Family of I
for i being object st i in I holds
F . i is Group
proof end;

definition
let I be non empty set ;
let F be Group-Family of I;
let i be Element of I;
:: original: .
redefine func F . i -> Group;
coherence
F . i is Group
by Th1;
end;

registration
let I be set ;
let F be Group-Family of I;
correctness
coherence
( not sum F is empty & sum F is constituted-Functions )
;
proof end;
end;

theorem Th2: :: GROUP_19:2
for I being set
for F being Function st I = dom F & ( for i being object st i in I holds
F . i is Group ) holds
F is Group-Family of I
proof end;

theorem Th3: :: GROUP_19:3
for I being set
for F being multMagma-Family of I
for a being Element of () holds dom a = I
proof end;

theorem Th4: :: GROUP_19:4
for I being non empty set
for F being multMagma-Family of I
for x being Element of I holds () . x = [#] (F . x)
proof end;

theorem Th5: :: GROUP_19:5
for I being non empty set
for F being multMagma-Family of I
for x being Function
for i being Element of I st x in product F holds
x . i in F . i
proof end;

theorem Th6: :: GROUP_19:6
for G, H being Group
for I being Subgroup of H
for f being Homomorphism of G,I holds f is Homomorphism of G,H
proof end;

definition
let I be set ;
let F be Group-Family of I;
let a be Function;
func support (a,F) -> Subset of I means :Def1: :: GROUP_19:def 1
for i being object holds
( i in it iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) );
existence
ex b1 being Subset of I st
for i being object holds
( i in b1 iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) )
proof end;
uniqueness
for b1, b2 being Subset of I st ( for i being object holds
( i in b1 iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) ) ) & ( for i being object holds
( i in b2 iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines support GROUP_19:def 1 :
for I being set
for F being Group-Family of I
for a being Function
for b4 being Subset of I holds
( b4 = support (a,F) iff for i being object holds
( i in b4 iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) ) );

theorem Th7: :: GROUP_19:7
for I being set
for F being Group-Family of I
for a being Element of (sum F) ex J being finite Subset of I ex b being ManySortedSet of J st
( J = support (a,F) & a = (1_ ()) +* b & ( for j being object
for G being Group st j in I \ J & G = F . j holds
a . j = 1_ G ) & ( for j being object st j in J holds
a . j = b . j ) )
proof end;

registration
let I be set ;
let F be Group-Family of I;
let a be Element of (sum F);
cluster support (a,F) -> finite ;
correctness
coherence
support (a,F) is finite
;
proof end;
end;

definition
let I be set ;
let G be Group;
let a be Function of I,G;
func support a -> Subset of I means :Def2: :: GROUP_19:def 2
for i being object holds
( i in it iff ( a . i <> 1_ G & i in I ) );
existence
ex b1 being Subset of I st
for i being object holds
( i in b1 iff ( a . i <> 1_ G & i in I ) )
proof end;
uniqueness
for b1, b2 being Subset of I st ( for i being object holds
( i in b1 iff ( a . i <> 1_ G & i in I ) ) ) & ( for i being object holds
( i in b2 iff ( a . i <> 1_ G & i in I ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines support GROUP_19:def 2 :
for I being set
for G being Group
for a being Function of I,G
for b4 being Subset of I holds
( b4 = support a iff for i being object holds
( i in b4 iff ( a . i <> 1_ G & i in I ) ) );

definition
let I be set ;
let G be Group;
let a be Function of I,G;
attr a is finite-support means :Def3: :: GROUP_19:def 3
support a is finite ;
end;

:: deftheorem Def3 defines finite-support GROUP_19:def 3 :
for I being set
for G being Group
for a being Function of I,G holds
( a is finite-support iff support a is finite );

registration
let I be set ;
let G be Group;
correctness
existence
ex b1 being Function of I,G st b1 is finite-support
;
proof end;
end;

registration
let I be set ;
let G be Group;
let a be finite-support Function of I,G;
correctness
coherence ;
by Def3;
end;

definition
let I be set ;
let G be Group;
let a be finite-support Function of I,G;
func Product a -> Element of G equals :: GROUP_19:def 4
Product (a | ());
correctness
coherence
Product (a | ()) is Element of G
;
;
end;

:: deftheorem defines Product GROUP_19:def 4 :
for I being set
for G being Group
for a being finite-support Function of I,G holds Product a = Product (a | ());

theorem Th8: :: GROUP_19:8
for I being set
for F being Group-Family of I
for a being Element of () holds
( a in sum F iff support (a,F) is finite )
proof end;

theorem Th9: :: GROUP_19:9
for I being set
for G being Group
for H being Group-Family of I
for x being Function of I,G
for y being Element of () st x = y & ( for i being object st i in I holds
H . i is Subgroup of G ) holds
support x = support (y,H)
proof end;

theorem Th10: :: GROUP_19:10
for I being set
for G being Group
for F being Group-Family of I
for a being object st a in sum F & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
a is finite-support Function of I,G
proof end;

theorem :: GROUP_19:11
for I being non empty set
for F being Group-Family of I holds support ((1_ ()),F) is empty
proof end;

theorem Th12: :: GROUP_19:12
for I being non empty set
for G being Group
for a being Function of I,G st a = I --> (1_ G) holds
support a is empty
proof end;

theorem Th13: :: GROUP_19:13
for I being non empty set
for G being Group
for F being Group-Family of I st ( for i being Element of I holds F . i is Subgroup of G ) holds
1_ () = I --> (1_ G)
proof end;

theorem :: GROUP_19:14
for I being non empty set
for F being Group-Family of I
for G being Group
for x being finite-support Function of I,G st support x = {} & ( for i being object st i in I holds
F . i is Subgroup of G ) holds
x = 1_ ()
proof end;

theorem Th15: :: GROUP_19:15
for I being set
for G being Group
for x being finite-support Function of I,G st support x = {} holds
Product x = 1_ G
proof end;

theorem Th16: :: GROUP_19:16
for I being non empty set
for G being Group
for a being finite-support Function of I,G st a = I --> (1_ G) holds
Product a = 1_ G
proof end;

theorem Th17: :: GROUP_19:17
for I being non empty set
for F being Group-Family of I
for x being Element of ()
for i being Element of I
for g being Element of (F . i) st x = (1_ ()) +* (i,g) holds
support (x,F) c= {i}
proof end;

theorem :: GROUP_19:18
for I being non empty set
for F being Group-Family of I
for x being Element of ()
for i being Element of I
for g being Element of (F . i) st x = (1_ ()) +* (i,g) & g <> 1_ (F . i) holds
support (x,F) = {i}
proof end;

theorem Th19: :: GROUP_19:19
for I being non empty set
for G being Group
for i being Element of I
for g being Element of G
for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) holds
support a c= {i}
proof end;

theorem Th20: :: GROUP_19:20
for I being non empty set
for G being Group
for i being Element of I
for g being Element of G
for a being Function of I,G st a = (I --> (1_ G)) +* (i,g) & g <> 1_ G holds
support a = {i}
proof end;

theorem Th21: :: GROUP_19:21
for I being non empty set
for G being Group
for a being finite-support Function of I,G
for i being Element of I
for g being Element of G st a = (I --> (1_ G)) +* (i,g) holds
Product a = g
proof end;

theorem :: GROUP_19:22
for I being non empty set
for F being Group-Family of I
for x being Function
for i being Element of I
for g being Element of (F . i) st support (x,F) is finite holds
support ((x +* (i,g)),F) is finite
proof end;

theorem Th23: :: GROUP_19:23
for I being non empty set
for G being Group
for a being Function of I,G
for i being Element of I
for g being Element of G st support a is finite holds
support (a +* (i,g)) is finite
proof end;

theorem Th24: :: GROUP_19:24
for I being non empty set
for F being Group-Family of I
for x being Function
for i being Element of I
for g being Element of (F . i) st x in product F holds
x +* (i,g) in product F
proof end;

theorem Th25: :: GROUP_19:25
for I being non empty set
for F being Group-Family of I
for x being Function
for i being Element of I
for g being Element of (F . i) st x in sum F holds
x +* (i,g) in sum F
proof end;

theorem :: GROUP_19:26
for I being non empty set
for G being Group
for a being finite-support Function of I,G
for i being Element of I
for g being Element of G holds a +* (i,g) is finite-support Function of I,G
proof end;

theorem Th27: :: GROUP_19:27
for I being non empty set
for F being Group-Family of I
for i being Element of I
for a, b being Function st dom a = I & b = a +* (i,(1_ (F . i))) holds
support (b,F) = (support (a,F)) \ {i}
proof end;

theorem Th28: :: GROUP_19:28
for I being non empty set
for G being Group
for i being object
for a, b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
support b = () \ {i}
proof end;

theorem :: GROUP_19:29
for I being non empty set
for F being Group-Family of I
for i being Element of I
for a being Element of (sum F)
for b being Function st i in support (a,F) & b = a +* (i,(1_ (F . i))) holds
card (support (b,F)) = (card (support (a,F))) - 1
proof end;

theorem :: GROUP_19:30
for I being non empty set
for G being Group
for i being object
for a being finite-support Function of I,G
for b being Function of I,G st i in support a & b = a +* (i,(1_ G)) holds
card () = (card ()) - 1
proof end;

theorem :: GROUP_19:31
for I being non empty set
for F being Group-Family of I
for a, b being Element of () st support (a,F) misses support (b,F) holds
a +* (b | (support (b,F))) = a * b
proof end;

theorem Th32: :: GROUP_19:32
for I being non empty set
for F being Group-Family of I
for a, b being Element of () st support (a,F) misses support (b,F) holds
a * b = b * a
proof end;

theorem Th33: :: GROUP_19:33
for I being non empty set
for F being Group-Family of I
for i being Element of I holds ProjGroup (F,i) is Subgroup of sum F
proof end;

theorem Th34: :: GROUP_19:34
for I being non empty set
for F, G being Group-Family of I
for x, y being Function st ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st y . i = hi . (x . i) ) holds
support (y,G) c= support (x,F)
proof end;

definition
let F, G be non-empty non empty Function;
let h be non empty Function;
assume A1: ( dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds
h . i is Function of (F . i),(G . i) ) ) ;
func ProductMap (F,G,h) -> Function of (),() means :Def5: :: GROUP_19:def 5
for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (it . x) . i = hi . (x . i) );
existence
ex b1 being Function of (),() st
for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (b1 . x) . i = hi . (x . i) )
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (b1 . x) . i = hi . (x . i) ) ) & ( for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (b2 . x) . i = hi . (x . i) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ProductMap GROUP_19:def 5 :
for F, G being non-empty non empty Function
for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds
h . i is Function of (F . i),(G . i) ) holds
for b4 being Function of (),() holds
( b4 = ProductMap (F,G,h) iff for x being Element of product F
for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & (b4 . x) . i = hi . (x . i) ) );

theorem Th35: :: GROUP_19:35
for F, G being non-empty non empty Function
for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is onto ) ) holds
ProductMap (F,G,h) is onto
proof end;

theorem Th36: :: GROUP_19:36
for F, G being non-empty non empty Function
for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is one-to-one ) ) holds
ProductMap (F,G,h) is one-to-one
proof end;

theorem Th37: :: GROUP_19:37
for F, G being non-empty non empty Function
for h being non empty Function st dom F = dom G & dom G = dom h & ( for i being object st i in dom h holds
ex hi being Function of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
ProductMap (F,G,h) is bijective
proof end;

theorem Th38: :: GROUP_19:38
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function
for x being Element of ()
for y being Element of () st I = dom h & y = (ProductMap ((),(),h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
proof end;

definition
let I be non empty set ;
let F, G be Group-Family of I;
let h be non empty Function;
assume A1: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) ) ;
func ProductMap (F,G,h) -> Homomorphism of (),() equals :Def6: :: GROUP_19:def 6
ProductMap ((),(),h);
coherence
ProductMap ((),(),h) is Homomorphism of (),()
proof end;
end;

:: deftheorem Def6 defines ProductMap GROUP_19:def 6 :
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
ProductMap (F,G,h) = ProductMap ((),(),h);

theorem Th39: :: GROUP_19:39
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function
for x being Element of ()
for y being Element of () st I = dom h & y = (ProductMap (F,G,h)) . x & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & y . i = hi . (x . i) )
proof end;

theorem Th40: :: GROUP_19:40
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
ProductMap (F,G,h) is bijective
proof end;

definition
let I be non empty set ;
let F be Group-Family of I;
let i be Element of I;
:: original: ProjGroup
redefine func ProjGroup (F,i) -> strict Subgroup of sum F;
correctness
coherence
ProjGroup (F,i) is strict Subgroup of sum F
;
by Th33;
end;

definition
let I be non empty set ;
let F, G be Group-Family of I;
let h be non empty Function;
assume A1: ( I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) ) ;
func SumMap (F,G,h) -> Homomorphism of (sum F),(sum G) equals :Def7: :: GROUP_19:def 7
(ProductMap (F,G,h)) | (sum F);
correctness
coherence
(ProductMap (F,G,h)) | (sum F) is Homomorphism of (sum F),(sum G)
;
proof end;
end;

:: deftheorem Def7 defines SumMap GROUP_19:def 7 :
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
SumMap (F,G,h) = (ProductMap (F,G,h)) | (sum F);

theorem :: GROUP_19:41
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I ex hi being Homomorphism of (F . i),(G . i) st
( hi = h . i & hi is bijective ) ) holds
SumMap (F,G,h) is bijective
proof end;

theorem :: GROUP_19:42
for I being non empty set
for F, G being Group-Family of I
for h being non empty Function st I = dom h & ( for i being Element of I holds h . i is Homomorphism of (F . i),(G . i) ) holds
for i being Element of I
for f being Element of (F . i)
for hi being Homomorphism of (F . i),(G . i) st hi = h . i holds
(SumMap (F,G,h)) . ((1ProdHom (F,i)) . f) = (1ProdHom (G,i)) . (hi . f)
proof end;

theorem Th43: :: GROUP_19:43
for I being non empty set
for G being Group
for i being object st i in I holds
ex F being Group-Family of I ex h being Homomorphism of (sum F),G st
( h is bijective & F = (I --> ((1). G)) +* ({i} --> G) & ( for j being Element of I holds 1_ (F . j) = 1_ G ) & ( for x being Element of (sum F) holds h . x = x . i ) & ( for x being Element of (sum F) ex J being finite Subset of I ex a being ManySortedSet of J st
( J c= {i} & J = support (x,F) & ( support (x,F) = {} or support (x,F) = {i} ) & x = (1_ ()) +* a & ( for j being Element of I st j in I \ J holds
x . j = 1_ (F . j) ) & ( for j being object st j in J holds
x . j = a . j ) ) ) )
proof end;

definition
let I be non empty set ;
let G be Group;
mode DirectSumComponents of G,I -> Group-Family of I means :Def8: :: GROUP_19:def 8
ex h being Homomorphism of (sum it),G st h is bijective ;
existence
ex b1 being Group-Family of I ex h being Homomorphism of (sum b1),G st h is bijective
proof end;
end;

:: deftheorem Def8 defines DirectSumComponents GROUP_19:def 8 :
for I being non empty set
for G being Group
for b3 being Group-Family of I holds
( b3 is DirectSumComponents of G,I iff ex h being Homomorphism of (sum b3),G st h is bijective );

definition
let I be non empty set ;
let G be Group;
let F be DirectSumComponents of G,I;
attr F is internal means :Def9: :: GROUP_19:def 9
( ( for i being Element of I holds F . i is Subgroup of G ) & ex h being Homomorphism of (sum F),G st
( h is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h . x = Product x ) ) );
end;

:: deftheorem Def9 defines internal GROUP_19:def 9 :
for I being non empty set
for G being Group
for F being DirectSumComponents of G,I holds
( F is internal iff ( ( for i being Element of I holds F . i is Subgroup of G ) & ex h being Homomorphism of (sum F),G st
( h is bijective & ( for x being finite-support Function of I,G st x in sum F holds
h . x = Product x ) ) ) );

registration
let I be non empty set ;
let G be Group;
existence
ex b1 being DirectSumComponents of G,I st b1 is internal
proof end;
end;

theorem Th44: :: GROUP_19:44
for G being Group
for A being non empty Subset of G st ( for x, y being Element of G st x in A & y in A holds
x * y = y * x ) holds
gr A is commutative
proof end;

theorem Th45: :: GROUP_19:45
for G being Group
for H being Subgroup of G
for a being FinSequence of G
for b being FinSequence of H st a = b holds
Product a = Product b
proof end;

theorem Th46: :: GROUP_19:46
for G being Group
for h being Element of G
for F being FinSequence of G st ( for k being Nat st k in dom F holds
h * (F /. k) = (F /. k) * h ) holds
h * () = () * h
proof end;

theorem Th47: :: GROUP_19:47
for G being Group
for F, F1, F2 being FinSequence of G st len F = len F1 & len F = len F2 & ( for i, j being Nat st i in dom F & j in dom F & i <> j holds
(F1 /. i) * (F2 /. j) = (F2 /. j) * (F1 /. i) ) & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
proof end;

theorem Th48: :: GROUP_19:48
for G being Group
for a being FinSequence of G st ( for i being object st i in dom a holds
a . i = 1_ G ) holds
Product a = 1_ G
proof end;

theorem Th49: :: GROUP_19:49
for I being finite set
for G being Group
for a being b1 -defined the carrier of b2 -valued total Function st ( for i being object st i in I holds
a . i = 1_ G ) holds
Product a = 1_ G
proof end;

theorem Th50: :: GROUP_19:50
for A being finite set
for B being non empty set
for f being b1 -defined b2 -valued total Function holds f * () is FinSequence of B
proof end;

theorem Th51: :: GROUP_19:51
for I being non empty set
for G being Group
for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W & ( for i, j being Element of I holds (a . i) * (a . j) = (a . j) * (a . i) ) holds
Product a = Product (a | W)
proof end;

theorem :: GROUP_19:52
for I being non empty set
for G being Group
for a being finite-support Function of I,G
for W being finite Subset of I st support a c= W holds
ex aW being finite-support Function of W,G st
( aW = a | W & support a = support aW & Product a = Product aW )
proof end;

theorem Th53: :: GROUP_19:53
for I being non empty set
for G being Group
for F being Group-Family of I
for sx, sy being Element of (sum F)
for x, y, xy being finite-support Function of I,G st ( for i being Element of I holds F . i is Subgroup of G ) & ( 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 ) & sx = x & sy = y & sx * sy = xy holds
Product xy = () * ()
proof end;

theorem :: GROUP_19:54
for I being non empty set
for G being 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
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi ) & ( 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;