:: 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 b₁ being set st
for x being object holds
( x in b₁ iff x is strict normal Subgroup of G )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff x is strict normal Subgroup of G ) ) & ( for x being object holds
( x in b₂ iff x is strict normal Subgroup of G ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines the_normal_subgroups_of GRNILP_1:def 1 :
for G being Group
for b₂ being set holds
( b₂ = the_normal_subgroups_of G iff for x being object holds
( x in b₂ 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 b₁ being Group st
( b₁ is nilpotent & b₁ 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 b₁ being Subgroup of G holds b₁ is nilpotent

proof end;

end;

registration

cluster non empty Group-like associative commutative -> nilpotent for multMagma ;

correctness
coherence
for b₁ being Group st b₁ is commutative holds
b₁ is nilpotent ;

proof end;

cluster non empty Group-like associative cyclic -> nilpotent for multMagma ;

coherence
for b₁ being Group st b₁ is cyclic holds
b₁ 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 b₁ being Group st b₁ is nilpotent holds
b₁ is solvable ;

proof end;

end;