:: Equivalent Expressions of Direct Sum Decomposition of Groups
:: by Kazuhisa Nakasho , Hiroyuki Okazaki , Hiroshi Yamazaki and Yasunari Shidama
::
:: Received February 26, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, FUNCT_1, RELAT_1, RLVECT_2, CARD_3, TARSKI, BINOP_1,
GROUP_1, XXREAL_0, GROUP_2, CARD_1, NUMBERS, FUNCT_4, GROUP_6, FUNCOP_1,
GROUP_12, PARTFUN1, FUNCT_2, SUBSET_1, XBOOLE_0, STRUCT_0, NAT_1,
ORDINAL4, PRE_TOPC, ARYTM_1, ARYTM_3, FINSET_1, NEWTON, GROUP_4,
PRE_POLY, UPROOTS, GROUP_19, SEMI_AF1, QC_LANG1, VECTMETR, GROUP_20;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, DOMAIN_1, FUNCT_3, FUNCOP_1, FUNCT_4, FINSET_1,
CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, FINSEQ_1, FUNCT_7, STRUCT_0,
ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_6, PRALG_1, GRSOLV_1,
GROUP_7, GROUP_12, GROUP_19;
constructors REALSET1, FUNCT_4, MONOID_0, PRALG_1, GROUP_4, FUNCT_7, RELSET_1,
INT_7, FUNCT_3, GROUP_17, GRSOLV_1, GROUP_19;
registrations XBOOLE_0, XREAL_0, STRUCT_0, GROUP_2, MONOID_0, ORDINAL1, NAT_1,
FUNCT_2, FUNCOP_1, CARD_1, GROUP_7, GROUP_3, RELSET_1, SUBSET_1, INT_1,
FINSET_1, RELAT_1, FUNCT_1, NUMBERS, GROUP_12, GROUP_6, GROUP_19;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GROUP_2, FINSEQ_1, STRUCT_0, FUNCOP_1, GRSOLV_1, GROUP_19;
expansions STRUCT_0, TARSKI;
theorems FUNCT_1, CARD_3, FUNCT_2, FUNCOP_1, TARSKI, GROUP_1, GROUP_2,
GROUP_3, FUNCT_4, FINSEQ_1, GROUP_4, GROUP_6, FINSEQ_2, XREAL_1,
FINSEQ_3, XBOOLE_0, RELAT_1, GROUP_7, FUNCT_7, XBOOLE_1, GROUP_12,
PARTFUN1, ZFMISC_1, GROUP_17, GROUP_19, GRSOLV_1, PENCIL_3;
schemes NAT_1, FUNCT_1, CLASSES1;
begin :: 1. Internal Direct Sum Decomposition into Normal Subgroups
definition
let I be set, G be Group;
mode Subgroup-Family of I,G -> Group-Family of I means :Def1:
for i being object st i in I holds it.i is Subgroup of G;
existence
proof
deffunc f(object) = (1).G;
consider F be Function such that
A1: dom F = I and
A2: for i be object st i in I holds F.i = f(i) from FUNCT_1:sch 3;
for i be object st i in I holds F.i is Group by A2; then
reconsider F as Group-Family of I by A1,GROUP_19:2;
take F;
thus thesis by A2;
end;
end;
definition
let I be set, G be Group, F be Subgroup-Family of I,G;
attr F is component-commutative means
for i,j be object, gi,gj be Element of G
st i in I & j in I & i <> j
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;
definition
let I be non empty set, G be Group, F be Subgroup-Family of I,G;
redefine attr F is component-commutative means :Def2: :: redefines component-commutative (GROUP_20, definition)
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi;
compatibility
proof
thus F is component-commutative implies
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi
proof
assume
A1: F is component-commutative;
let i,j be Element of I, gi,gj be Element of G;
assume i <> j;
then 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) by A1;
hence thesis;
end;
assume
A2: for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi;
let i,j be object, gi,gj be Element of G;
assume that
A3: i in I & j in I and
A4: i <> j;
reconsider Fi = F.i, Fj = F.j as Subgroup of G by A3,Def1;
take Fi, Fj;
thus thesis by A2,A3,A4;
end;
end;
registration
let I be non empty set, G be Group;
cluster component-commutative for Subgroup-Family of I,G;
existence
proof
deffunc f(object) = (1).G;
consider F be Function such that
A1: dom F = I and
A2: for i be object st i in I holds F.i = f(i) from FUNCT_1:sch 3;
for i be object st i in I holds F.i is Group by A2; then
reconsider F as Group-Family of I by A1,GROUP_19:2;
for i be object st i in I holds F.i is Subgroup of G by A2; then
reconsider F as Subgroup-Family of I,G by Def1;
take F;
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi
proof
let i,j be Element of I;
let gi,gj be Element of G;
assume i <> j & gi in F.i & gj in F.j; then
gi in (1).G & gj in (1).G by A2; then
gi in {1_G} & gj in {1_G} by GROUP_2:def 7; then
gi = 1_G & gj = 1_G by TARSKI:def 1;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th1:
for G be Group, H be normal Subgroup of G, x,y be Element of G st y in H
holds x * y * x" in H & x * (y * x") in H
proof
let G be Group,
H be normal Subgroup of G,
x,y be Element of G;
assume
A1: y in H;
x * H = H * x by GROUP_3:117; then
consider g be Element of G such that
A2: x * y = g * x & g in H by A1,GROUP_2:103,104;
(x * y) * x" = g by A2,GROUP_3:1;
hence thesis by A2,GROUP_1:def 3;
end;
theorem Th2:
for I be non empty set,
G be Group,
F be Group-Family of I,
x be Function of I,G
st x in product F
holds x is Function of I,Union(Carrier F)
proof
let I be non empty set,
G be Group,
F be Group-Family of I,
x be Function of I,G;
assume
A1: x in product F;
A2: dom(Carrier F) = I by PARTFUN1:def 2;
for z be object st z in rng x holds z in Union(Carrier F)
proof
let z be object;
assume z in rng x; then
consider i be object such that
A3: i in I & z = x.i by FUNCT_2:11;
reconsider i as Element of I by A3;
x.i in F.i by A1,GROUP_19:5; then
z in [#](F.i) by A3; then
A4: z in (Carrier F).i by PENCIL_3:7;
(Carrier F).i in rng(Carrier F) by A2,FUNCT_1:3; then
z in union rng(Carrier F) by A4,TARSKI:def 4;
hence z in Union(Carrier F) by CARD_3:def 4;
end; then
rng x c= Union(Carrier F);
hence x is Function of I,Union (Carrier F) by FUNCT_2:6;
end;
theorem Th3:
for I be non empty set,
G be Group,
H be Subgroup of G,
x be Function of I,G,
y be Function of I,H
st x = y
holds support x = support y
proof
let I be non empty set,
G be Group,
H be Subgroup of G,
x be Function of I,G,
y be Function of I,H;
assume
A1: x = y;
for i be object holds i in support x iff i in support y
proof
let i be object;
A2: i in support x iff x.i <> 1_G & i in I by GROUP_19:def 2;
i in support y iff y.i <> 1_H & i in I by GROUP_19:def 2;
hence thesis by A1,A2,GROUP_2:44;
end;
hence thesis by TARSKI:2;
end;
theorem Th4:
for I be non empty set,
G be Group,
H be Subgroup of G,
y be finite-support Function of I,H
holds y is finite-support Function of I,G
proof
let I be non empty set,
G be Group,
H be Subgroup of G,
y be finite-support Function of I,H;
[#]H c= [#]G by GROUP_2:def 5; then
reconsider x = y as Function of I,G by FUNCT_2:7;
support x = support y by Th3;
hence thesis by GROUP_19:def 3;
end;
theorem Th5:
for I be non empty set,
G be Group,
H be Subgroup of G,
x be finite-support Function of I,G
st rng x c= [#]H
holds x is finite-support Function of I,H
proof
let I be non empty set,
G be Group,
H be Subgroup of G,
x be finite-support Function of I,G;
assume rng x c= [#]H; then
reconsider y = x as Function of I,H by FUNCT_2:6;
support x = support y by Th3;
hence thesis by GROUP_19:def 3;
end;
theorem Th6:
for I be non empty set,
G be Group,
H be Subgroup of G,
x be finite-support Function of I,G,
y be finite-support Function of I,H
st x = y
holds Product x = Product y
proof
let I be non empty set,
G be Group,
H be Subgroup of G,
x be finite-support Function of I,G,
y be finite-support Function of I,H;
assume
A1: x = y; then
A2: support x = support y by Th3;
reconsider fx = (x|support(x)) * canFS(support x)
as FinSequence of G by FINSEQ_2:32;
reconsider fy = (y|support(y)) * canFS(support y)
as FinSequence of H by FINSEQ_2:32;
thus Product x = Product fx by GROUP_17:def 1
.= Product fy by A1,A2,GROUP_19:45
.= Product y by GROUP_17:def 1;
end;
theorem Th7:
for f be Function, i,x be set
holds f = f +* (i,x) +* (i,f.i)
proof
let f be Function, i,x be set;
thus f = f +* (i,f.i) by FUNCT_7:35
.= f +* (i,x) +* (i,f.i) by FUNCT_7:34;
end;
theorem Th8:
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
x,y be finite-support Function of I,G,
i be Element of I
st y = x +* (i,1_F.i) & x in product F
holds Product x = Product(y) * x.i = x.i * Product(y)
proof
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G,
x,y be finite-support Function of I,G,
i be Element of I;
A1: for i be object st i in I holds F.i is Subgroup of G by Def1;
A2: for i,j being Element of I, gi,gj being Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi by Def2;
assume that
A3: y = x +* (i,1_F.i) and
A4: x in product F;
A5: for i be Element of I holds F.i is Subgroup of G by Def1;
reconsider px = x as Element of product F by A4;
A6: x.i in F.i by A4,GROUP_19:5;
y in product F by A3,A4,GROUP_19:24; then
reconsider py = y as Element of product F;
support(y) = support(py,F) by A1,GROUP_19:9; then
py in sum F by GROUP_19:8; then
reconsider sy = py as Element of sum F;
set z = 1_product F +* (i,x.i);
A7: z in sum F by A6,GROUP_19:25,GROUP_2:46; then
A8: z in product F by GROUP_2:40;
reconsider sz = z as Element of sum F by A7;
reconsider pz = z as Element of product F by A8;
reconsider z as finite-support Function of I,G by A1,A7,GROUP_19:10;
A9: dom x = I by A4,GROUP_19:3;
sy * sz is Element of product F by GROUP_2:42; then
A10: dom(sy * sz) = I by GROUP_19:3;
A11: dom(1_product F) = I by GROUP_19:3;
A12: x = sy * sz
proof
for j be object st j in I holds x.j = (sy * sz).j
proof
let j be object;
assume j in I; then
reconsider j as Element of I;
y.j in F.j by A3,A4,GROUP_19:5,24; then
reconsider yj = y.j as Element of F.j;
z.j in F.j by A7,GROUP_19:5,GROUP_2:40; then
reconsider zj = z.j as Element of F.j;
per cases;
suppose
A13: j = i; then
A14: y.j = 1_F.j by A3,A9,FUNCT_7:31;
z.j = x.j by A11,A13,FUNCT_7:31; then
yj * zj = x.j by A14,GROUP_1:def 4; then
px.j = (py * pz).j by GROUP_7:1;
hence thesis by GROUP_2:43;
end;
suppose
A15: j <> i; then
A16: y.j = x.j by A3,FUNCT_7:32;
(1_product F).j = 1_F.j by GROUP_7:6; then
z.j = 1_F.j by A15,FUNCT_7:32; then
yj * zj = x.j by A16,GROUP_1:def 4; then
px.j = (py * pz).j by GROUP_7:1;
hence thesis by GROUP_2:43;
end;
end;
hence thesis by A9,A10,FUNCT_1:2;
end;
A17: sy * sz = sz * sy
proof
A18: support(py,F) = support(px,F) \ {i} by A3,A9,GROUP_19:27;
A19: support(py,F) misses support(pz,F)
by A6,A18,GROUP_19:17,XBOOLE_1:85;
thus sy * sz = py * pz by GROUP_2:43
.= pz * py by A19,GROUP_19:32
.= sz * sy by GROUP_2:43;
end;
A20: Product x = Product(y) * Product(z) by A2,A5,A12,GROUP_19:53;
1_product F = I --> 1_G by A5,GROUP_19:13; then
Product(z) = x.i by GROUP_19:21;
hence thesis by A2,A5,A12,A17,A20,GROUP_19:53;
end;
theorem Th9:
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
holds
for i be Element of I, x,y be 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 = x.i * Product(y)
proof
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G;
let i be Element of I,
x,y be finite-support Function of I,gr UF;
assume that
A1: y = x +* (i,1_F.i) and
A2: x in product F;
reconsider x0 = x, y0 = y as finite-support Function of I,G by Th4;
A3: Product x = Product x0 by Th6;
A4: Product y = Product y0 by Th6;
A5: Product x0 = Product(y0) * x0.i = x0.i * Product(y0) by A1,A2,Th8; then
Product x = Product(y) * x.i by A3,A4,GROUP_2:43;
hence thesis by A3,A4,A5,GROUP_2:43;
end;
theorem Th10:
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
holds
for y be finite-support Function of I,gr UF,
i be Element of I, g be 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
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G;
let y be finite-support Function of I,gr UF,
i be Element of I,
g be Element of gr UF;
assume that
A1: y in product F and
A2: y.i = 1_F.i and
A3: g in F.i;
reconsider x = y +* (i,g)
as finite-support Function of I,gr UF by GROUP_19:26;
A4: y = x +* (i,1_F.i) by A2,Th7;
A5: x in product F by A1,A3,GROUP_19:24;
dom y = I by PARTFUN1:def 2; then
x.i = g by FUNCT_7:31;
hence thesis by A4,A5,Th9;
end;
theorem Th11:
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
st UF = Union Carrier F
holds
for g be Element of G,
H be FinSequence of G,
K be FinSequence of INT
st len H = len K & rng H c= UF & Product(H|^K) = g
holds
ex f be finite-support Function of I,G
st f in product F & g = Product f
proof
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G;
assume
A1: UF = Union Carrier F;
defpred P[Nat] means
for g be Element of G,
H be FinSequence of G,
K be FinSequence of INT
st len H = $1 & len H = len K & rng H c= UF & Product(H|^K) = g
holds
ex f be finite-support Function of I,G
st f in product F & g = Product f;
A2: P[0]
proof
let g be Element of G,
H be FinSequence of G,
K be FinSequence of INT such that
A3: len H = 0 & len H = len K & rng H c= UF & Product(H|^K) = g;
H = <*>([#]G) & K = <*>INT by A3; then
A4: H|^K = <*>([#]G) by GROUP_4:21;
reconsider f = I --> 1_G as Function of I,G;
support(f) is finite by GROUP_19:12; then
reconsider f as finite-support Function of I,G by GROUP_19:def 3;
take f;
for i be Element of I holds F.i is Subgroup of G by Def1; then
f = 1_product F by GROUP_19:13;
hence f in product F;
Product f = 1_G by GROUP_19:16;
hence g = Product f by A3,A4,GROUP_4:8;
end;
A5: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A6: P[n];
let g be Element of G,
H be FinSequence of G,
K be FinSequence of INT such that
A7: len H = n+1 & len H = len K & rng H c= UF & Product(H|^K) = g;
reconsider h = H/.(n+1) as Element of G;
reconsider k = K/.(n+1) as Element of INT;
reconsider H0 = H|n as FinSequence of G;
reconsider K0 = K|n as FinSequence of INT;
reconsider H1 = <*h*> as FinSequence of G;
reconsider K1 = <*k*> as FinSequence of INT;
rng H0 c= rng H by RELAT_1:70; then
A8: rng H0 c= UF by A7;
A9: <* @k *> = K1 by GROUP_4:def 1;
n+1 in Seg(n+1) by FINSEQ_1:4; then
A10: n+1 in dom H & n+1 in dom K by A7,FINSEQ_1:def 3; then
H/.(n+1) = H.(n+1) & K/.(n+1) = K.(n+1) by PARTFUN1:def 6; then
A11: H = H0^H1 & K = K0^K1 by A7,FINSEQ_3:55;
h = H.(n+1) by A10,PARTFUN1:def 6; then
A12: h in UF by A7,A10,FUNCT_1:3;
n <= len H & n <= len K by A7,XREAL_1:31; then
A13: len H0 = n & len K0 = n by FINSEQ_1:17;
A14: len H1 = 1 & len K1 = 1 by FINSEQ_1:39;
A15: H|^K = (H0|^K0)^(H1|^K1) by A11,A13,A14,GROUP_4:19
.= (H0|^K0)^<*h|^k*> by A9,GROUP_4:22;
consider f0 be finite-support Function of I,G such that
A16: f0 in product F & Product(H0|^K0) = Product f0 by A6,A8,A13;
h in union rng Carrier F by A1,A12,CARD_3:def 4; then
consider Fi be set such that
A17: h in Fi & Fi in rng Carrier F by TARSKI:def 4;
consider i be object such that
A18: i in dom(Carrier F) & Fi = (Carrier F).i by A17,FUNCT_1:def 3;
reconsider i as Element of I by A18;
A19: F.i is Subgroup of G by Def1;
(Carrier F).i = [#](F.i) by PENCIL_3:7; then
h in F.i by A17,A18; then
A22: h|^k in F.i by A19,GROUP_4:4;
A23: f0.i in F.i by A16,GROUP_19:5;
1_F.i is Element of G by A19,GROUP_2:42; then
reconsider f1 = f0 +* (i,1_F.i)
as finite-support Function of I,G by GROUP_19:26;
reconsider f = f1 +* (i, f0.i * h|^k)
as finite-support Function of I,G by GROUP_19:26;
A27: dom f0 = I by FUNCT_2:def 1;
A28: dom f1 = I by FUNCT_2:def 1;
A29: f1 in product F by A16,GROUP_19:24;
A30: f.i = f0.i * h|^k by A28,FUNCT_7:31;
take f;
f0.i * h|^k in F.i by A19,A22,A23,GROUP_2:50;
hence
A31: f in product F by A29,GROUP_19:24;
f1.i = 1_F.i by A27,FUNCT_7:31; then
f1 = f +* (i, 1_F.i) by Th7; then
Product f = Product(f1) * (f0.i * h|^k) by A30,A31,Th8
.= Product(f1) * f0.i * h|^k by GROUP_1:def 3
.= Product(f0) * h|^k by A16,Th8
.= g by A7,A15,A16,GROUP_4:6;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A2,A5);
hence thesis;
end;
theorem Th12:
for I be non empty set,
G be Group,
F be Subgroup-Family of I,G,
h,h0 be finite-support Function of I,G,
i be Element of I,
UFi be 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
let I be non empty set,
G be Group,
F be Subgroup-Family of I,G,
h,h0 be finite-support Function of I,G,
i be Element of I,
UFi be Subset of G;
assume that
A1: UFi = Union((Carrier F) | (I \ {i})) and
A2: h0 = h +* (i, 1_F.i) and
A3: h in product F;
set CFi = (Carrier F) | (I \ {i});
dom(Carrier F) = I by PARTFUN1:def 2; then
A4: dom CFi = I \ {i} by RELAT_1:62;
for y be object st y in rng h0 holds y in [#]gr(UFi)
proof
let y be object;
assume y in rng h0; then
consider j be Element of I such that
A5: y = h0.j by FUNCT_2:113;
per cases;
suppose
A6: j <> i; then
not j in {i} by TARSKI:def 1; then
A7: j in dom CFi by A4,XBOOLE_0:def 5;
A8: h0.j = h.j by A2,A6,FUNCT_7:32;
h.j in F.j by A3,GROUP_19:5; then
h.j in [#](F.j); then
h.j in (Carrier F).j by PENCIL_3:7; then
A9: h0.j in CFi.j by A7,A8,FUNCT_1:47;
CFi.j c= union rng CFi by A7,FUNCT_1:3,ZFMISC_1:74; then
A10: CFi.j c= UFi by A1,CARD_3:def 4;
UFi c= [#]gr(UFi) by GROUP_4:def 4;
hence thesis by A5,A9,A10;
end;
suppose
A11: j = i;
dom h = I by A3,GROUP_19:3; then
A12: h0.j = 1_F.j by A2,A11,FUNCT_7:31;
F.j is Subgroup of G by Def1; then
1_F.j = 1_gr(UFi) by GROUP_2:45;
hence thesis by A5,A12;
end;
end; then
rng h0 c= [#]gr(UFi); then
reconsider x0 = h0 as finite-support Function of I,gr(UFi) by Th5;
Product x0 = Product h0 by Th6;
hence Product h0 in gr(UFi);
end;
theorem Th13:
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
st UF = Union Carrier F
holds
for g be Element of G st g in gr UF holds
ex f be finite-support Function of I,gr UF
st f in sum F & g = Product f
proof
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G;
assume
A1: UF = Union Carrier F;
A2: for i be object st i in I holds F.i is Subgroup of G by Def1;
let g be Element of G;
assume g in gr UF; then
consider H be FinSequence of G,
K be FinSequence of INT such that
A3: len H = len K & rng H c= UF & Product(H|^K) = g by GROUP_4:28;
consider f be finite-support Function of I,G such that
A4: f in product F & g = Product f by A1,A3,Th11;
f is Function of I,Union Carrier F by A4,Th2; then
A5: rng f c= UF by A1,RELAT_1:def 19;
UF c= [#]gr(UF) by GROUP_4:def 4; then
rng f c= [#]gr(UF) by A5; then
reconsider f0 = f as finite-support Function of I,gr(UF) by Th5;
take f0;
support(f,F) = support(f) by A2,A4,GROUP_19:9;
hence thesis by A4,GROUP_19:8,Th6;
end;
theorem Th14:
for I be non empty set, G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G
st UF = Union Carrier F
holds
for i be Element of I holds F.i is normal Subgroup of gr UF
proof
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G,
UF be Subset of G;
assume
A1: UF = Union Carrier F;
let i be Element of I;
A2: dom(Carrier F) = I by PARTFUN1:def 2;
A3: F.i is Subgroup of G by Def1;
(Carrier F).i in rng Carrier F by A2,FUNCT_1:3; then
[#](F.i) in rng Carrier F by PENCIL_3:7; then
[#](F.i) c= union rng Carrier F by ZFMISC_1:74; then
A4: [#](F.i) c= UF by A1,CARD_3:def 4;
UF c= [#]gr(UF) by GROUP_4:def 4; then
[#](F.i) c= [#]gr(UF) by A4; then
reconsider Fi = F.i as Subgroup of gr UF by A3,GROUP_2:57;
for a be Element of gr UF holds a * Fi c= Fi * a
proof
let a be Element of gr UF;
for x be object st x in a * Fi holds x in Fi * a
proof
let x be object;
assume x in a * Fi; then
consider g be Element of gr(UF) such that
A5: x = a * g & g in Fi by GROUP_2:103;
reconsider a1 = a as Element of G by GROUP_2:42;
a1 in gr(UF); then
consider h be finite-support Function of I,gr UF such that
A6: h in sum F & a = Product h by A1,Th13;
reconsider m = h.i as Element of gr UF;
A7: h in product F by A6,GROUP_2:40;
A8: h.i in F.i by A6,GROUP_19:5,GROUP_2:40;
reconsider I0 = I \ {i} as Subset of I;
1_F.i in gr(UF) by A3,GROUP_2:47; then
reconsider h0 = h +* (i, 1_F.i)
as finite-support Function of I,gr(UF) by GROUP_19:26;
A9: h0 in product F by A6,GROUP_19:24,GROUP_2:40;
dom h = I by FUNCT_2:def 1; then
A10: h0.i = 1_F.i by FUNCT_7:31;
A11: a * g = Product(h0) * m * g by A6,A7,Th9
.= Product(h0) * (m * g) by GROUP_1:def 3;
A12: a * g = (m * g) * Product(h0)
by A5,A8,A9,A10,A11,GROUP_2:50,Th10
.= (m * g) * 1_gr(UF) * Product(h0) by GROUP_1:def 4
.= (m * g) * (m" * m) * Product(h0) by GROUP_1:def 5
.= (m * g * m") * m * Product(h0) by GROUP_1:def 3
.= (m * g * m") * (m * Product(h0)) by GROUP_1:def 3
.= (m * g * m") * (Product(h0) * m) by A7,Th9
.= (m * g * m") * a by A6,A7,Th9;
m" in Fi by A8,GROUP_2:51; then
g * m" in Fi by A5,GROUP_2:50; then
m * (g * m") in Fi by A8,GROUP_2:50; then
m * g * m" in Fi by GROUP_1:def 3;
hence thesis by A5,A12,GROUP_2:104;
end;
hence thesis;
end;
hence thesis by GROUP_3:118;
end;
theorem Th15:
for I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G
st for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#]gr(UFi) /\ [#](F.i) = {1_G}
holds
for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2
proof
let I be non empty set,
G be Group,
F be component-commutative Subgroup-Family of I,G;
A1: for i be object st i in I holds F.i is Subgroup of G by Def1;
assume
A2: for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#]gr(UFi) /\ [#](F.i) = {1_G};
let x1,x2 be finite-support Function of I,G;
assume that
A3: x1 in sum F & x2 in sum F and
A4: Product x1 = Product x2;
defpred P[Nat] means
for x1,x2 be finite-support Function of I,G
st card(support x1) = $1
& x1 in sum F & x2 in sum F & Product x1 = Product x2 holds x1 = x2;
A5: P[0]
proof
let x1,x2 be finite-support Function of I,G;
assume that
A6: card(support x1) = 0 and
A7: x1 in sum F & x2 in sum F and
A8: Product x1 = Product x2;
A9: support(x1) = {} by A6;
A10: Product x2 = 1_G by A8,A9,GROUP_19:15;
x2 = 1_product F
proof
assume x2 <> 1_product F; then
support(x2) is not empty by A1,GROUP_19:14; then
consider i be object such that
A11: i in support(x2) by XBOOLE_0:def 1;
A12: x2.i <> 1_G & i in I by A11,GROUP_19:def 2;
reconsider i as Element of I by A11;
A13: F.i is Subgroup of G by Def1; then
1_F.i is Element of G by GROUP_2:42; then
reconsider y = x2 +* (i,1_F.i)
as finite-support Function of I,G by GROUP_19:26;
x2 in product F by A7,GROUP_2:41; then
A14: Product(x2) = Product(y) * x2.i by Th8;
consider UFi be Subset of G such that
A15: UFi = Union((Carrier F) | (I \ {i})) and
A16: [#]gr(UFi) /\ [#](F.i) = {1_G} by A2;
A17: Product(y) in gr(UFi) by A7,A15,GROUP_2:41,Th12;
x2.i in F.i by A7,GROUP_19:5,GROUP_2:41; then
A18: (x2.i)" in F.i by A13,GROUP_2:51;
A19: Product(y) = (x2.i)" by A10,A14,GROUP_1:12; then
Product(y) in {1_G} by A16,A17,A18,XBOOLE_0:def 4; then
Product(y) = 1_G by TARSKI:def 1;
hence contradiction by A12,A19,GROUP_1:10;
end;
hence thesis by A1,A9,GROUP_19:14;
end;
A20: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A21: P[k];
let x1,x2 be finite-support Function of I,G;
assume that
A22: card(support x1) = k+1 and
A23: x1 in sum F & x2 in sum F and
A24: Product(x1) = Product(x2);
support(x1) is not empty by A22; then
consider i be object such that
A25: i in support(x1) by XBOOLE_0:def 1;
reconsider i as Element of I by A25;
A26: F.i is Subgroup of G by Def1; then
A27: 1_F.i is Element of G by GROUP_2:42;
reconsider y1 = x1 +* (i,1_F.i)
as finite-support Function of I,G by A27,GROUP_19:26;
reconsider y2 = x2 +* (i,1_F.i)
as finite-support Function of I,G by A27,GROUP_19:26;
consider UFi be Subset of G such that
A28: UFi = Union((Carrier F) | (I \ {i})) and
A29: [#]gr(UFi) /\ [#](F.i) = {1_G} by A2;
1_F.i = 1_G by A26,GROUP_2:44; then
A30: card(support y1) = card(support x1) -1 by A25,GROUP_19:30
.= k by A22;
A31: y1 in sum F & y2 in sum F by A23,GROUP_19:25;
A32: x1 in product F & x2 in product F by A23,GROUP_2:41;
A33: Product(x1) = Product(y1) * x1.i by A32,Th8;
A34: Product(y1) in gr(UFi) & Product(y2) in gr(UFi)
by A23,A28,GROUP_2:41,Th12;
A35: x1.i in F.i & x2.i in F.i by A23,GROUP_19:5,GROUP_2:41;
Product(y1) = Product(y2) * x2.i * (x1.i)"
by A24,A32,A33,GROUP_1:14,Th8; then
Product(y1) = Product(y2) * (x2.i * (x1.i)") by GROUP_1:def 3; then
A36: Product(y2)" * Product(y1) = x2.i * (x1.i)" by GROUP_1:13;
Product(y2)" in gr(UFi) by A34,GROUP_2:51; then
A37: Product(y2)" * Product(y1) in gr(UFi) by A34,GROUP_2:50;
(x1.i)" in F.i by A26,A35,GROUP_2:51; then
A38: x2.i * (x1.i)" in F.i by A26,A35,GROUP_2:50;
Product(y2)" * Product(y1) in {1_G} by A29,A36,A37,A38,XBOOLE_0:def 4;
then Product(y2)" * Product(y1) = 1_G by TARSKI:def 1; then
Product(y1)" = Product(y2)" by GROUP_1:12; then
A39: y1 = y2 by A21,A30,A31,GROUP_1:9;
x2.i * (x1.i)" in {1_G} by A29,A36,A37,A38,XBOOLE_0:def 4; then
x2.i * (x1.i)" = 1_G by TARSKI:def 1; then
(x1.i)" = (x2.i)" by GROUP_1:12; then
A40: x1.i = x2.i by GROUP_1:9;
x1 = y1 +* (i,x1.i) by Th7;
hence thesis by A39,A40,Th7;
end;
A42: for k be Nat holds P[k] from NAT_1:sch 2(A5,A20);
card(support x1) is Nat;
hence thesis by A3,A4,A42;
end;
theorem
for I be non empty set,
G be strict Group,
F be Group-Family of I
holds
F is internal DirectSumComponents of G,I
iff
(for i be Element of I holds F.i is normal Subgroup of G)
& (ex UF be Subset of G st UF = Union Carrier F & gr(UF) = G)
& for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#](gr(UFi)) /\ [#](F.i) = {1_G}
proof
let I be non empty set,
G be strict Group,
F be Group-Family of I;
A1: dom F = I by PARTFUN1:def 2;
A2: dom(Carrier F) = I by PARTFUN1:def 2;
hereby
assume
A3: F is internal DirectSumComponents of G,I; then
A4: (for i be object st i in I holds F.i is Subgroup of G)
& (for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi)
& (for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x)
& (for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2) by GROUP_19:54; then
A5: F is component-commutative Subgroup-Family of I,G by Def1,Def2;
for x be object st x in Union(Carrier F) holds x in [#]G
proof
let x be object;
assume x in Union(Carrier F); then
x in union rng(Carrier F) by CARD_3:def 4; then
consider Fi be set such that
A6: x in Fi & Fi in rng(Carrier F) by TARSKI:def 4;
consider i be object such that
A7: i in I & Fi = (Carrier F).i by A2,A6,FUNCT_1:def 3;
reconsider i as Element of I by A7;
A8: (Carrier F).i = [#](F.i) by PENCIL_3:7;
F.i is Subgroup of G by A3,GROUP_19:54; then
[#](F.i) c= [#]G by GROUP_2:def 5;
hence thesis by A6,A7,A8;
end; then
Union(Carrier F) c= [#]G; then
reconsider UF = Union(Carrier F) as Subset of G;
A9: for g be Element of G holds g in gr(UF)
proof
let g be Element of G;
consider x be finite-support Function of I,G such that
A10: x in sum F & g = Product x by A3,GROUP_19:54;
x is Function of I,Union(Carrier F) by A10,GROUP_2:41,Th2; then
A11: rng x c= UF by RELAT_1:def 19;
UF c= [#] gr(UF) by GROUP_4:def 4; then
rng x c= [#] gr(UF) by A11; then
reconsider x0 = x as finite-support Function of I,gr(UF) by Th5;
reconsider fx = (x0|support(x0)) * canFS(support x0)
as FinSequence of gr(UF) by FINSEQ_2:32;
Product fx = Product x0 by GROUP_17:def 1
.= g by A10,Th6;
hence thesis;
end; then
A12: gr(UF) = G by GROUP_2:62;
thus for i be Element of I holds F.i is normal Subgroup of G
by A5,A12,Th14;
thus ex UF be Subset of G
st UF = Union (Carrier F) & gr(UF) = G by A9,GROUP_2:62;
thus for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#](gr(UFi)) /\ [#](F.i) = {1_G}
proof
let i be Element of I;
A13: for i be Element of I holds F.i is Subgroup of G
by A3,GROUP_19:54;
per cases;
suppose
I \ {i} = {}; then
A14: Union((Carrier F) | (I \ {i})) = Union((Carrier F) | {})
.= union rng {} by CARD_3:def 4
.= {} by ZFMISC_1:2;
reconsider UFi = {} the carrier of G as Subset of G;
reconsider Fi = F.i as Subgroup of G by A3,GROUP_19:54;
gr(UFi) = (1).G by GROUP_4:30; then
A15: gr(UFi) /\ Fi = (1).G by GROUP_2:85;
[#] gr(UFi) /\ [#]Fi = carr(gr(UFi)) /\ carr(Fi)
.= carr((1).G) by A15,GROUP_2:81
.= {1_G} by GROUP_2:def 7;
hence thesis by A14;
end;
suppose
A16: I \ {i} <> {};
set CFi = (Carrier F) | (I \ {i});
set UFi = Union(CFi);
for x be object st x in UFi holds x in [#]G
proof
let x be object;
assume x in UFi; then
x in union rng(CFi) by CARD_3:def 4; then
consider Fi be set such that
A17: x in Fi & Fi in rng(CFi) by TARSKI:def 4;
A18: dom(CFi) = I \ {i} by A2,RELAT_1:62;
consider j be object such that
A19: j in I \ {i} & Fi = CFi.j by A17,A18,FUNCT_1:def 3;
reconsider j as Element of I by A19;
A20: CFi.j = (Carrier F).j by A19,FUNCT_1:49
.= [#](F.j) by PENCIL_3:7;
F.j is Subgroup of G by A3,GROUP_19:54; then
[#](F.j) c= [#]G by GROUP_2:def 5;
hence thesis by A17,A19,A20;
end; then
reconsider UFi as Subset of G by TARSKI:def 3;
take UFi;
thus UFi = Union(CFi);
A21: 1_G in gr(UFi) by GROUP_2:46;
F.i is Subgroup of G by A3,GROUP_19:54; then
1_G in F.i by GROUP_2:46; then
1_G in [#]gr(UFi) /\ [#](F.i) by A21,XBOOLE_0:def 4; then
A22: {1_G} c= [#]gr(UFi) /\ [#](F.i) by ZFMISC_1:31;
for x be object st x in [#]gr(UFi) /\ [#](F.i) holds x in {1_G}
proof
let x be object;
assume
A23: x in [#]gr(UFi) /\ [#](F.i); then
x in [#]gr(UFi) & x in [#](F.i) by XBOOLE_0:def 4; then
reconsider g = x as Element of G by GROUP_2:def 5,TARSKI:def 3;
set I0 = I \ {i};
set F0 = F | I0;
A24: dom F0 = I0 by A1,RELAT_1:62;
A25: for j be object st j in I0 holds F0.j is Subgroup of G
proof
let j be object;
assume
A26: j in I0; then
A27: F.j = F0.j by FUNCT_1:49;
reconsider j as Element of I by A26;
F0.j is Subgroup of G by A3,A27,GROUP_19:54;
hence thesis;
end; then
for j be object st j in I0 holds F0.j is Group; then
reconsider F0 as Group-Family of I0 by A24,GROUP_19:2;
reconsider F0 as Subgroup-Family of I0,G by A25,Def1;
A29: F0 is component-commutative
proof
let j,k be object,
gj,gk be Element of G;
assume
A28: j in I0 & k in I0 & j <> k;
then reconsider Fj = F0.j, Fk = F0.k as Subgroup of G by Def1;
take Fj,Fk;
thus Fj = F0.j & Fk = F0.k;
assume
A29: gj in Fj & gk in Fk;
reconsider j,k as Element of I by A28;
F0.j = F.j & F0.k = F.k by A28,FUNCT_1:49;
hence gj * gk = gk * gj by A3,A28,A29,GROUP_19:54;
end;
A30: dom(Carrier F0) = I0 by PARTFUN1:def 2;
for j be object st j in dom CFi holds CFi.j = (Carrier F0).j
proof
let j be object;
assume
A31: j in dom CFi; then
A32: j in I0;
then reconsider I0 as non empty set;
reconsider F0 as Group-Family of I0;
reconsider j0 = j as Element of I0 by A31;
reconsider j as Element of I by A32;
(CFi).j = (Carrier F).j by A31,FUNCT_1:49
.= [#](F.j) by PENCIL_3:7
.= [#](F0.j0) by FUNCT_1:49
.= (Carrier F0).j by PENCIL_3:7;
hence thesis;
end; then
A33: UFi = Union Carrier F0 by A2,A30,FUNCT_1:2,RELAT_1:62;
g in gr UFi by A23,XBOOLE_0:def 4; then
consider hi be finite-support Function of I0,gr(UFi) such that
A34: hi in sum F0 & g = Product hi by A16,A29,A33,Th13;
set h = hi +* ({i}-->1_G);
A35: rng h c= rng hi \/ rng({i}-->1_G) by FUNCT_4:17;
rng hi c= [#]G by GROUP_2:def 5,TARSKI:def 3; then
rng hi \/ rng({i}-->1_G) c= [#]G by XBOOLE_1:8; then
A36: rng h c= [#]G by A35;
A37: dom({i}-->1_G) = {i};
dom hi = I0 by FUNCT_2:def 1; then
A38: dom h = I0 \/ {i} by A37,FUNCT_4:def 1
.= I by XBOOLE_1:45; then
reconsider h as Function of I,G by A36,FUNCT_2:2;
A39: for j be object holds j in support h iff j in support hi
proof
let j be object;
hereby
assume
A40: j in support h; then
A41: j in I & h.j <> 1_G by GROUP_19:def 2;
A42: i <> j
proof
assume
A43: j = i; then
A44: j in {i} by TARSKI:def 1;
i in {i} by TARSKI:def 1; then
i in dom({i} --> 1_G); then
h.j = ({i} --> 1_G).j by A43,FUNCT_4:13
.= 1_G by A44,FUNCOP_1:7;
hence contradiction by A40,GROUP_19:def 2;
end; then
not j in {i} by TARSKI:def 1; then
A45: j in I0 by A40,XBOOLE_0:def 5;
not j in dom({i} --> 1_G) by A42,TARSKI:def 1; then
hi.j <> 1_G by A41,FUNCT_4:11; then
hi.j <> 1_gr(UFi) by GROUP_2:44;
hence j in support hi by A45,GROUP_19:def 2;
end;
assume
A46: j in support hi; then
A47: j in I0 & hi.j <> 1_gr(UFi) by GROUP_19:def 2;
A48: j in I & not j in {i} by A46,XBOOLE_0:def 5;
not j in dom({i} --> 1_G) by A46,XBOOLE_0:def 5; then
h.j = hi.j by FUNCT_4:11; then
h.j <> 1_G by A47,GROUP_2:44;
hence j in support h by A48,GROUP_19:def 2;
end; then
A49: support h = support hi by TARSKI:2; then
reconsider h as finite-support Function of I,G by GROUP_19:def 3;
A50: support(h) = dom(h|support(h)) by PARTFUN1:def 2;
A51: support(hi) = dom(hi|support(hi)) by PARTFUN1:def 2;
for x be object st x in dom(h|support(h))
holds (h|support(h)).x = (hi|support(hi)).x
proof
let x be object;
assume
A52: x in dom(h|support(h));
x in dom(hi|support(hi)) by A39,A51,A52; then
A53: x in dom hi /\ support(hi) by RELAT_1:61;
A54: dom hi = I0 & dom({i}-->1_G) = {i} by FUNCT_2:def 1;
thus (h|support(h)).x = h.x by A52,FUNCT_1:47
.= hi.x by A53,A54,FUNCT_4:16,XBOOLE_1:79
.= (hi|support(hi)).x by A39,A51,A52,FUNCT_1:47;
end; then
A55: h|support(h) = hi|support(hi)
by A39,A50,A51,FUNCT_1:2,TARSKI:2;
reconsider fh = (h|support(h)) * canFS(support(h))
as FinSequence of G by FINSEQ_2:32;
reconsider fhi = (hi|support(hi)) * canFS(support(hi))
as FinSequence of gr(UFi) by FINSEQ_2:32;
A56: g = Product fhi by A34,GROUP_17:def 1
.= Product fh by A49,A55,GROUP_19:45
.= Product h by GROUP_17:def 1;
A57: i in {i} by TARSKI:def 1;
A58: dom({i} --> 1_G) = {i};
A59: h in product F
proof
for j be object st j in I holds h.j in (Carrier F).j
proof
let j be object;
assume j in I; then
reconsider j as Element of I;
h.j in [#](F.j)
proof
per cases;
suppose
i = j; then
A60: h.j = ({i} --> 1_G).i by A57,A58,FUNCT_4:13
.= 1_G by A57,FUNCOP_1:7;
F.j is Subgroup of G by A3,GROUP_19:54; then
1_G in F.j by GROUP_2:46;
hence thesis by A60;
end;
suppose
A61: i <> j; then
not j in {i} by TARSKI:def 1; then
A62: j in I0 by XBOOLE_0:def 5;
A63: not j in dom({i} --> 1_G) by A61,TARSKI:def 1;
A64: h.j = hi.j by A63,FUNCT_4:11;
reconsider I0 as non empty set by A62;
reconsider F0 as Group-Family of I0;
reconsider j0 = j as Element of I0 by A62;
hi.j0 in F0.j0 by A34,GROUP_19:5,GROUP_2:40;
hence thesis by A64,FUNCT_1:49;
end;
end;
hence thesis by PENCIL_3:7;
end; then
h in product Carrier F by A2,A38,CARD_3:def 5;
hence thesis by GROUP_7:def 2;
end;
A65: h in sum F
proof
reconsider h0 = h as Element of product F by A59;
support h = support(h0,F) by A4,GROUP_19:9;
hence thesis by GROUP_19:8;
end;
reconsider id1g = I --> 1_G as Function of I,G;
support(id1g) is empty by GROUP_19:12; then
reconsider id1g as finite-support Function of I,G
by GROUP_19:def 3;
A66: 1_product F = id1g by A13,GROUP_19:13; then
reconsider k = 1_product F +* (i,g)
as finite-support Function of I,G by GROUP_19:26;
A67: Product k = g by A66,GROUP_19:21;
k in ProjSet(F,i) by A23,GROUP_12:def 1; then
k in ProjGroup(F,i) by GROUP_12:def 2; then
A68: k in sum F by GROUP_2:40;
dom(1_product F) = I by GROUP_19:3; then
g = k.i by FUNCT_7:31
.= h.i by A3,A56,A65,A67,A68,GROUP_19:54
.= ({i} --> 1_G).i by A57,A58,FUNCT_4:13
.= 1_G by A57,FUNCOP_1:7;
hence x in {1_G} by TARSKI:def 1;
end; then
[#]gr(UFi) /\ [#](F.i) c= {1_G};
hence thesis by A22,XBOOLE_0:def 10;
end;
end;
end;
assume that
A69: for i be Element of I holds F.i is normal Subgroup of G and
A70: ex UF be Subset of G st UF = Union(Carrier F) & gr(UF) = G and
A71: for i be Element of I holds
ex UFi be Subset of G
st UFi = Union((Carrier F) | (I \ {i}))
& [#](gr(UFi)) /\ [#](F.i) = {1_G};
consider UF be Subset of G such that
A72: UF = Union(Carrier F) & gr(UF) = G by A70;
A73: for i be Element of I holds F.i is Subgroup of G by A69;
A74: for i be object st i in I holds F.i is Subgroup of G by A69;
A75: for i,j be Element of I st i <> j holds [#](F.i) /\ [#](F.j) = {1_G}
proof
let i,j be Element of I;
assume
A76: i <> j;
F.i is Subgroup of G by A69; then
1_G in F.i by GROUP_2:46; then
A77: {1_G} c= [#](F.i) by ZFMISC_1:31;
F.j is Subgroup of G by A69; then
1_G in F.j by GROUP_2:46; then
{1_G} c= [#](F.j) by ZFMISC_1:31; then
A78: {1_G} c= [#](F.i) /\ [#](F.j) by A77,XBOOLE_1:19;
for x be object st x in [#](F.i) /\ [#](F.j) holds x in {1_G}
proof
let x be object;
assume
A79: x in [#](F.i) /\ [#](F.j); then
A80: x in [#](F.i) & x in [#](F.j) by XBOOLE_0:def 4;
consider UFj be Subset of G such that
A81: UFj = Union((Carrier F) | (I \ {j}))
& [#]gr(UFj) /\ [#](F.j) = {1_G} by A71;
i in I & not i in {j} by A76,TARSKI:def 1; then
A82: i in (I \ {j}) by XBOOLE_0:def 5;
A83: i in dom((Carrier F) | (I \ {j})) by A2,A82,RELAT_1:62;
((Carrier F) | (I \ {j})).i = (Carrier F).i by A82,FUNCT_1:49
.= [#](F.i) by PENCIL_3:7; then
[#](F.i) c= union rng((Carrier F) | (I \ {j}))
by A83,FUNCT_1:3,ZFMISC_1:74; then
A84: [#](F.i) c= UFj by A81,CARD_3:def 4;
UFj c= [#]gr(UFj) by GROUP_4:def 4; then
x in [#]gr(UFj) by A80,A84;
hence thesis by A79,A81,XBOOLE_0:def 4;
end; then
[#](F.i) /\ [#](F.j) c= {1_G};
hence thesis by A78,XBOOLE_0:def 10;
end;
A85: for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi
proof
let i,j be Element of I, gi,gj be Element of G;
assume
A86: i <> j & gi in F.i & gj in F.j;
A87: F.i is normal Subgroup of G by A69;
A88: F.j is normal Subgroup of G by A69;
A89: [#](F.i) /\ [#](F.j) = {1_G} by A75,A86;
set x = (gi * gj) * (gj * gi)";
A90: gi" in F.i by A86,A87,GROUP_2:51;
A91: gj" in F.j by A86,A88,GROUP_2:51;
A92: gi * gj * gi" in F.j by A86,A88,Th1;
A93: gj * (gi" * gj") in F.i by A87,A90,Th1;
x = (gi * gj) * (gi" * gj") by GROUP_1:17
.= (gi * gj * gi") * gj" by GROUP_1:def 3; then
A94: x in F.j by A88,A91,A92,GROUP_2:50;
x = (gi * gj) * (gi" * gj") by GROUP_1:17
.= gi * (gj * (gi" * gj")) by GROUP_1:def 3; then
x in F.i by A86,A87,A93,GROUP_2:50; then
x in [#](F.i) /\ [#](F.j) by A94,XBOOLE_0:def 4; then
x = 1_G by A89,TARSKI:def 1; then
(gi * gj)" = (gj * gi)" by GROUP_1:12;
hence thesis by GROUP_1:9;
end;
A95: F is component-commutative Subgroup-Family of I,G by A74,A85,Def1,Def2;
A96: for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x
proof
let y be Element of G;
y in gr(UF) by A72; then
consider x be finite-support Function of I,gr UF such that
A97: x in sum F & y = Product x by A72,A95,Th13;
reconsider x as finite-support Function of I,G by A72;
take x;
thus thesis by A72,A97;
end;
for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2 by A71,A95,Th15;
hence F is internal DirectSumComponents of G,I by A73,A85,A96,GROUP_19:54;
end;
begin :: 2. Internal Direct Sum Decomposition for Commutative Group
theorem
for I be non empty set,
G be commutative Group,
F be Group-Family of I
holds
F is internal DirectSumComponents of G,I
iff
(for i be Element of I holds F.i is Subgroup of G)
&(for i,j be Element of I st i <> j holds
[#] (F.i) /\ [#] (F.j) = {1_G})
&(for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product(x))
&(for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product(x1) = Product(x2)
holds x1 = x2)
proof
let I be non empty set,
G be commutative Group,
F be Group-Family of I;
hereby
assume
A1: F is internal DirectSumComponents of G,I; then
A2: (for i be Element of I holds F.i is Subgroup of G)
& (for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi)
& (for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product x)
& (for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product x1 = Product x2
holds x1 = x2) by GROUP_19:54;
A3: for i be object st i in I holds F.i is Subgroup of G
by A1,GROUP_19:54;
A4: for i,j be Element of I st i <> j holds [#](F.i) /\ [#](F.j) = {1_G}
proof
let i,j be Element of I;
assume
A5: i <> j;
A6: F.i is Subgroup of G by A1,GROUP_19:54; then
A7: 1_G in F.i by GROUP_2:46;
A8: F.j is Subgroup of G by A1,GROUP_19:54; then
1_G in F.j by GROUP_2:46; then
1_G in [#](F.j) /\ [#](F.i) by A7,XBOOLE_0:def 4; then
A9: {1_G} c= [#](F.i) /\ [#](F.j) by ZFMISC_1:31;
for x be object st x in [#](F.i) /\ [#](F.j) holds x in {1_G}
proof
let x be object;
assume
A10: x in [#](F.i) /\ [#](F.j);
reconsider gi = x as Element of F.i by A10,XBOOLE_0:def 4;
reconsider gj = x as Element of F.j by A10;
gi in G by A6,GROUP_2:41; then
reconsider ggi = gi as Element of G;
gj in G by A8,GROUP_2:41; then
reconsider ggj = gj as Element of G;
x = 1_G
proof
assume
A11: x <> 1_G;
set xi = 1_product F +* (i,gi);
set xj = 1_product F +* (j,gj);
A12: xi in sum F by GROUP_19:25,GROUP_2:46; then
reconsider xi as finite-support Function of I,G by A3,GROUP_19:10;
A13: xj in sum F by GROUP_19:25,GROUP_2:46; then
reconsider xj as finite-support Function of I,G by A3,GROUP_19:10;
A14: 1_product F = I --> 1_G by A2,GROUP_19:13; then
Product xi = ggj by GROUP_19:21
.= Product xj by A14,GROUP_19:21; then
A15: xi = xj by A1,A12,A13,GROUP_19:54;
A16: dom(1_product F) = I by GROUP_19:3;
xj.i = (1_product F).i by A5,FUNCT_7:32
.= 1_F.i by GROUP_7:6
.= 1_G by A6,GROUP_2:44;
hence contradiction by A11,A15,A16,FUNCT_7:31;
end;
hence x in {1_G} by TARSKI:def 1;
end; then
[#](F.i) /\ [#](F.j) c= {1_G};
hence thesis by A9,XBOOLE_0:def 10;
end;
thus (for i be Element of I holds F.i is Subgroup of G)
& (for i,j be Element of I st i <> j holds
[#] (F.i) /\ [#] (F.j) = {1_G})
& (for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product(x))
& (for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product(x1) = Product(x2)
holds x1 = x2) by A1,A4,GROUP_19:54;
end;
assume
A17: (for i be Element of I holds F.i is Subgroup of G)
& (for i,j be Element of I st i <> j holds
[#] (F.i) /\ [#] (F.j) = {1_G})
& (for y be Element of G
ex x be finite-support Function of I,G
st x in sum F & y = Product(x))
& (for x1,x2 be finite-support Function of I,G
st x1 in sum F & x2 in sum F & Product(x1) = Product(x2)
holds x1 = x2);
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j
holds gi * gj = gj * gi;
hence F is internal DirectSumComponents of G,I by A17,GROUP_19:54;
end;
begin :: 3. Equivalence between Internal and External Direct Sum
theorem Th19:
for I be non empty set,
G be Group,
F be Subgroup-Family of I,G,
h be Homomorphism of sum F,G,
a be finite-support Function of I,G
st a in sum F
& for i be Element of I, x be Element of F.i
holds h.(1ProdHom(F,i).x) = x
holds h.a = Product a
proof
let I be non empty set,
G be Group,
F be Subgroup-Family of I,G,
h be Homomorphism of sum F,G,
a be finite-support Function of I,G;
assume that
A1: a in sum F and
A2: for i be Element of I, x be Element of F.i
holds h.(1ProdHom(F,i).x) = x;
A3: for i be object st i in I holds F.i is Subgroup of G by Def1;
defpred P[Nat] means
for b be finite-support Function of I,G st b in sum F holds
card support(b) = $1 implies h.b = Product b;
A4: P[0]
proof
let b be finite-support Function of I,G;
assume b in sum F;
assume card support(b) = 0; then
A5: support(b) = {}; then
b = 1_product F by A3,GROUP_19:14
.= 1_sum F by GROUP_2:44; then
h.b = 1_G by GROUP_6:31;
hence thesis by A5,GROUP_19:15;
end;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: P[k];
let b be finite-support Function of I,G;
assume
A8: b in sum F;
assume
A9: card support(b) = k+1; then
support(b) is not empty; then
consider i be object such that
A10: i in support(b) by XBOOLE_0:def 1;
A11: b.i <> 1_G & i in I by A10,GROUP_19:def 2;
reconsider i as Element of I by A10;
set c = b +* (i,1_F.i);
c in sum F by A8,GROUP_19:25; then
reconsider c as Element of sum F;
F.i is Subgroup of G by Def1; then
A12: 1_F.i = 1_G by GROUP_2:44; then
reconsider c0 = c as finite-support Function of I,G by GROUP_19:26;
A13: b in product F by A8,GROUP_2:40;
A14: b.i in F.i by A8,GROUP_19:5,GROUP_2:40; then
1ProdHom(F,i).(b.i) in ProjGroup(F,i) by FUNCT_2:5; then
1ProdHom(F,i).(b.i) in sum F by GROUP_2:40; then
reconsider d = 1ProdHom(F,i).(b.i) as Element of sum F;
A15: d = 1_product F +* (i, b.i) by A14,GROUP_12:def 3;
A16: d is Element of product F by GROUP_2:42;
A17: support(d,F) = {i} by A11,A12,A14,A15,A16,GROUP_19:18;
A18: i in dom b by A11,A13,GROUP_19:3;
A19: b = c * d
proof
reconsider c1 = c, d1 = d as Element of product F by GROUP_2:42;
A20: support(c1,F) misses support(d1,F)
proof
c.i = 1_F.i by A18,FUNCT_7:31; then
not ex G being Group st G = F.i & c.i <> 1_G & i in I;
then not i in support(c,F) by GROUP_19:def 1;
hence thesis by A17,ZFMISC_1:50;
end;
A21: dom(i .--> b.i) = {i};
A22: dom(1_product F) = I by GROUP_19:3;
A23: d1|support(d1,F)
= (1_product F +* (i,b.i)) | {i} by A11,A12,A14,A15,GROUP_19:18
.= (1_product F +* (i .--> b.i)) | {i} by A22,FUNCT_7:def 3
.= i .--> b.i by A21,FUNCT_4:23;
A24: i in dom c by A18,FUNCT_7:30;
thus b = c1 +* (i,b.i) by Th7
.= c1 +* (d1|support(d1,F)) by A23,A24,FUNCT_7:def 3
.= c1 * d1 by A20,GROUP_19:31
.= c * d by GROUP_2:43;
end;
A25: h.c0 = Product c0
proof
A26: c0 in sum F;
card support(c0) = card support(b) - 1 by A10,A12,GROUP_19:30
.= k by A9;
hence thesis by A7,A26;
end;
for i,j be Element of I, gi,gj be Element of G
st i <> j & gi in F.i & gj in F.j holds gi * gj = gj * gi
proof
let i,j be Element of I;
let gi,gj be Element of G;
assume that
A27: i <> j and
A28: gi in F.i and
A29: gj in F.j;
set ai = 1ProdHom(F,i).gi;
A30: ai in ProjGroup(F,i) by A28,FUNCT_2:5; then
ai in sum F by GROUP_2:40; then
reconsider ai as Element of sum F;
reconsider bi = ai as Element of product F by GROUP_2:42;
set aj = 1ProdHom(F,j).gj;
A31: aj in ProjGroup(F,j) by A29,FUNCT_2:5; then
aj in sum F by GROUP_2:40; then
reconsider aj as Element of sum F;
reconsider bj = aj as Element of product F by GROUP_2:42;
A32: gi = h.ai by A2,A28;
gi * gj = h.ai * h.aj by A2,A29,A32
.= h.(ai * aj) by GROUP_6:def 6
.= h.(bi * bj) by GROUP_2:43
.= h.(bj * bi) by A27,A30,A31,GROUP_12:7
.= h.(aj * ai) by GROUP_2:43
.= h.aj * h.ai by GROUP_6:def 6
.= gj * gi by A2,A29,A32;
hence thesis;
end; then
A33: F is component-commutative;
A34: b in product F by A8,GROUP_2:40;
h.b = h.c * h.d by A19,GROUP_6:def 6
.= Product(c0) * b.i by A2,A14,A25
.= Product b by A33,A34,Th8;
hence thesis;
end;
A35: for k be Nat holds P[k] from NAT_1:sch 2(A4,A6);
consider k be Nat such that
A36: card support(a) = k;
thus thesis by A1,A35,A36;
end;
theorem
for I be non empty set,
G be Group,
M be DirectSumComponents of G,I
holds
ex f be Homomorphism of sum M,G,
N be internal DirectSumComponents of G,I
st f is bijective
& for i be Element of I holds
ex qi be Homomorphism of M.i,N.i
st qi = f * 1ProdHom(M,i)
& qi is bijective
proof
let I be non empty set;
let G be Group;
let M be DirectSumComponents of G,I;
consider f be Homomorphism of sum M,G such that
A1: f is bijective by GROUP_19:def 8;
deffunc FN(Element of I) = f.:ProjGroup(M,$1);
consider N be Function such that
A2: dom N = I and
A3: for i be Element of I st i in I holds N.i = FN(i) from CLASSES1:sch 2;
A4: for i be object st i in I holds N.i is strict Subgroup of G
proof
let i be object;
assume i in I; then
reconsider i as Element of I;
N.i = f.:ProjGroup(M,i) by A3;
hence thesis;
end; then
for i be object st i in I holds N.i is Group; then
reconsider N as Group-Family of I by A2,GROUP_19:2;
for i be object st i in I holds N.i is Subgroup of G by A4; then
reconsider N as Subgroup-Family of I,G by Def1;
A5: for i be Element of I holds N.i is Subgroup of G by A4;
deffunc FQ(Element of I) = f * 1ProdHom(M,$1);
consider q being Function such that
A6: dom q = I and
A7: for i being Element of I st i in I holds q.i = FQ(i)
from CLASSES1:sch 2;
reconsider q as non empty Function by A6;
A8: now
let i be Element of I;
A9: rng 1ProdHom(M,i) = [#]ProjGroup(M,i) by FUNCT_2:def 3;
reconsider fi = f|ProjGroup(M,i) as Homomorphism of ProjGroup(M,i),G;
dom fi = [#]ProjGroup(M,i) by FUNCT_2:def 1; then
A10: f * 1ProdHom(M,i) = fi * 1ProdHom(M,i) by A9,RELAT_1:165;
A11: rng fi = f.:([#]ProjGroup(M,i)) by RELAT_1:115
.= [#](f.:ProjGroup(M,i)) by GRSOLV_1:8
.= [#](N.i) by A3;
Image fi = f.:ProjGroup(M,i)
.= N.i by A3; then
reconsider fi as Homomorphism of ProjGroup(M,i),N.i by GROUP_6:49;
A12: fi is one-to-one by A1,FUNCT_1:52;
A13: fi is onto by A11,FUNCT_2:def 3;
reconsider qi = fi * 1ProdHom(M,i) as Homomorphism of M.i,N.i;
take qi;
thus qi = q.i by A7,A10;
thus qi is bijective by A12,A13,GROUP_6:64;
end; then
A14: for i be Element of I holds
ex qi be Homomorphism of M.i,N.i
st qi = q.i & qi is bijective;
reconsider r = SumMap(M,N,q) as Homomorphism of sum M,sum N;
A15: r is bijective by A6,A14,GROUP_19:41;
reconsider s = r" as Homomorphism of sum N,sum M
by A6,A14,GROUP_19:41,GROUP_6:62;
A16: s is bijective by A15,GROUP_6:63;
reconsider g = f * s as Function;
reconsider g as Homomorphism of sum N,G;
A17: g is bijective by A1,A16,GROUP_6:64; then
reconsider N as DirectSumComponents of G,I by GROUP_19:def 8;
for i be Element of I, n be Element of N.i holds g.(1ProdHom(N,i).n) = n
proof
let i be Element of I;
let n be Element of N.i;
consider qi be Homomorphism of M.i,N.i such that
A18: qi = q.i and
A19: qi is bijective by A8;
A20: dom qi = [#](M.i) by FUNCT_2:def 1;
rng qi = [#](N.i) by A19,FUNCT_2:def 3; then
consider m be object such that
A21: m in [#](M.i) and
A22: qi.m = n by A20,FUNCT_1:def 3;
reconsider m as Element of M.i by A21;
for i be Element of I holds
q.i is Homomorphism of M.i,N.i
proof
let i be Element of I;
ex qi be Homomorphism of M.i,N.i st
qi = q.i & qi is bijective by A8;
hence thesis;
end; then
A24: r.(1ProdHom(M,i).m) = 1ProdHom(N,i).n by A6,A18,A22,GROUP_19:42;
A25: dom r = [#]sum M by FUNCT_2:def 1;
1ProdHom(M,i).m in ProjGroup(M,i); then
A26: 1ProdHom(M,i).m in sum M by GROUP_2:40;
A27: dom s = [#]sum N by FUNCT_2:def 1;
1ProdHom(N,i).n in ProjGroup(N,i); then
A28: 1ProdHom(N,i).n in sum N by GROUP_2:40;
A29: qi = f * 1ProdHom(M,i) by A7,A18;
A30: m in dom 1ProdHom(M,i) by A21,FUNCT_2:def 1;
g.(1ProdHom(N,i).n) = f.(s.(1ProdHom(N,i).n)) by A27,A28,FUNCT_1:13
.= f.(1ProdHom(M,i).m) by A15,A24,A25,A26,FUNCT_1:34
.= n by A22,A29,A30,FUNCT_1:13;
hence thesis;
end; then
for a be finite-support Function of I,G st a in sum N
holds g.a = Product(a) by Th19; then
reconsider N as internal DirectSumComponents of G,I
by A5,A17,GROUP_19:def 9;
take f, N;
for i be Element of I holds
ex qi be Homomorphism of M.i,N.i
st qi = f * 1ProdHom(M,i) & qi is bijective
proof
let i be Element of I;
consider qi be Homomorphism of M.i,N.i such that
A31: qi = q.i and
A32: qi is bijective by A8;
take qi;
thus thesis by A7,A31,A32;
end;
hence thesis by A1;
end;