:: Nilpotent Groups :: by Dailu Li , Xiquan Liang and Yanhong Men :: :: Received November 10, 2009 :: Copyright (c) 2009-2021 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;