:: Nilpotent Groups
:: by Dailu Li , Xiquan Liang and Yanhong Men
::
:: Received November 10, 2009
:: Copyright (c) 2009-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 REALSET1, FINSEQ_1, GROUP_3, FUNCT_1, RLSUB_1, GROUP_2, RELAT_1,
GROUP_6, XBOOLE_0, QC_LANG1, GROUP_1, GRAPH_1, ARYTM_1, ARYTM_3,
ZFMISC_1, NUMBERS, SUBSET_1, XXREAL_1, STRUCT_0, NEWTON, TARSKI, NAT_1,
PARTFUN1, PRE_TOPC, XXREAL_0, CARD_1, GROUP_4, NATTRA_1, CARD_3, BINOP_1,
GROUP_5, GRSOLV_1, GRNILP_1, BCIALG_2, ALGSTR_0;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, STRUCT_0, ALGSTR_0, PARTFUN1, FINSEQ_1, ZFMISC_1, ORDINAL1,
XXREAL_0, NUMBERS, REALSET1, DOMAIN_1, GROUP_1, GROUP_3, GR_CY_1,
GRSOLV_1, GROUP_4, GROUP_5, GROUP_2, GROUP_6;
constructors BINOP_1, BINARITH, GROUP_4, GROUP_5, GRSOLV_1, RELSET_1, GR_CY_1,
REALSET1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, INT_1,
FINSEQ_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, GROUP_6, GR_CY_1,
ALGSTR_0, RELSET_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, GRSOLV_1;
equalities GROUP_2, GROUP_6, FINSEQ_1, GROUP_4, ALGSTR_0, GROUP_3, GROUP_5,
GRSOLV_1, REALSET1;
expansions TARSKI;
theorems FINSEQ_1, GROUP_2, GROUP_3, TARSKI, GROUP_5, GROUP_6, FINSEQ_2,
FUNCT_2, RELAT_1, XBOOLE_0, XBOOLE_1, NAT_1, GROUP_1, PARTFUN1, FINSEQ_3,
GROUP_4, FUNCT_1, GRSOLV_1, STRUCT_0, GROUP_11, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, FINSEQ_1, FINSEQ_2, XFAMILY;
begin
reserve x,y for set,
G for Group,
A,B,H,H1,H2 for Subgroup of G,
a,b,c for Element of G,
F,F1 for FinSequence of the carrier of G,
I,I1 for FinSequence of INT,
i,j for Element of NAT;
theorem
a |^ b = a * [.a,b.]
proof
a * [.a,b.] = a * ((a" * b") * (a * b)) by GROUP_1:def 3
.= a * (a" * (b" * (a * b))) by GROUP_1:def 3
.= (a * a") * (b" * (a * b)) by GROUP_1:def 3
.= 1_G * (b" * (a * b)) by GROUP_1:def 5
.= b" * (a * b) by GROUP_1:def 4
.= b" * a * b by GROUP_1:def 3;
hence thesis;
end;
theorem
[.a,b.]" = [.a,b".]|^b
proof
thus [.a,b.]" = ((a" * b") * (a * b))" by GROUP_1:def 3
.= (a * b)" * (a" * b")" by GROUP_1:17
.= (b" * a") * (a" * b")" by GROUP_1:17
.= (b" * a") * (b"" * a"") by GROUP_1:17
.= b" * (a" * (b * a)) by GROUP_1:def 3
.= b" * (a" * b * a) by GROUP_1:def 3
.= b" * (a" * b * a) * 1_G by GROUP_1:def 4
.= b" * (a" * b * a) * (b" * b) by GROUP_1:def 5
.= b" * (a" * b * a) * b" * b by GROUP_1:def 3
.= [.a,b".]|^b by GROUP_1:def 3;
end;
theorem
[.a,b.]" = [.a",b.]|^a
proof
thus [.a,b.]" = ((a" * b") * (a * b))" by GROUP_1:def 3
.= (a * b)" * (a" * b")" by GROUP_1:17
.= (b" * a") * (a" * b")" by GROUP_1:17
.= (b" * a") * (b"" * a"") by GROUP_1:17
.= b" * (a" * (b * a)) by GROUP_1:def 3
.= b" * (a" * b * a) by GROUP_1:def 3
.= 1_G * (b" * (a" * b * a)) by GROUP_1:def 4
.= a" * a * (b" * (a" * b * a)) by GROUP_1:def 5
.= a" * (a * (b" * (a" * b * a))) by GROUP_1:def 3
.= a" * ((a * b") * ((a" * b) * a)) by GROUP_1:def 3
.= a" * (((a * b") * (a" * b)) * a) by GROUP_1:def 3
.= a" * ((a * b") * (a" * b)) * a by GROUP_1:def 3
.= [.a",b.]|^a by GROUP_5:16;
end;
theorem Th4:
([.a,b".]|^ b)" = [.b",a.]|^ b
proof
thus ([.a,b".]|^ b)" = [.a,b".]"|^ b by GROUP_3:26
.= [.b",a.]|^ b by GROUP_5:22;
end;
theorem Th5:
[.a,b",c.] |^ b = [.[.a,b".]|^ b,c|^ b.]
proof
A1:[.a,b",c.] |^ b
= b" * ([.a,b".]" * 1_G * c" * [.a,b".] * c) * b by GROUP_1:def 4
.= b" * (([.a,b".]" * (b * b")) * c" * [.a,b".] * c) * b by GROUP_1:def 5
.= b" * (([.a,b".]" * b * b") * c" * [.a,b".] * c) * b by GROUP_1:def 3
.= b" * ((([.a,b".]" * b) * b") * c" * ([.a,b".] * c)) * b by GROUP_1:def 3
.= b" * (([.a,b".]" * b) * b" * (c" * ([.a,b".] * c))) * b by GROUP_1:def 3
.= (b" * (([.a,b".]" * b) * (b" * (c" * ([.a,b".] * c))))) * b
by GROUP_1:def 3
.= ((b" * ([.a,b".]" * b)) * (b" * (c" * ([.a,b".] * c)))) * b
by GROUP_1:def 3
.= (([.a,b".]"|^ b) * (b" * (c" * ([.a,b".] * c)))) * b by GROUP_1:def 3
.= [.a,b".]"|^ b * ((b" * (c" * ([.a,b".] * c))) * b) by GROUP_1:def 3
.= [.a,b".]"|^ b * ([.a,b".]|^ c |^ b) by GROUP_1:def 3
.= [.b",a.]|^ b * ([.a,b".]|^ c |^ b) by GROUP_5:22
.= [.b",a.]|^ b * [.a,b".]|^ (c * b) by GROUP_3:24;
[.[.a,b".]|^ b,c|^ b.]
= [.b",a.]|^ b * (c|^ b)" * ([.a,b".]|^ b) * (c|^ b) by Th4
.= [.b",a.]|^ b * (c"|^ b) * ([.a,b".]|^ b) * (c|^ b) by GROUP_3:26
.= [.b",a.]|^ b * (b" * c" * b) * ((b" * [.a,b".]) * b) * (b" * (c * b))
by GROUP_1:def 3
.= [.b",a.]|^ b * (b" * c" * b) * ((b" * [.a,b".]) * b * (b" * (c * b)))
by GROUP_1:def 3
.= [.b",a.]|^ b * ((b" * c") * b) * ((b" * [.a,b".]) * (b * (b" * (c * b))))
by GROUP_1:def 3
.= [.b",a.]|^ b * ((b" * c") * b) * ((b" * [.a,b".]) * (b * b" * (c * b)))
by GROUP_1:def 3
.= [.b",a.]|^ b * ((b" * c") * b) * ((b" * [.a,b".]) * (1_G * (c * b)))
by GROUP_1:def 5
.= [.b",a.]|^ b * ((b" * c") * b) * ((b" * [.a,b".]) * (c * b))
by GROUP_1:def 4
.= [.b",a.]|^ b * (((b" * c") * b) * ((b" * [.a,b".]) * (c * b)))
by GROUP_1:def 3
.= [.b",a.]|^ b * ((b" * c") * (b * ((b" * [.a,b".]) * (c * b))))
by GROUP_1:def 3
.= [.b",a.]|^ b * (((b" * c") * ((b * (b" * [.a,b".])) * (c * b))))
by GROUP_1:def 3
.= [.b",a.]|^ b * (((b" * c") * ((b * b" * [.a,b".]) * (c * b))))
by GROUP_1:def 3
.= [.b",a.]|^ b * (((b" * c") * ((1_G * [.a,b".]) * (c * b))))
by GROUP_1:def 5
.= [.b",a.]|^ b * (((b" * c") * ([.a,b".] * (c * b)))) by GROUP_1:def 4
.= [.b",a.]|^ b * (((b" * c") * [.a,b".] * (c * b))) by GROUP_1:def 3
.= [.b",a.]|^ b * [.a,b".] |^ (c * b) by GROUP_1:17;
hence thesis by A1;
end;
theorem Th6:
[.a,b".]|^ b = [.b,a.]
proof
thus [.a,b".]|^ b = b" * ((a" * b"" * a * b") * b) by GROUP_1:def 3
.= b" * (((a" * b"" * a) * (b" * b))) by GROUP_1:def 3
.= b" * ((a" * b"" * a) * 1_G) by GROUP_1:def 5
.= b" * (a" * b"" * a) by GROUP_1:def 4
.= b" * (a" * (b * a)) by GROUP_1:def 3
.= (b" * a") * (b * a) by GROUP_1:def 3
.= b" * a" * b * a by GROUP_1:def 3
.= [.b,a.];
end;
theorem Th7:
[.a,b",c.] |^ b = [.b,a,c|^ b.]
proof
[.a,b",c.] |^ b = [.[.a,b".]|^ b,c|^ b.] by Th5;
hence thesis by Th6;
end;
theorem
[.a,b,c|^ a.] * [.c,a,b|^ c.] * [.b,c,a|^ b.] = 1_G
proof
[.a,b,c|^ a.] = [.b,a",c.]|^ a & [.c,a,b|^ c.] = [.a,c",b.]|^ c &
[.b,c,a|^ b.] = [.c,b",a.]|^b by Th7;
hence thesis by GROUP_5:46;
end;
theorem Th9:
[.A,B.] is Subgroup of [.B,A.]
proof
now let a;
assume a in [.A,B.];
then consider F,I such that len F = len I and
A1: rng F c= commutators(A,B) and
A2: a = Product(F |^ I) by GROUP_5:61;
deffunc F(Nat) = (F/.$1)";
consider F1 such that
A3: len F1 = len F and
A4: for k be Nat st k in dom F1 holds F1.k = F(k) from FINSEQ_2:sch 1;
A5: dom F1 = Seg len F by A3,FINSEQ_1:def 3;
deffunc F(Nat) = @(- @(I/.$1));
consider I1 such that
A6: len I1 = len F and
A7: for k be Nat st k in dom I1 holds I1.k = F(k) from FINSEQ_2:sch 1;
A8: dom F = Seg len F by FINSEQ_1:def 3;
A9: dom F1 = dom F by A3,FINSEQ_3:29;
A10: dom I1 = dom F by A6,FINSEQ_3:29;
set J = F1 |^ I1;
A11: len J = len F & len(F |^ I) = len F by A3,GROUP_4:def 3;
then
A12: dom(F |^ I) = Seg len F by FINSEQ_1:def 3;
now
let k be Nat;
assume
A13: k in dom(F |^ I); then
A14: k in dom F by A12,FINSEQ_1:def 3;
J.k = (F1/.k) |^ @(I1/.k) & F1/.k = F1.k & F1.k = (F/.k)" &
I1.k = (I1/.k) & @(I1/.k) = I1/.k &
I1.k = @(- @(I/.k)) & @(- @(I/.k)) = - @(I/.k)
by A4,A7,A8,A9,A10,A13,A12,GROUP_4:def 3,PARTFUN1:def 6;
then J.k = ((F/.k)" |^ @(I/.k))" by GROUP_1:36
.= ((F/.k) |^ @(I/.k))"" by GROUP_1:37
.= (F/.k) |^ @(I/.k);
hence (F |^ I).k = J.k by A14,GROUP_4:def 3;
end; then
A15: J = F |^ I by A11,FINSEQ_2:9;
rng F1 c= commutators(B,A)
proof
let x be object;
assume x in rng F1;
then consider y being object such that
A16: y in dom F1 and
A17: F1.y = x by FUNCT_1:def 3;
reconsider y as Element of NAT by A16;
y in dom F by A3,A16,FINSEQ_3:29;
then F.y in rng F by FUNCT_1:def 3;
then consider b,c such that
A18: F.y = [.b,c.] and
A19: b in A & c in B by A1,GROUP_5:52;
x = (F/.y)" & F/.y = F.y by A16,A4,A8,A17,A5,PARTFUN1:def 6;
then x = [.c,b.] by A18,GROUP_5:22;
hence thesis by A19,GROUP_5:52;
end;
hence a in [.B,A.] by A2,A3,A6,A15,GROUP_5:61;
end;
hence thesis by GROUP_2:58;
end;
definition let G,A,B;
redefine func [.A,B.]; :: redefines [. (GROUP_5, definition)
commutativity
proof let A,B;
[.A,B.] is Subgroup of [.B,A.] & [.B,A.] is Subgroup of [.A,B.] by Th9;
hence thesis by GROUP_2:55;
end;
end;
theorem Th10:
B is Subgroup of A implies commutators(A,B) c= carr A
proof
assume
A1: B is Subgroup of A;
let x be object;
assume x in commutators(A,B);
then consider a,b such that
A2: x = [.a,b.] & a in A & b in B by GROUP_5:52;
A3: b in A by A1,A2,GROUP_2:40;
then A4: a * b in A by A2,GROUP_2:50;
a" in A & b" in A by A2,A3,GROUP_2:51;
then a" * b" in A by GROUP_2:50;
then
A5: (a" * b") * (a * b) in A by A4,GROUP_2:50;
[.a,b.] = (a" * b") * (a * b) by GROUP_1:def 3;
hence thesis by A2,A5,STRUCT_0:def 5;
end;
Lm1: gr carr A is Subgroup of A
proof
set A9 = multMagma(# the carrier of A, the multF of A #);
the carrier of A9 c= the carrier of G &
the multF of A9 = (the multF of G) || the carrier of A by GROUP_2:def 5;
then reconsider A9 = multMagma(# the carrier of A, the multF of A #)
as strict Subgroup of G by GROUP_2:def 5;
A1: gr carr A is Subgroup of A9 by GROUP_4:def 4;
A9 is Subgroup of A by GROUP_2:57;
hence thesis by A1,GROUP_2:56;
end;
theorem Th11:
B is Subgroup of A implies [.A,B.] is Subgroup of A
proof
A1: gr carr A is Subgroup of A by Lm1;
assume B is Subgroup of A;
then commutators(A,B) c= carr A by Th10;
then [.A,B.] is Subgroup of gr carr A by GROUP_4:32;
hence thesis by A1,GROUP_2:56;
end;
theorem
B is Subgroup of A implies [.B,A.] is Subgroup of A by Th11;
Lm2: A is Subgroup of (Omega).G
proof
dom the multF of G c= [:the carrier of G, the carrier of G:];
then the multF of G
= (the multF of (Omega).G) || the carrier of (Omega).G by RELAT_1:68;
then G is Subgroup of (Omega).G by GROUP_2:def 5;
hence thesis by GROUP_2:56;
end;
theorem
[.H1, (Omega).G.] is Subgroup of H2
implies [.H1 /\ H,H.] is Subgroup of H2 /\ H
proof
assume
A1: [.H1, (Omega).G.] is Subgroup of H2;
H1 /\ H is Subgroup of H by GROUP_2:88;
then
A2:[.H1 /\ H,H.] is Subgroup of H by Th11;
A3: H is Subgroup of (Omega).G by Lm2;
H1 /\ H is Subgroup of H1 by GROUP_2:88;
then [.H1 /\ H,H.] is Subgroup of [.H1, (Omega).G.] by A3,GROUP_5:66;
then [.H1 /\ H,H.] is Subgroup of H2 by A1,GROUP_2:56;
hence thesis by A2,GROUP_2:91;
end;
theorem
[.H1,H2.] is Subgroup of [.H1,(Omega).G.]
proof
A1: H2 is Subgroup of (Omega).G by Lm2;
H1 is Subgroup of H1 by GROUP_2:54;
hence thesis by A1,GROUP_5:66;
end;
Lm3: for N being normal Subgroup of G holds [.N,H.] is Subgroup of N
proof
let N be normal Subgroup of G;
the carrier of N c= the carrier of G &
the multF of N = (the multF of G) || the carrier of N by GROUP_2:def 5;
then reconsider N9 = multMagma(# the carrier of N, the multF of N #)
as strict Subgroup of G by GROUP_2:def 5;
now
let a be Element of G;
the carrier of N |^ a = (carr N) |^ a by GROUP_3:def 6
.= (carr N9) |^ a .= the carrier of N9 |^ a by GROUP_3:def 6;
hence N9 |^ a = N |^ a by GROUP_2:59
.= multMagma(# the carrier of N9,the multF of N9 #) by GROUP_3:def 13;
end;
then reconsider N9 as strict normal Subgroup of G by GROUP_3:def 13;
[.N9,H.] = [.N,H.]; then
A1: [.N,H.] is Subgroup of N9 by GROUP_5:67;
N9 is Subgroup of N by GROUP_2:57;
hence thesis by A1,GROUP_2:56;
end;
theorem Th15:
A is normal Subgroup of G iff [.A,(Omega).G.] is Subgroup of A
proof
thus A is normal Subgroup of G implies [.A,(Omega).G.] is
Subgroup of A by Lm3;
assume
A1: [.A,(Omega).G.] is Subgroup of A;
for b holds b * A c= A * b
proof
let b;
let x be object;
assume
A2: x in b * A;
then reconsider x as Element of G;
consider Z be Element of G such that
A3: x = b * Z & Z in A by A2,GROUP_2:103;
A4: Z" in A by A3,GROUP_2:51;
b" in (Omega).G by STRUCT_0:def 5; then
[.b",Z".] in [.(Omega).G,A.] by A4,GROUP_5:65;
then [.b",Z".] in A by A1,GROUP_2:40; then
A5: (b * Z * b" * Z") * Z in A by A3,GROUP_2:50;
A6: (b * Z * b" * Z") * Z = ((b * Z) * b") * (Z" * Z) by GROUP_1:def 3
.= ((b * Z) * b") * 1_G by GROUP_1:def 5
.= b * Z * b" by GROUP_1:def 4;
(b * Z * b") * b = (b * Z) * (b" * b) by GROUP_1:def 3
.= b * Z * 1_G by GROUP_1:def 5
.= b * Z by GROUP_1:def 4;
hence thesis by A3,A5,A6,GROUP_2:104;
end;
hence thesis by GROUP_3:118;
end;
definition let G;
func the_normal_subgroups_of G -> set means :Def1:
for x being object holds x in it iff x is strict normal Subgroup of G;
existence
proof
defpred P[object,object] means
ex H being strict normal Subgroup of G st $2 = H & $1 = the carrier of H;
defpred P[set] means ex H being strict normal Subgroup of G st $1 = the
carrier of H;
consider B being set such that
A1: for x being set holds x in B iff x in bool the carrier of G & P[x]
from XFAMILY:sch 1;
A2: for x,y1,y2 being object st P[x,y1] & P[x,y2] holds y1 = y2 by GROUP_2:59;
consider f being Function such that
A3: for x,y being object holds [x,y] in f iff x in B & P[x,y] from
FUNCT_1:sch 1(A2);
for x being object holds x in B iff ex y being object st [x,y] in f
proof
let x be object;
thus x in B implies ex y being object st [x,y] in f
proof
assume
A4: x in B;
then consider H being strict normal Subgroup of G such that
A5: x = the carrier of H by A1;
reconsider y = H as set by TARSKI:1;
take y;
thus thesis by A3,A4,A5;
end;
given y be object such that
A6: [x,y] in f;
thus thesis by A3,A6;
end;
then
A7: B = dom f by XTUPLE_0:def 12;
for y being object
holds y in rng f iff y is strict normal Subgroup of G
proof
let y be object;
thus y in rng f implies y is strict normal Subgroup of G
proof
assume y in rng f;
then consider x be object such that
A8: x in dom f & y = f.x by FUNCT_1:def 3;
[x,y] in f by A8,FUNCT_1:def 2;
then ex H being strict normal Subgroup of G st y = H & x = the carrier
of H by A3;
hence thesis;
end;
assume y is strict normal Subgroup of G;
then reconsider H = y as strict normal Subgroup of G;
reconsider x = the carrier of H as set;
A9: y is set by TARSKI:1;
the carrier of H c= the carrier of G by GROUP_2:def 5;
then
A10: x in dom f by A1,A7;
then [x,y] in f by A3,A7;
then y = f.x by A10,FUNCT_1:def 2,A9;
hence thesis by A10,FUNCT_1:def 3;
end;
hence thesis;
end;
uniqueness
proof
defpred P[object] means $1 is strict normal Subgroup of G;
let A1,A2 be set;
assume
A11: for x being object holds x in A1 iff P[x];
assume
A12: for x being object holds x in A2 iff P[x];
thus thesis from XBOOLE_0:sch 2(A11,A12);
end;
end;
registration let G;
cluster the_normal_subgroups_of G -> non empty;
coherence
proof
the strict normal Subgroup of G in the_normal_subgroups_of G by Def1;
hence thesis;
end;
end;
theorem Th16:
for F being FinSequence of the_normal_subgroups_of G
for j st j in dom F holds F.j is strict normal Subgroup of G
proof
let F be FinSequence of the_normal_subgroups_of G;
let j;
assume j in dom F;
then F.j in rng F by FUNCT_1:3;
hence thesis by Def1;
end;
theorem Th17:
the_normal_subgroups_of G c= Subgroups G
proof
let x be object;
assume x in the_normal_subgroups_of G;
then x is strict normal Subgroup of G by Def1;
hence thesis by GROUP_3:def 1;
end;
theorem Th18:
for F being FinSequence of the_normal_subgroups_of G
holds F is FinSequence of Subgroups G
proof
let F be FinSequence of the_normal_subgroups_of G;
the_normal_subgroups_of G c= Subgroups G by Th17;
then rng F c= Subgroups G;
hence thesis by FINSEQ_1:def 4;
end;
definition let IT be Group;
attr IT is nilpotent means :Def2:
ex F being FinSequence of the_normal_subgroups_of IT st
len F > 0 & F.1 = (Omega).IT & F.(len F) = (1).IT &
for i st i in dom F & i+1 in dom F
for G1,G2 being strict normal Subgroup of IT st G1 = F.i & G2 = F.(i+1) holds
G2 is Subgroup of G1 &
G1./.(G1,G2)`*` is Subgroup of center (IT./.G2);
end;
registration
cluster nilpotent strict for Group;
existence
proof
set G = the Group;
take H = (1).G;
thus H is nilpotent
proof
rng <*H*> c= the_normal_subgroups_of H
proof
let x be object;
assume
A1: x in rng<*H*>;
rng <*H*> = { H } by FINSEQ_1:39;
then
x = H by A1,TARSKI:def 1;
then x is strict normal Subgroup of H by GROUP_2:54,GROUP_6:8;
hence thesis by Def1;
end;
then reconsider F = <*H*> as FinSequence of the_normal_subgroups_of H
by FINSEQ_1:def 4;
take F;
A2: len F = 1 by FINSEQ_1:39; then
A3: F.(len F) = H
.= (1).H by GROUP_2:63;
for i st i in dom F & i+1 in dom F for G1,G2
being strict normal Subgroup of H st G1 = F.i & G2 = F.(i+1) holds
G2 is strict Subgroup of G1 &
G1./.(G1,G2)`*` is Subgroup of center (H./.G2)
proof
let i;
assume
A4: i in dom F & i+1 in dom F;
let G1,G2 be strict normal Subgroup of H;
assume G1=F.i & G2=F.(i+1);
dom F={1} by A2,FINSEQ_1:2,def 3;
then i=1 & i+1=1 by A4,TARSKI:def 1;
hence thesis;
end;
hence thesis by A3,FINSEQ_1:40;
end;
thus thesis;
end;
end;
theorem Th19:
for G1 being Subgroup of G,N being strict normal Subgroup of G st
N is Subgroup of G1 & G1./.(G1,N)`*` is Subgroup of center (G./.N) holds
[.G1,(Omega).G.] is Subgroup of N
proof
let G1 be Subgroup of G;
let N be strict normal Subgroup of G;
assume that
A1: N is Subgroup of G1 and
A2: G1./.(G1,N)`*` is Subgroup of center (G./.N);
A3: (G1,N)`*` = N by A1,GROUP_6:def 1;
reconsider J = G1./.(G1,N)`*` as Subgroup of G./.N by A1,GROUP_6:28;
reconsider I = N as normal Subgroup of G1 by A3;
A4: commutators (G1,(Omega).G) c= carr N
proof
now
let x be Element of G;
assume x in commutators (G1,(Omega).G);
then consider a,b such that
A5: x = [.a,b.] & a in G1 & b in (Omega).G by GROUP_5:52;
reconsider c = a as Element of G1 by A5,STRUCT_0:def 5;
reconsider S9 = c * I as Element of J by A3,GROUP_6:22;
A6: S9 in J by STRUCT_0:def 5;
reconsider T = b * N as Element of G./.N
by GROUP_6:14;
reconsider d = c as Element of G;
d * N = c * I by GROUP_6:2;
then reconsider S = S9 as Element of G./.N by GROUP_6:14;
S in center (G./.N) by A2,A6,GROUP_2:40; then
A7: S * T = T * S by GROUP_5:77;
A8: S = d * N & T = b * N & @S = S & @T = T by GROUP_6:2;
then A9: S * T = (d * N) * (b * N) by GROUP_6:def 3
.= d * (N * (b * N)) by GROUP_3:10
.= d * (N * b * N) by GROUP_3:13
.= d * (b * N * N) by GROUP_3:117
.= d * (b * N) by GROUP_6:5
.= d * b * N by GROUP_2:105;
T * S = (b * N) * (d * N) by A8,GROUP_6:def 3
.= b * (N * (d * N)) by GROUP_3:10
.= b * (N * d * N) by GROUP_3:13
.= b * (d * N * N) by GROUP_3:117
.= b * (d * N) by GROUP_6:5
.= b * d * N by GROUP_2:105;
then
A10: (d" * b") * (d * b * N) = ((d" * b") * (b * d)) * N by A7,A9,GROUP_2:105
.= (d" * (b" * (b * d))) * N by GROUP_1:def 3
.= (d" * ((b" * b) * d)) * N by GROUP_1:def 3
.= (d" * (1_G * d)) * N by GROUP_1:def 5
.= (d" * d) * N by GROUP_1:def 4
.= 1_G * N by GROUP_1:def 5
.= carr N by GROUP_2:109;
(d" * b") * (d * b * N) = (d" * b") * (d * b) * N by GROUP_2:105
.= [.d,b.] * N by GROUP_5:16;
then [.d,b.] in N by A10,GROUP_2:113;
hence x in carr N by A5,STRUCT_0:def 5;
end;
hence thesis;
end;
gr carr N = N by GROUP_4:31;
hence thesis by A4,GROUP_4:32;
end;
theorem Th20:
for G1 being Subgroup of G, N being normal Subgroup of G st
N is strict Subgroup of G1 & [.G1,(Omega).G.] is strict Subgroup of N holds
G1./.(G1,N)`*` is Subgroup of center (G./.N)
proof
let G1 be Subgroup of G;
let N be normal Subgroup of G;
assume that
A1: N is strict Subgroup of G1 and
A2: [.G1,(Omega).G.] is strict Subgroup of N;
A3: (G1,N)`*` = N by A1,GROUP_6:def 1;
reconsider J = G1./.(G1,N)`*` as Subgroup of G./.N by A1,GROUP_6:28;
reconsider I = N as normal Subgroup of G1 by A3;
for S1 be Element of G./.N st S1 in J holds S1 in center (G./.N)
proof
let S1 be Element of G./.N;
assume
A4: S1 in J;
for S be Element of G./.N holds S1 * S = S * S1
proof
let S be Element of G./.N;
consider a being Element of G such that
A5: S = a * N & S = N * a by GROUP_6:21;
consider c being Element of G1 such that
A6: S1 = c * I & S1 = I * c by A3,A4,GROUP_6:23;
reconsider d = c as Element of G by GROUP_2:42;
A7: d in G1 by STRUCT_0:def 5;
a in (Omega).G by STRUCT_0:def 5;
then [.d,a.] in [.G1,(Omega).G.] by A7,GROUP_5:65; then
A8: [.d,a.] in N by A2,GROUP_2:40;
A9: @S = S & @S1 = S1 & c * I = d * N & N * d = I * c by GROUP_6:2; then
A10: S * S1 = a * N * (d * N) by A5,A6,GROUP_6:def 3
.= a * d * N by GROUP_11:1;
A11: S1 * S = d * N * (a * N) by A5,A6,A9,GROUP_6:def 3
.= d * a * N by GROUP_11:1;
A12: a * d * [.d,a.] * N = a * d * ([.d,a.] * N) by GROUP_2:32
.= a * d * N by A8,GROUP_2:113;
a * d * [.d,a.] * N = a * d * ((d" * a") * (d * a)) * N by GROUP_1:def 3
.= (a * d * (d" * a")) * (d * a) * N by GROUP_1:def 3
.= (a * (d * (d" * a"))) * (d * a) * N by GROUP_1:def 3
.= (a * (d * d" * a")) * (d * a) * N by GROUP_1:def 3
.= (a * (1_G * a")) * (d * a) * N by GROUP_1:def 5
.= (a * a") * (d * a) * N by GROUP_1:def 4
.= 1_G * (d * a) * N by GROUP_1:def 5
.= d * a * N by GROUP_1:def 4;
hence thesis by A10,A11,A12;
end;
hence thesis by GROUP_5:77;
end;
hence thesis by GROUP_2:58;
end;
theorem Th21:
for G being Group holds G is nilpotent iff
ex F being FinSequence of the_normal_subgroups_of G st len F > 0 &
F.1 = (Omega).G & F.(len F) = (1).G &
for i st i in dom F & i+1 in dom F for G1,G2 being
strict normal Subgroup of G st G1 = F.i & G2 = F.(i+1) holds
G2 is Subgroup of G1 & [.G1, (Omega).G.] is Subgroup of G2
proof
let G be Group;
A1: now assume G is nilpotent;
then consider R being FinSequence of the_normal_subgroups_of G such that
A2: len R > 0 & R.1 = (Omega).G & R.(len R) = (1).G & for i st i in dom R
& i+1 in dom R for H1,H2 being strict normal Subgroup of G st H1 = R.i
& H2 = R.(i+1) holds H2 is Subgroup of H1 &
H1./.(H1,H2)`*` is Subgroup of center (G./.H2);
reconsider F = R as FinSequence of the_normal_subgroups_of G;
A3: for i st i in dom F & i+1 in dom F for G1,G2 being
strict normal Subgroup of G st G1 = F.i & G2 = F.(i+1) holds G2 is strict
Subgroup of G1 & [.G1, (Omega).G.] is strict Subgroup of G2
proof
let i;
assume
A4: i in dom F & i+1 in dom F;
let G1,G2 be strict normal Subgroup of G;
assume
A5: G1 = F.i & G2 = F.(i+1);
then
A6: G2 is strict Subgroup of G1 & for N being strict normal
Subgroup of G st N = G2 & N is strict Subgroup of G1 holds
G1./.(G1,N)`*` is Subgroup of center (G./.N) by A2,A4;
[.G1, (Omega).G.] is strict Subgroup of G2
proof
now
let N be strict normal Subgroup of G;
assume
A7: N = G2 & N is strict Subgroup of G1;
then G1./.(G1,N)`*` is Subgroup of center (G./.N) by A2,A4,A5;
hence [.G1, (Omega).G.] is strict Subgroup of G2 by A7,Th19;
end;
hence thesis by A6;
end;
hence thesis by A2,A4,A5;
end;
take F;
thus len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G &
for i st i in dom F & i+1 in dom F for G1,G2 being
strict normal Subgroup of G st G1 = F.i & G2 = F.(i+1) holds G2 is
Subgroup of G1 & [.G1, (Omega).G.] is Subgroup of G2 by A2,A3;
end;
now
given F being FinSequence of the_normal_subgroups_of G such that
A8: len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G &
for i st i in dom F & i+1 in dom F for G1,G2 being
strict normal Subgroup of G st G1 = F.i & G2 = F.(i+1) holds G2 is
Subgroup of G1 & [.G1, (Omega).G.] is Subgroup of G2;
A9: for i st i in dom F & i+1 in dom F for G1,G2 being strict normal Subgroup
of G st G1 = F.i & G2 = F.(i+1) holds
G2 is strict Subgroup of G1 &
G1./.(G1,G2)`*` is Subgroup of center (G./.G2)
proof
let i;
assume
A10: i in dom F & i+1 in dom F;
let G1,G2 be strict normal Subgroup of G;
assume
A11: G1 = F.i & G2 = F.(i+1);
then A12: G2 is strict Subgroup of G1 by A8,A10;
[.G1, (Omega).G.] is strict Subgroup of G2 by A8,A10,A11;
hence thesis by A12,Th20;
end;
take F;
len F > 0 &
F.1 = (Omega).G & F.(len F) = (1).G & for i st i in dom F & i+1 in dom F
for G1,G2 being strict normal Subgroup of G st
G1 = F.i & G2 = F.(i+1) holds
G2 is Subgroup of G1 &
G1./.(G1,G2)`*` is Subgroup of center (G./.G2) by A8,A9;
hence G is nilpotent;
end;
hence thesis by A1;
end;
theorem Th22:
for G being Group for H,G1 being Subgroup of G
for G2 being strict normal Subgroup of G
for H1 being Subgroup of H
for H2 being normal Subgroup of H
st G2 is Subgroup of G1
& G1./.(G1,G2)`*` is Subgroup of center (G./.G2)
& H1=G1 /\ H & H2=G2 /\ H holds
H1./.(H1,H2)`*` is Subgroup of center (H./.H2)
proof
let G be Group;
let H,G1 be Subgroup of G;
let G2 be strict normal Subgroup of G;
let H1 be Subgroup of H;
let H2 be normal Subgroup of H;
assume that
A1: G2 is Subgroup of G1 and
A2: G1./.(G1,G2)`*` is Subgroup of center (G./.G2) and
A3: H1=G1 /\ H & H2=G2 /\ H;
A4: [.G1, (Omega).G.] is Subgroup of G2 by A1,A2,Th19;
A5: H2 is strict Subgroup of H1 by A1,A3,GROUP_2:92; then
A6: (H1,H2)`*` = H2 by GROUP_6:def 1;
then reconsider I = H2 as normal Subgroup of H1;
reconsider J = H1./.(H1,H2)`*` as Subgroup of H./.H2 by A5,GROUP_6:28;
for T be Element of H./.H2 st T in J holds T in center (H./.H2)
proof
let T be Element of H./.H2;
assume
A7: T in J;
for S be Element of H./.H2 holds S * T = T * S
proof
let S be Element of H./.H2;
consider h being Element of H such that
A8: S = h * H2 & S = H2 * h by GROUP_6:21;
consider h1 being Element of H1 such that
A9: T = h1 * I & T = I * h1 by A6,A7,GROUP_6:23;
reconsider h2 = h1 as Element of H by GROUP_2:42;
A10: @S = S & @T = T & h1 * I = h2 * H2 by GROUP_6:2;
then
A11: S * T = h * H2 * (h2 * H2) by A8,A9,GROUP_6:def 3
.= h * h2 * H2 by GROUP_11:1;
A12: T * S = h2 * H2 * (h * H2) by A8,A9,A10,GROUP_6:def 3
.= h2 * h * H2 by GROUP_11:1;
A13: [.h2,h.] in H by STRUCT_0:def 5;
reconsider a = h as Element of G by GROUP_2:42;
A14: a in (Omega).G by STRUCT_0:def 5;
H1 is Subgroup of G1 by A3,GROUP_2:88;
then reconsider b = h1 as Element of G1 by GROUP_2:42;
reconsider c = b as Element of G by GROUP_2:42;
b in G1 by STRUCT_0:def 5;
then [.c,a.] in [.G1, (Omega).G.] by A14,GROUP_5:65;
then
A15: [.c,a.] in G2 by A4,GROUP_2:40;
A16: a" = h" by GROUP_2:48;
c" = h2" by GROUP_2:48;
then A17: h2" * h" = c" * a" by A16,GROUP_2:43;
h2 * h = c * a by GROUP_2:43;
then
A18: (h2" * h") * (h2 * h) = (c" * a") * (c * a) by A17,GROUP_2:43;
A19: [.h2,h.] = (h2" * h") * (h2 * h) by GROUP_5:16;
[.c,a.] = (c" * a") * (c * a) by GROUP_5:16;
then
[.h2,h.] in H2 by A3,A13,A15,A18,A19,GROUP_2:82;
then h * h2 * H2 = h * h2 * ([.h2,h.] * H2) by GROUP_2:113
.= h * h2 * ((h2" * h") * (h2 * h) * H2) by GROUP_5:16
.= h * h2 * ((h2" * h") * (h2 * h)) * H2 by GROUP_2:32
.= (h * h2 * (h2" * h")) * (h2 * h) * H2 by GROUP_1:def 3
.= (h * (h2 * (h2" * h"))) * (h2 * h) * H2 by GROUP_1:def 3
.= (h * (h2 * h2" * h")) * (h2 * h) * H2 by GROUP_1:def 3
.= (h * (1_H * h")) * (h2 * h) * H2 by GROUP_1:def 5
.= (h * h") * (h2 * h) * H2 by GROUP_1:def 4
.= 1_H * (h2 * h) * H2 by GROUP_1:def 5
.= h2 * h * H2 by GROUP_1:def 4;
hence thesis by A11,A12;
end;
hence thesis by GROUP_5:77;
end;
hence thesis by GROUP_2:58;
end;
Lm4: (Omega).G /\ H = (Omega).H
proof
reconsider G9 = (Omega).G as strict Group;
the carrier of H c= the carrier of G &
the multF of H = (the multF of G) || the carrier of H by GROUP_2:def 5;
then reconsider H9 = (Omega).H as strict Subgroup of G9 by GROUP_2:def 5;
the carrier of H c= the carrier of G &
the multF of H = (the multF of G) || the carrier of H by GROUP_2:def 5;
then
A1: H is Subgroup of (Omega).G by GROUP_2:def 5;
the multMagma of ((Omega).G qua Subgroup of G) /\ H
= the multMagma of H /\ ((Omega).G qua Subgroup of G)
.= multMagma(# the carrier of (H /\ (Omega).G),
the multF of (H /\ (Omega).G) #)
.= multMagma(# the carrier of H, the multF of H #) by A1,GROUP_2:89
.= multMagma(# the carrier of (H9 /\ (Omega).G9),
the multF of (H9 /\ (Omega).G9) #) by GROUP_2:89
.= the multMagma of H9 /\ ((Omega).G9 qua Subgroup of G9)
.= the multMagma of ((Omega).G9 qua Subgroup of G9) /\ H9;
hence thesis by GROUP_2:86;
end;
Lm5: for F1 being strict Subgroup of G for H, F2 being Subgroup of G
st F1 is normal Subgroup of F2 holds F1 /\ H is normal Subgroup of F2 /\ H
proof
let F1 be strict Subgroup of G;
let H,F2 be Subgroup of G;
reconsider F=F2 /\ H as Subgroup of F2 by GROUP_2:88;
assume
A1: F1 is normal Subgroup of F2; then
A2: (F1 /\ H) = ((F1 /\ F2) /\ H) by GROUP_2:89
.= F1 /\ (F2 /\ H) by GROUP_2:84;
reconsider F1 as normal Subgroup of F2 by A1;
F1/\F is normal Subgroup of F;
hence thesis by A2,GROUP_6:3;
end;
registration let G be nilpotent Group;
cluster -> nilpotent for Subgroup of G;
coherence
proof
let H be Subgroup of G;
consider F being FinSequence of the_normal_subgroups_of G such that
A1:len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G and
A2: for i st i in dom F & i+1 in dom F for G1,G2 being strict normal
Subgroup of G st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of
G1 & G1./.(G1,G2)`*` is Subgroup of center (G./.G2) by Def2;
defpred P[set,set] means ex I being strict normal Subgroup of G st I=F.$1 &
$2=I/\H;
A3: for k be Nat st k in Seg len F ex x being Element of
the_normal_subgroups_of H st P[k,x]
proof
let k be Nat;
assume k in Seg len F;
then k in dom F by FINSEQ_1:def 3;
then F.k in the_normal_subgroups_of G by FINSEQ_2:11;
then reconsider I=F.k as strict normal Subgroup of G by Def1;
reconsider x=I /\ H as strict Subgroup of H;
reconsider y=x as Element of the_normal_subgroups_of H by Def1;
take y;
take I;
thus thesis;
end;
consider R being FinSequence of the_normal_subgroups_of H such that
A4: dom R=Seg len F & for i be Nat st i in Seg len F holds P[i,R.i] from
FINSEQ_1:sch 5(A3);
A5: len R=len F by A4,FINSEQ_1:def 3;
A6: len R >0 by A1,A4,FINSEQ_1:def 3;
A7: R.1=(Omega).H
proof
1<=len R by A6,NAT_1:14;
then 1 in Seg len F by A5;
then ex I being strict normal Subgroup of G st I=F.1 & R.1=I /\ H by A4;
hence R.1 = (Omega).H by A1,Lm4;
end;
A8:R.(len R)= (1).H
proof
ex I being strict normal Subgroup of G st I=F.(len R) & R.(len R )=I /\ H
by A1,A4,A5,FINSEQ_1:3;
hence R.(len R)=(1).G by A1,A5,GROUP_2:85
.=(1).H by GROUP_2:63;
end;
A9: for i st i in dom R & i+1 in dom R for H1,H2 being strict normal Subgroup
of H st H1=R.i & H2=R.(i+1) holds H2 is Subgroup of H1 &
H1./.(H1,H2)`*` is Subgroup of center (H./.H2)
proof
let i;
assume
A10: i in dom R & i+1 in dom R;
let H1,H2 be strict normal Subgroup of H;
assume
A11: H1 = R.i & H2 = R.(i+1);
consider I being strict normal Subgroup of G such that
A12: I = F.i & R.i = I /\ H by A4,A10;
consider J being strict normal Subgroup of G such that
A13: J = F.(i+1) & R.(i+1) = J /\ H by A4,A10;
A14: i in dom F & i+1 in dom F by A4,A10,FINSEQ_1:def 3;
then
A15: J is strict normal Subgroup of I by A12,A13,A2,GROUP_6:8;
I./.(I,J)`*` is Subgroup of center (G./.J) by A14,A12,A13,A2;
hence thesis by A13,A15,A12,A11,Th22,Lm5;
end;
take R;
thus thesis by A1,A4,A7,A8,A9,FINSEQ_1:def 3;
end;
end;
registration
cluster commutative -> nilpotent for Group;
correctness
proof
let G be Group;
assume
A1: G is commutative;
(Omega).G in the_normal_subgroups_of G &
(1).G in the_normal_subgroups_of G by Def1;
then <*(Omega).G,(1).G*>is FinSequence of the_normal_subgroups_of G
by FINSEQ_2:13;
then consider F being FinSequence of the_normal_subgroups_of G such that
A2: F = <*(Omega).G,(1).G*>;
A3: len F = 2 & F.1 = (Omega).G & F.2 = (1).G by A2,FINSEQ_1:44;
for i st i in dom F & i+1 in dom F
for G1,G2 being strict normal Subgroup of G
st G1 = F.i & G2 = F.(i+1) holds
G2 is Subgroup of G1 & [.G1,(Omega).G.] is Subgroup of G2
proof
let i;
assume
A4: i in dom F & i+1 in dom F;
now
let G1,G2 be Subgroup of G;
assume
A5: G1 = F.i & G2 = F.(i+1);
A6: dom F={1,2} by A3,FINSEQ_1:2,def 3;
A7: i in {1,2} & i+1 in {1,2} by A3,A4,FINSEQ_1:2,def 3;
A8: i = 1 or i = 2 by A4,A6,TARSKI:def 2;
commutators(G1,(Omega).G) = {1_G} by A1,GROUP_5:57; then
A9: [.G1,(Omega).G.] = gr ({1_G} \ {1_G}) by GROUP_4:35
.= gr {} the carrier of G by XBOOLE_1:37
.= (1).G by GROUP_4:30;
G1 = (Omega).G & G2 = (1).G by A2,A5,A7,A8,TARSKI:def 2;
hence thesis by A5,A9,GROUP_2:65;
end;
hence thesis;
end;
hence thesis by A3,Th21;
end;
cluster cyclic -> nilpotent for Group;
coherence;
end;
theorem Th23:
for G,H being strict Group, h being Homomorphism of G,H for A
being strict Subgroup of G for a,b being Element of G
holds h.a * h.b * h.:A = h.:(a * b * A) & h.:A * h.a * h.b = h.:(A * a * b)
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let A be strict Subgroup of G;
let a,b be Element of G;
thus h.a * h.b * h.:A = h. (a * b) * h.:A by GROUP_6:def 6
.= h.:(a * b * A) by GRSOLV_1:13;
thus h.:A * h.a * h.b = h.:A * (h.a * h.b) by GROUP_2:107
.= h.:A * h. (a * b) by GROUP_6:def 6
.= h.:(A * (a * b)) by GRSOLV_1:13
.= h.:(A * a * b) by GROUP_2:107;
end;
theorem Th24:
for G,H being strict Group, h being Homomorphism of G,H
for A being strict Subgroup of G for a,b being Element of G
for H1 being Subgroup of Image h for a1,b1 being Element of Image h
st a1 = h.a & b1 = h.b & H1 = h.:A holds a1 * b1 * H1 = h.a * h.b * h.:A
proof
let G,H be strict Group;
let h being Homomorphism of G,H;
let A be strict Subgroup of G;
let a,b be Element of G;
let H1 be Subgroup of Image h;
let a1,b1 be Element of Image h;
assume that
A1: a1 = h.a and
A2: b1 = h.b and
A3: H1 = h.:A;
A4: a1 * b1 = h.a * h.b by A1,A2,GROUP_2:43;
set c1 = a1 * b1;
set c = a * b;
A5: h.c = h.a * h.b by GROUP_6:def 6;
A6: h.:(c * A) = h.c * h.:A by GRSOLV_1:13;
c1 * H1 = h.c * h.:A
proof
now
let x be object;
assume x in c1 * H1;
then consider Z being Element of Image h such that
A7: x = c1 * Z and
A8: Z in H1 by GROUP_2:103;
consider Z1 being Element of A such that
A9: Z = (h|A).Z1 by A3,A8,GROUP_6:45;
A10: Z1 in A by STRUCT_0:def 5;
reconsider Z1 as Element of G by GROUP_2:42;
Z = h.Z1 by A9,FUNCT_1:49;
then
A11: x = h.c * h.Z1 by A4,A5,A7,GROUP_2:43
.= h.(c * Z1) by GROUP_6:def 6;
c * Z1 in c * A by A10,GROUP_2:103;
hence x in h.c * h.:A by A11,A6,FUNCT_2:35;
end;
then
A12: c1 * H1 c= h.c * h.:A;
now
let x be object;
assume x in h.c * h.:A;
then consider y being object such that
A13: y in the carrier of G and
A14: y in c * A and
A15: x = h.y by A6,FUNCT_2:64;
reconsider y as Element of G by A13;
consider Z being Element of G such that
A16: y= c * Z and
A17: Z in A by A14,GROUP_2:103;
Z in the carrier of A by A17,STRUCT_0:def 5;
then h.Z in h.:(the carrier of A) by FUNCT_2:35;
then h.Z in the carrier of h.: A by GRSOLV_1:8;
then
A18: h.Z in H1 by A3,STRUCT_0:def 5;
then h.Z in Image h by GROUP_2:40;
then reconsider Z1 = h.Z as Element of Image h by STRUCT_0:def 5;
x = h.c * h.Z by A15,A16,GROUP_6:def 6;
then x = c1 * Z1 by A4,A5,GROUP_2:43;
hence x in c1 * H1 by A18,GROUP_2:103;
end;
then h.c * h.:A c= c1 * H1;
hence thesis by A12,XBOOLE_0:def 10;
end;
hence thesis by GROUP_6:def 6;
end;
theorem Th25:
for G,H being strict Group,h being Homomorphism of G,H
for G1 being strict Subgroup of G
for G2 being strict normal Subgroup of G
for H1 being strict Subgroup of Image h
for H2 being strict normal Subgroup of Image h
st G2 is strict Subgroup of G1 &
G1./.(G1,G2)`*` is Subgroup of center (G./.G2)
& H1=h.:G1 & H2=h.:G2 holds
H1./.(H1,H2)`*` is Subgroup of center (Image h./.H2)
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let G1 be strict Subgroup of G;
let G2 be strict normal Subgroup of G;
let H1 be strict Subgroup of Image h;
let H2 be strict normal Subgroup of Image h;
assume that
A1: G2 is strict Subgroup of G1 and
A2: G1./.(G1,G2)`*` is Subgroup of center (G./.G2) and
A3: H1=h.:G1 & H2=h.:G2;
A4: H2 is strict Subgroup of H1 by A1,A3,GRSOLV_1:12; then
A5: (H1,H2)`*` = H2 by GROUP_6:def 1;
then reconsider I = H2 as normal Subgroup of H1;
reconsider J = H1./.(H1,H2)`*` as Subgroup of Image h./.H2 by A4,GROUP_6:28;
for T be Element of Image h./.H2 st T in J holds T in center (Image h./.H2)
proof
let T be Element of Image h./.H2;
assume
A6: T in J;
for S be Element of Image h./.H2 holds S * T = T * S
proof
let S be Element of Image h./.H2;
consider g being Element of Image h such that
A7: S = g * H2 & S = H2 * g by GROUP_6:21;
consider h1 being Element of H1 such that
A8: T = h1 * I & T = I * h1 by A5,A6,GROUP_6:23;
reconsider h2 = h1 as Element of Image h by GROUP_2:42;
A9: @S = S & @T = T & h1 * I = h2 * H2 by GROUP_6:2;
then
A10: S * T = g * H2 * (h2 * H2) by A7,A8,GROUP_6:def 3
.= g * h2 * H2 by GROUP_11:1;
A11: T * S = h2 * H2 * (g * H2) by A7,A8,A9,GROUP_6:def 3
.= h2 * g * H2 by GROUP_11:1;
g in Image h by STRUCT_0:def 5;
then consider a being Element of G such that
A12: g = h.a by GROUP_6:45;
A13: a in (Omega).G by STRUCT_0:def 5;
h1 in H1 by STRUCT_0:def 5;
then consider a1 being Element of G1 such that
A14: h1 = (h|G1).a1 by A3,GROUP_6:45;
A15: a1 in G1 by STRUCT_0:def 5;
reconsider a2 = a1 as Element of G by GROUP_2:42;
A16: h2 = h.a2 by A14,FUNCT_1:49;
then A17: g * h2 * H2 = h.a * h.a2 * h.:G2 by A12,A3,Th24
.= h.:(a * a2 * G2) by Th23;
A18: h2 * g * H2 = h.a2 * h.a * h.:G2 by A12,A16,A3,Th24
.= h.:(a2 * a * G2) by Th23;
A19: [.G1, (Omega).G.] is strict Subgroup of G2 by A1,A2,Th19;
[.a2,a.] in [.G1, (Omega).G.] by A13,A15,GROUP_5:65; then
[.a2,a.] in G2 by A19,GROUP_2:40;
then a * a2 * G2= a * a2 * ([.a2,a.] * G2) by GROUP_2:113
.= a * a2 * ((a2" * a") * (a2 * a) * G2) by GROUP_5:16
.= a * a2 * ((a2" * a") * (a2 * a)) * G2 by GROUP_2:32
.= (a * a2 * (a2" * a")) * (a2 * a) * G2 by GROUP_1:def 3
.= (a * (a2 * (a2" * a"))) * (a2 * a) * G2 by GROUP_1:def 3
.= (a * (a2 * a2" * a")) * (a2 * a) * G2 by GROUP_1:def 3
.= (a * (1_G * a")) * (a2 * a) * G2 by GROUP_1:def 5
.= (a * a") * (a2 * a) * G2 by GROUP_1:def 4
.= 1_G * (a2 * a) * G2 by GROUP_1:def 5
.= a2 * a * G2 by GROUP_1:def 4;
hence thesis by A10,A11,A17,A18;
end;
hence thesis by GROUP_5:77;
end;
hence thesis by GROUP_2:58;
end;
theorem Th26:
for G,H being strict Group, h being Homomorphism of G,H holds
for A being strict normal Subgroup of G holds
h.:A is strict normal Subgroup of Image h
proof
let G,H be strict Group;
let h be Homomorphism of G,H;
let A be strict normal Subgroup of G;
reconsider C=h.:A as strict Subgroup of Image h by GRSOLV_1:9;
for b being Element of Image h holds b* C c= C * b
proof
let b be Element of Image h;
A1: b in Image h by STRUCT_0:def 5;
now
consider b1 being Element of G such that
A2: b = h.b1 by A1,GROUP_6:45;
let x be object;
assume x in b * C;
then consider g being Element of Image h such that
A3: x = b * g and
A4: g in C by GROUP_2:103;
consider g1 being Element of A such that
A5: g=(h|A).g1 by A4,GROUP_6:45;
reconsider g1 as Element of G by GROUP_2:42;
g=h.g1 by A5,FUNCT_1:49;
then
A6: x =h.b1 * h.g1 by A2,A3,GROUP_2:43
.=h.(b1 *g1) by GROUP_6:def 6;
g1 in A by STRUCT_0:def 5; then
A7: b1 * g1 in b1 * A by GROUP_2:103;
A8: h.:(A * b1) = h.:A * h.b1 by GRSOLV_1:13;
b1 * A = A * b1 by GROUP_3:117;
then x in h.:A * h.b1 by A6,A7,A8,FUNCT_2:35;
hence x in C * b by A2,GROUP_6:2;
end;
hence thesis;
end;
hence thesis by GROUP_3:118;
end;
registration
let G be strict nilpotent Group, H be strict Group,
h be Homomorphism of G,H;
cluster Image h -> nilpotent;
coherence
proof
consider F being FinSequence of the_normal_subgroups_of G such that
A1: len F>0 and
A2: F.1 = (Omega).G and
A3: F.(len F) = (1).G and
A4: for i st i in dom F & i+1 in dom F for G1,G2 being strict normal Subgroup
of G st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of G1 &
G1./.(G1,G2)`*` is Subgroup of center (G./.G2) by Def2;
1 <= len F by A1,NAT_1:14;
then
A5: 1 in Seg len F;
defpred P[set,set] means ex J being strict normal Subgroup of G st J = F.$1
& $2 = h.:(J);
A6: for k be Nat st k in Seg len F ex x being Element of
the_normal_subgroups_of Image h st P[k,x]
proof
let k be Nat;
assume k in Seg len F;
then k in dom F by FINSEQ_1:def 3;
then F.k in the_normal_subgroups_of G by FINSEQ_2:11;
then F.k is strict normal Subgroup of G by Def1;
then consider A being strict normal Subgroup of G such that
A7: A=F.k;
h.:(A) is strict normal Subgroup of Image h by Th26;
then h.:(A) in the_normal_subgroups_of Image h by Def1;
hence thesis by A7;
end;
consider Z being FinSequence of the_normal_subgroups_of Image h such that
A8: dom Z = Seg len F & for j be Nat st j in Seg len F holds P[j,Z.j]
from FINSEQ_1:sch 5(A6);
Seg len Z = Seg len F by A8,FINSEQ_1:def 3;
then
A9: dom F = Seg len Z by FINSEQ_1:def 3
.= dom Z by FINSEQ_1:def 3;
A10: for i st i in dom Z & i+1 in dom Z for H1,H2 being strict normal Subgroup
of Image h st H1 = Z.i & H2 = Z.(i+1) holds H2 is strict Subgroup of H1 &
H1./.(H1,H2)`*` is Subgroup of center (Image h./.H2)
proof
let i;
assume
A11: i in dom Z & i+1 in dom Z;
let H1,H2 be strict normal Subgroup of Image h;
assume that
A12: H1=Z.i and
A13: H2=Z.(i+1);
A14:i in dom F & i+1 in dom F by A8,A11,FINSEQ_1:def 3;
consider G1 being strict normal Subgroup of G such that
A15: G1 = F.i and
A16: H1 = h.:G1 by A8,A11,A12;
consider G2 being strict normal Subgroup of G such that
A17: G2 = F.(i+1) and
A18: H2 = h.:G2 by A8,A11,A13;
A19: G2 is strict Subgroup of G1 by A4,A9,A11,A15,A17;
G1./.(G1,G2)`*` is Subgroup of center (G./.G2) by A14,A15,A17,A4;
hence thesis by A16,A19,A18,Th25,GRSOLV_1:12;
end;
take Z;
A20: len Z = len F by A8,FINSEQ_1:def 3;
Z.1 = (Omega).(Image h) & Z.(len Z) = (1).(Image h)
proof
ex G1 being strict normal Subgroup of G st G1 = F.1 & Z.1 = h.:G1 by A8,A5;
hence Z.1 = (Omega).(Image h) by A2,GRSOLV_1:11;
ex G2 being strict normal Subgroup of G st G2 = F.(len F) &
Z.(len F ) = h.:G2 by A1,A8,FINSEQ_1:3;
hence Z.(len Z) = (1).H by A3,A20,GRSOLV_1:11
.= (1).(Image h) by GROUP_2:63;
end;
hence thesis by A1,A8,A10,FINSEQ_1:def 3;
end;
end;
registration
let G be strict nilpotent Group, N be strict normal Subgroup of G;
cluster G./.N -> nilpotent;
coherence
proof
Image nat_hom N = G./.N by GROUP_6:48;
hence thesis;
end;
end;
theorem
for G being Group st ex F being FinSequence of the_normal_subgroups_of G st
len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G & for i st i in dom F
& i+1 in dom F for G1 being strict normal Subgroup of G st G1 = F.i
holds [.G1, (Omega).G.] = F.(i+1) holds G is nilpotent
proof
let G be Group;
given F being FinSequence of the_normal_subgroups_of G such that
A1: len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G and
A2: for i st i in dom F & i+1 in dom F for G1 being strict normal
Subgroup of G st G1 = F.i holds [.G1, (Omega).G.] = F.(i+1);
for i st i in dom F & i+1 in dom F for H1,H2 being
strict normal Subgroup of G st H1 = F.i & H2 = F.(i+1) holds H2 is
Subgroup of H1 & [.H1, (Omega).G.] is Subgroup of H2
proof
let i;
assume
A3: i in dom F & i+1 in dom F;
let H1,H2 be strict normal Subgroup of G;
assume H1 = F.i & H2 = F.(i+1);
then H2 = [.H1, (Omega).G.] by A2,A3;
hence thesis by Th15,GROUP_2:54;
end;
hence thesis by A1,Th21;
end;
theorem
for G being Group st ex F being FinSequence of the_normal_subgroups_of G
st len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G & for i st i in dom F
& i+1 in dom F for G1,G2 being strict normal Subgroup of G
st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of G1 &
G./.G2 is commutative Group holds G is nilpotent
proof
let G be Group;
given F being FinSequence of the_normal_subgroups_of G such that
A1: len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G and
A2: for i st i in dom F & i+1 in dom F for G1,G2 being strict normal Subgroup
of G st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of G1 &
G./.G2 is commutative Group;
A3: for i st i in dom F & i+1 in dom F for H1,H2 being
strict normal Subgroup of G st H1 = F.i & H2 = F.(i+1) holds H2 is
Subgroup of H1 & H1./.(H1,H2)`*` is Subgroup of center (G./.H2)
proof
let i;
assume
A4: i in dom F & i+1 in dom F;
let H1,H2 be strict normal Subgroup of G;
assume
A5: H1 = F.i & H2 = F.(i+1);
then H2 is Subgroup of H1 by A2,A4;
then
A6: H1./.(H1,H2)`*` is Subgroup of G./.H2 by GROUP_6:28;
G./.H2 is commutative Group by A2,A4,A5;
hence thesis by A2,A4,A5,A6,GROUP_5:82;
end;
take F;
thus thesis by A1,A3;
end;
theorem
for G being Group st ex F being FinSequence of the_normal_subgroups_of
G st len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G & for i st i in dom F
& i+1 in dom F for G1,G2 being strict normal Subgroup of G
st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of G1 &
G./.G2 is cyclic Group holds G is nilpotent
proof
let G be Group;
given F being FinSequence of the_normal_subgroups_of G such that
A1: len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G and
A2: for i st i in dom F & i+1 in dom F for G1,G2 being strict normal Subgroup
of G st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of G1 &
G./.G2 is cyclic Group;
A3: for i st i in dom F & i+1 in dom F for H1,H2 being
strict normal Subgroup of G st H1 = F.i & H2 = F.(i+1) holds H2 is strict
Subgroup of H1 & H1./.(H1,H2)`*` is Subgroup of center (G./.H2)
proof
let i;
assume
A4: i in dom F & i+1 in dom F;
let H1,H2 be strict normal Subgroup of G;
assume
A5: H1 = F.i & H2 = F.(i+1);
then H2 is strict Subgroup of H1 by A2,A4; then
A6: H1./.(H1,H2)`*` is Subgroup of G./.H2 by GROUP_6:28;
G./.H2 is commutative Group by A2,A4,A5;
hence thesis by A2,A4,A5,A6,GROUP_5:82;
end;
take F;
thus thesis by A1,A3;
end;
registration
cluster nilpotent -> solvable for Group;
correctness
proof
let G be Group;
assume G is nilpotent;
then consider F being FinSequence of the_normal_subgroups_of G such that
A1: len F > 0 & F.1 = (Omega).G & F.(len F) = (1).G &
for i st i in dom F & i+1 in dom F for G1,G2 being strict normal
Subgroup of G st G1 = F.i & G2 = F.(i+1) holds G2 is Subgroup of
G1 & G1./.(G1,G2)`*` is Subgroup of center (G./.G2);
reconsider R = F as FinSequence of Subgroups G by Th18;
A2: for i st i in dom R & i+1 in dom R for H1,H2 being Subgroup
of G st H1 = R.i & H2 = R.(i+1) holds H2 is strict normal Subgroup of H1
& for N being normal Subgroup of H1 st N = H2 holds H1./.N is commutative
proof
let i;
assume
A3: i in dom R & i+1 in dom R;
then A4: F.i is strict normal Subgroup of G &
F.(i+1) is strict normal Subgroup of G by Th16;
let H1,H2 be Subgroup of G;
assume
A5: H1 = R.i & H2 = R.(i+1);
for N being normal Subgroup of H1 st N = H2 holds H1./.N is commutative
proof
let N be normal Subgroup of H1;
assume
A6: N = H2;
then reconsider N9 = N as strict normal Subgroup of G by A5,A4;
A7: H1./.(H1,N9)`*` is Subgroup of center (G./.N9) by A1,A3,A5,A6,A4;
center (G./.N9) is commutative by GROUP_5:80;
hence H1./.N is commutative by A7,GROUP_6:def 1;
end;
hence thesis by A1,A3,A5,A4,GROUP_6:8;
end;
take R;
thus thesis by A1,A2;
end;
end;