:: Nilpotent Groups
:: by Dailu Li , Xiquan Liang and Yanhong Men
::
:: Received November 10, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users


theorem :: GRNILP_1:1
for G being Group
for a, b being Element of G holds a |^ b = a * [.a,b.]
proof end;

theorem :: GRNILP_1:2
for G being Group
for a, b being Element of G holds [.a,b.] " = [.a,(b ").] |^ b
proof end;

theorem :: GRNILP_1:3
for G being Group
for a, b being Element of G holds [.a,b.] " = [.(a "),b.] |^ a
proof end;

theorem Th4: :: GRNILP_1:4
for G being Group
for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b
proof end;

theorem Th5: :: GRNILP_1:5
for G being Group
for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).]
proof end;

theorem Th6: :: GRNILP_1:6
for G being Group
for a, b being Element of G holds [.a,(b ").] |^ b = [.b,a.]
proof end;

theorem Th7: :: GRNILP_1:7
for G being Group
for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.b,a,(c |^ b).]
proof end;

theorem :: GRNILP_1:8
for G being Group
for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G
proof end;

theorem Th9: :: GRNILP_1:9
for G being Group
for A, B being Subgroup of G holds [.A,B.] is Subgroup of [.B,A.]
proof end;

definition
let G be Group;
let A, B be Subgroup of G;
:: original: [.
redefine func [.A,B.] -> Subgroup of G;
commutativity
for A, B being Subgroup of G holds [.A,B.] = [.B,A.]
proof end;
end;

theorem Th10: :: GRNILP_1:10
for G being Group
for A, B being Subgroup of G st B is Subgroup of A holds
commutators (A,B) c= carr A
proof end;

Lm1: for G being Group
for A being Subgroup of G holds gr (carr A) is Subgroup of A

proof end;

theorem Th11: :: GRNILP_1:11
for G being Group
for A, B being Subgroup of G st B is Subgroup of A holds
[.A,B.] is Subgroup of A
proof end;

theorem :: GRNILP_1:12
for G being Group
for A, B being Subgroup of G st B is Subgroup of A holds
[.B,A.] is Subgroup of A by Th11;

Lm2: for G being Group
for A being Subgroup of G holds A is Subgroup of (Omega). G

proof end;

theorem :: GRNILP_1:13
for G being Group
for H, H1, H2 being Subgroup of G st [.H1,((Omega). G).] is Subgroup of H2 holds
[.(H1 /\ H),H.] is Subgroup of H2 /\ H
proof end;

theorem :: GRNILP_1:14
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] is Subgroup of [.H1,((Omega). G).]
proof end;

Lm3: for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds [.N,H.] is Subgroup of N

proof end;

theorem Th15: :: GRNILP_1:15
for G being Group
for A being Subgroup of G holds
( A is normal Subgroup of G iff [.A,((Omega). G).] is Subgroup of A )
proof end;

definition
let G be Group;
func the_normal_subgroups_of G -> set means :Def1: :: GRNILP_1:def 1
for x being object holds
( x in it iff x is strict normal Subgroup of G );
existence
ex b1 being set st
for x being object holds
( x in b1 iff x is strict normal Subgroup of G )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff x is strict normal Subgroup of G ) ) & ( for x being object holds
( x in b2 iff x is strict normal Subgroup of G ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines the_normal_subgroups_of GRNILP_1:def 1 :
for G being Group
for b2 being set holds
( b2 = the_normal_subgroups_of G iff for x being object holds
( x in b2 iff x is strict normal Subgroup of G ) );

registration
let G be Group;
cluster the_normal_subgroups_of G -> non empty ;
coherence
not the_normal_subgroups_of G is empty
proof end;
end;

theorem Th16: :: GRNILP_1:16
for G being Group
for F being FinSequence of the_normal_subgroups_of G
for j being Element of NAT st j in dom F holds
F . j is strict normal Subgroup of G
proof end;

theorem Th17: :: GRNILP_1:17
for G being Group holds the_normal_subgroups_of G c= Subgroups G
proof end;

theorem Th18: :: GRNILP_1:18
for G being Group
for F being FinSequence of the_normal_subgroups_of G holds F is FinSequence of Subgroups G
proof end;

definition
let IT be Group;
attr IT is nilpotent means :Def2: :: GRNILP_1:def 2
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 being Element of NAT st i in dom F & i + 1 in dom F holds
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;

:: deftheorem Def2 defines nilpotent GRNILP_1:def 2 :
for IT being Group holds
( IT is nilpotent iff 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 being Element of NAT st i in dom F & i + 1 in dom F holds
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) ) ) ) );

registration
cluster non empty strict unital Group-like associative nilpotent for multMagma ;
existence
ex b1 being Group st
( b1 is nilpotent & b1 is strict )
proof end;
end;

theorem Th19: :: GRNILP_1:19
for G being Group
for G1 being Subgroup of G
for 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 end;

theorem Th20: :: GRNILP_1:20
for G being Group
for G1 being Subgroup of G
for 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 end;

theorem Th21: :: GRNILP_1:21
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 being Element of NAT st i in dom F & i + 1 in dom F holds
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 end;

theorem Th22: :: GRNILP_1:22
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 end;

Lm4: for G being Group
for H being Subgroup of G holds ((Omega). G) /\ H = (Omega). H

proof end;

Lm5: for G being Group
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 end;

registration
let G be nilpotent Group;
cluster -> nilpotent for Subgroup of G;
coherence
for b1 being Subgroup of G holds b1 is nilpotent
proof end;
end;

registration
cluster non empty Group-like associative commutative -> nilpotent for multMagma ;
correctness
coherence
for b1 being Group st b1 is commutative holds
b1 is nilpotent
;
proof end;
cluster non empty Group-like associative cyclic -> nilpotent for multMagma ;
coherence
for b1 being Group st b1 is cyclic holds
b1 is nilpotent
;
end;

theorem Th23: :: GRNILP_1:23
for G, H being strict Group
for 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 end;

theorem Th24: :: GRNILP_1:24
for G, H being strict Group
for 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 end;

theorem Th25: :: GRNILP_1:25
for G, H being strict Group
for 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 end;

theorem Th26: :: GRNILP_1:26
for G, H being strict Group
for h being Homomorphism of G,H
for A being strict normal Subgroup of G holds h .: A is strict normal Subgroup of Image h
proof end;

registration
let G be strict nilpotent Group;
let H be strict Group;
let h be Homomorphism of G,H;
cluster Image h -> nilpotent ;
coherence
Image h is nilpotent
proof end;
end;

registration
let G be strict nilpotent Group;
let N be strict normal Subgroup of G;
cluster G ./. N -> nilpotent ;
coherence
G ./. N is nilpotent
proof end;
end;

theorem :: GRNILP_1:27
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 being Element of NAT st i in dom F & i + 1 in dom F holds
for G1 being strict normal Subgroup of G st G1 = F . i holds
[.G1,((Omega). G).] = F . (i + 1) ) ) holds
G is nilpotent
proof end;

theorem :: GRNILP_1:28
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 being Element of NAT st i in dom F & i + 1 in dom F holds
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 end;

theorem :: GRNILP_1:29
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 being Element of NAT st i in dom F & i + 1 in dom F holds
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 end;

registration
cluster non empty Group-like associative nilpotent -> solvable for multMagma ;
correctness
coherence
for b1 being Group st b1 is nilpotent holds
b1 is solvable
;
proof end;
end;