:: Nilpotent Groups
:: by Dailu Li , Xiquan Liang and Yanhong Men
::
:: Received November 10, 2009
:: Copyright (c) 2009-2016 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;
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 :: GRNILP_1:1
a |^ b = a * [.a,b.];
theorem :: GRNILP_1:2
[.a,b.]" = [.a,b".]|^b;
theorem :: GRNILP_1:3
[.a,b.]" = [.a",b.]|^a;
theorem :: GRNILP_1:4
([.a,b".]|^ b)" = [.b",a.]|^ b;
theorem :: GRNILP_1:5
[.a,b",c.] |^ b = [.[.a,b".]|^ b,c|^ b.];
theorem :: GRNILP_1:6
[.a,b".]|^ b = [.b,a.];
theorem :: GRNILP_1:7
[.a,b",c.] |^ b = [.b,a,c|^ b.];
theorem :: GRNILP_1:8
[.a,b,c|^ a.] * [.c,a,b|^ c.] * [.b,c,a|^ b.] = 1_G;
theorem :: GRNILP_1:9
[.A,B.] is Subgroup of [.B,A.];
definition let G,A,B;
redefine func [.A,B.];
commutativity;
end;
theorem :: GRNILP_1:10
B is Subgroup of A implies commutators(A,B) c= carr A;
theorem :: GRNILP_1:11
B is Subgroup of A implies [.A,B.] is Subgroup of A;
theorem :: GRNILP_1:12
B is Subgroup of A implies [.B,A.] is Subgroup of A;
theorem :: GRNILP_1:13
[.H1, (Omega).G.] is Subgroup of H2
implies [.H1 /\ H,H.] is Subgroup of H2 /\ H;
theorem :: GRNILP_1:14
[.H1,H2.] is Subgroup of [.H1,(Omega).G.];
theorem :: GRNILP_1:15
A is normal Subgroup of G iff [.A,(Omega).G.] is Subgroup of A;
definition let G;
func the_normal_subgroups_of G -> set means
:: GRNILP_1:def 1
for x being object holds x in it iff x is strict normal Subgroup of G;
end;
registration let G;
cluster the_normal_subgroups_of G -> non empty;
end;
theorem :: GRNILP_1:16
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;
theorem :: GRNILP_1:17
the_normal_subgroups_of G c= Subgroups G;
theorem :: GRNILP_1:18
for F being FinSequence of the_normal_subgroups_of G
holds F is FinSequence of Subgroups G;
definition let IT be Group;
attr IT is nilpotent means
:: 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 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;
end;
theorem :: GRNILP_1:19
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;
theorem :: GRNILP_1:20
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);
theorem :: 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 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;
theorem :: 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);
registration let G be nilpotent Group;
cluster -> nilpotent for Subgroup of G;
end;
registration
cluster commutative -> nilpotent for Group;
cluster cyclic -> nilpotent for Group;
end;
theorem :: GRNILP_1:23
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);
theorem :: GRNILP_1:24
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;
theorem :: GRNILP_1:25
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);
theorem :: GRNILP_1:26
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;
registration
let G be strict nilpotent Group, H be strict Group,
h be Homomorphism of G,H;
cluster Image h -> nilpotent;
end;
registration
let G be strict nilpotent Group, N be strict normal Subgroup of G;
cluster G./.N -> nilpotent;
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 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;
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 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;
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 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;
registration
cluster nilpotent -> solvable for Group;
end;