:: Definition and Properties of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroshi Yamazaki , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received December 31, 2014
:: Copyright (c) 2014-2021 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

let I be set ;
mode Group-Family of I is Group-like associative multMagma-Family of I;

end;

registration

let G be Group;

cluster non empty unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V162() for Subgroup of G;

correctness
existence
ex b₁ being Subgroup of G st b₁ 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;

cluster sum F -> non empty constituted-Functions ;

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 (product F) holds dom a = I

proof end;

theorem :: GROUP_19:4

canceled;

::$CT

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 b₁ being Subset of I st
for i being object holds
( i in b₁ iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) )

proof end;

uniqueness
for b₁, b₂ being Subset of I st ( for i being object holds
( i in b₁ iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) ) ) & ( for i being object holds
( i in b₂ iff ex G being Group st
( G = F . i & a . i <> 1_ G & i in I ) ) ) holds
b₁ = b₂

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 b₄ being Subset of I holds
( b₄ = support (a,F) iff for i being object holds
( i in b₄ 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_ (product F)) +* 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 b₁ being Subset of I st
for i being object holds
( i in b₁ iff ( a . i <> 1_ G & i in I ) )

proof end;

uniqueness
for b₁, b₂ being Subset of I st ( for i being object holds
( i in b₁ iff ( a . i <> 1_ G & i in I ) ) ) & ( for i being object holds
( i in b₂ iff ( a . i <> 1_ G & i in I ) ) ) holds
b₁ = b₂

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 b₄ being Subset of I holds
( b₄ = support a iff for i being object holds
( i in b₄ 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;

cluster Relation-like I -defined the carrier of G -valued Function-like total quasi_total finite-support for Element of bool [:I, the carrier of G:];

correctness
existence
ex b₁ being Function of I,G st b₁ is finite-support ;

proof end;

end;

registration

let I be set ;
let G be Group;
let a be finite-support Function of I,G;

cluster support a -> finite ;

correctness
coherence
support a is finite ;
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 | (support a));

correctness
coherence
Product (a | (support 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 | (support a));

theorem Th8: :: GROUP_19:8

for I being set
for F being Group-Family of I
for a being Element of (product F) 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 (product H) 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_ (product F)),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_ (product F) = 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_ (product F)

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 (product F)
for i being Element of I
for g being Element of (F . i) st x = (1_ (product F)) +* (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 (product F)
for i being Element of I
for g being Element of (F . i) st x = (1_ (product F)) +* (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 = (support a) \ {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 (support b) = (card (support a)) - 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 (product F) 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 (product F) 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 (product F),(product G) 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 b₁ being Function of (product F),(product G) 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 & (b₁ . x) . i = hi . (x . i) )

proof end;

uniqueness
for b₁, b₂ being Function of (product F),(product G) 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 & (b₁ . 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 & (b₂ . x) . i = hi . (x . i) ) ) holds
b₁ = b₂

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 b₄ being Function of (product F),(product G) holds
( b₄ = 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 & (b₄ . 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 (product F)
for y being Element of (product G) st I = dom h & y = (ProductMap ((Carrier F),(Carrier 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;

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 (product F),(product G) equals :Def6: :: GROUP_19:def 6
ProductMap ((Carrier F),(Carrier G),h);

coherence
ProductMap ((Carrier F),(Carrier G),h) is Homomorphism of (product F),(product G)

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 ((Carrier F),(Carrier G),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 (product F)
for y being Element of (product G) 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_ (product F)) +* 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 b₁ being Group-Family of I ex h being Homomorphism of (sum b₁),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 b₃ being Group-Family of I holds
( b₃ is DirectSumComponents of G,I iff ex h being Homomorphism of (sum b₃),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;

cluster Relation-like I -defined Function-like non empty total 1-sorted-yielding multMagma-yielding Group-like associative internal for DirectSumComponents of G,I;

existence
ex b₁ being DirectSumComponents of G,I st b₁ 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 * (Product F) = (Product F) * 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 b₁ -defined the carrier of b₂ -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 b₁ -defined b₂ -valued total Function holds f * (canFS A) 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 = (Product x) * (Product y)

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;