:: Commutator and Center of a Group :: by Wojciech A. Trybulec :: :: Received May 15, 1991 :: Copyright (c) 1991-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 XBOOLE_0, SUBSET_1, TARSKI, NUMBERS, INT_1, GROUP_1, GROUP_2, PRE_TOPC, FINSEQ_1, STRUCT_0, NEWTON, RELAT_1, EQREL_1, BINOP_1, NAT_1, FUNCT_1, PARTFUN1, ORDINAL4, ARYTM_3, CARD_1, CARD_3, QC_LANG1, XXREAL_1, ARYTM_1, GROUP_4, RLSUB_1, FINSET_1, CQC_SIM1, GROUP_3, GROUP_5; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, PARTFUN1, CARD_1, FINSEQ_1, FINSET_1, FINSEQ_4, INT_1, DOMAIN_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4; constructors PARTFUN1, SETFAM_1, NAT_1, FINSEQ_4, FINSOP_1, REALSET1, GROUP_4, RELSET_1, BINOP_2; registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, INT_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, ORDINAL1, FINSEQ_1, CARD_1; requirements NUMERALS, BOOLE, SUBSET; begin :: Preliminaries. reserve x,y for set, k,n for Nat, i for Integer, G for Group, a,b,c ,d,e for Element of G, A,B,C,D for Subset of G, H,H1,H2,H3,H4 for Subgroup of G , N1,N2 for normal Subgroup of G, F,F1,F2 for FinSequence of the carrier of G, I,I1,I2 for FinSequence of INT; theorem :: GROUP_5:1 x in (1).G iff x = 1_G; theorem :: GROUP_5:2 a in H & b in H implies a |^ b in H; theorem :: GROUP_5:3 for N being strict normal Subgroup of G holds a in N implies a |^ b in N; theorem :: GROUP_5:4 x in H1 * H2 iff ex a,b st x = a * b & a in H1 & b in H2; theorem :: GROUP_5:5 H1 * H2 = H2 * H1 implies (x in H1 "\/" H2 iff ex a,b st x = a * b & a in H1 & b in H2); theorem :: GROUP_5:6 G is commutative Group implies (x in H1 "\/" H2 iff ex a,b st x = a * b & a in H1 & b in H2); theorem :: GROUP_5:7 for N1,N2 being strict normal Subgroup of G holds x in N1 "\/" N2 iff ex a,b st x = a * b & a in N1 & b in N2; theorem :: GROUP_5:8 for N being normal Subgroup of G holds H * N = N * H; definition let G,F,a; func F |^ a -> FinSequence of the carrier of G means :: GROUP_5:def 1 len it = len F & for k be Nat st k in dom F holds it.k = (F/.k) |^ a; end; theorem :: GROUP_5:9 (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a; theorem :: GROUP_5:10 (<*> the carrier of G) |^ a = {}; theorem :: GROUP_5:11 <* a *> |^ b = <* a |^ b *>; theorem :: GROUP_5:12 <* a,b *> |^ c = <* a |^ c,b |^ c *>; theorem :: GROUP_5:13 <* a,b,c *> |^ d = <* a |^ d,b |^ d,c |^ d *>; theorem :: GROUP_5:14 Product(F |^ a) = Product(F) |^ a; theorem :: GROUP_5:15 (F |^ a) |^ I = (F |^ I) |^ a; begin :: Commutators. definition let G,a,b; func [.a,b.] -> Element of G equals :: GROUP_5:def 2 a" * b" * a * b; end; theorem :: GROUP_5:16 [.a,b.] = a" * b" * a * b & [.a,b.] = a" * (b" * a) * b & [.a,b .] = a" * (b" * a * b) & [.a,b.] = a" * (b" * (a * b)) & [.a,b.] = (a" * b") * (a * b); theorem :: GROUP_5:17 [.a,b.] = (b * a)" * (a * b); theorem :: GROUP_5:18 [.a,b.] = (b" |^ a) * b & [.a,b.] = a" * (a |^ b); theorem :: GROUP_5:19 [.1_G,a.] = 1_G & [.a,1_G.] = 1_G; theorem :: GROUP_5:20 [.a,a.] = 1_G; theorem :: GROUP_5:21 [.a,a".] = 1_G & [.a",a.] = 1_G; theorem :: GROUP_5:22 [.a,b.]" = [.b,a.]; theorem :: GROUP_5:23 [.a,b.] |^ c = [.a |^ c,b |^ c.]; theorem :: GROUP_5:24 [.a,b.] = (a" |^ 2) * ((a * b") |^ 2)* (b |^ 2); theorem :: GROUP_5:25 [.a * b,c.] = [.a,c.] |^ b * [.b,c.]; theorem :: GROUP_5:26 [.a,b * c.] = [.a,c.] * ([.a,b.] |^ c); theorem :: GROUP_5:27 [.a",b.] = [.b,a.] |^ a"; theorem :: GROUP_5:28 [.a,b".] = [.b,a.] |^ b"; theorem :: GROUP_5:29 [.a",b".] = [.a,b.] |^ (a * b)" & [.a",b".] = [.a,b.] |^ (b * a)"; theorem :: GROUP_5:30 [.a,b |^ a".] = [.b,a".]; theorem :: GROUP_5:31 [.a |^ b",b.] = [.b",a.]; theorem :: GROUP_5:32 [.a |^ n,b.] = a |^ (- n) * ((a |^ b) |^ n); theorem :: GROUP_5:33 [.a,b |^ n.] = (b |^ a) |^ (- n) * (b |^ n); theorem :: GROUP_5:34 [.a |^ i,b.] = a |^ (- i) * ((a |^ b) |^ i); theorem :: GROUP_5:35 [.a,b |^ i.] = (b |^ a) |^ (- i) * (b |^ i); theorem :: GROUP_5:36 [.a,b.] = 1_G iff a * b = b * a; theorem :: GROUP_5:37 G is commutative Group iff for a,b holds [.a,b.] = 1_G; theorem :: GROUP_5:38 a in H & b in H implies [.a,b.] in H; definition let G,a,b,c; func [.a,b,c.] -> Element of G equals :: GROUP_5:def 3 [.[.a,b.],c.]; end; theorem :: GROUP_5:39 [.a,b,1_G.] = 1_G & [.a,1_G,b.] = 1_G & [.1_G,a,b.] = 1_G; theorem :: GROUP_5:40 [.a,a,b.] = 1_G; theorem :: GROUP_5:41 [.a,b,a.] = [.a |^ b,a.]; theorem :: GROUP_5:42 [.b,a,a.] = ([.b,a".] * [.b,a.]) |^ a; theorem :: GROUP_5:43 [.a,b,b |^ a.] = [.b,[.b,a.].]; theorem :: GROUP_5:44 [.a * b,c.] = [.a,c.] * [.a,c,b.] * [.b,c.]; theorem :: GROUP_5:45 [.a,b * c.] = [.a,c.] * [.a,b.] * [.a,b,c.]; :: :: P. Hall Identity. :: theorem :: GROUP_5:46 ([.a,b",c.] |^ b) * ([.b,c",a.] |^ c) * ([.c,a",b.] |^ a) = 1_G; definition let G,A,B; func commutators(A,B) -> Subset of G equals :: GROUP_5:def 4 {[.a,b.] : a in A & b in B}; end; theorem :: GROUP_5:47 x in commutators(A,B) iff ex a,b st x = [.a,b.] & a in A & b in B; theorem :: GROUP_5:48 commutators({} the carrier of G,A) = {} & commutators(A,{} the carrier of G) = {}; theorem :: GROUP_5:49 commutators({a},{b}) = {[.a,b.]}; theorem :: GROUP_5:50 A c= B & C c= D implies commutators(A,C) c= commutators(B,D); theorem :: GROUP_5:51 G is commutative Group iff for A,B st A <> {} & B <> {} holds commutators(A,B) = {1_G}; definition let G,H1,H2; func commutators(H1,H2) -> Subset of G equals :: GROUP_5:def 5 commutators(carr H1,carr H2); end; theorem :: GROUP_5:52 x in commutators(H1,H2) iff ex a,b st x = [.a,b.] & a in H1 & b in H2; theorem :: GROUP_5:53 1_G in commutators(H1,H2); theorem :: GROUP_5:54 commutators((1).G,H) = {1_G} & commutators(H,(1).G) = {1_G}; theorem :: GROUP_5:55 for N being strict normal Subgroup of G holds commutators(H,N) c= carr N & commutators(N,H) c= carr N; theorem :: GROUP_5:56 H1 is Subgroup of H2 & H3 is Subgroup of H4 implies commutators( H1,H3) c= commutators(H2,H4); theorem :: GROUP_5:57 G is commutative Group iff for H1,H2 holds commutators(H1,H2) = {1_G}; definition let G; func commutators G -> Subset of G equals :: GROUP_5:def 6 commutators((Omega).G,(Omega).G); end; theorem :: GROUP_5:58 x in commutators G iff ex a,b st x = [.a,b.]; theorem :: GROUP_5:59 G is commutative Group iff commutators G = {1_G}; definition let G,A,B; func [.A,B.] -> strict Subgroup of G equals :: GROUP_5:def 7 gr commutators(A,B); end; theorem :: GROUP_5:60 a in A & b in B implies [.a,b.] in [.A,B.]; theorem :: GROUP_5:61 x in [.A,B.] iff ex F,I st len F = len I & rng F c= commutators( A,B) & x = Product(F |^ I); theorem :: GROUP_5:62 A c= C & B c= D implies [.A,B.] is Subgroup of [.C,D.]; definition let G,H1,H2; func [.H1,H2.] -> strict Subgroup of G equals :: GROUP_5:def 8 [.carr H1,carr H2.]; end; theorem :: GROUP_5:63 [.H1,H2.] = gr commutators(H1,H2); theorem :: GROUP_5:64 x in [.H1,H2.] iff ex F,I st len F = len I & rng F c= commutators(H1, H2) & x = Product(F |^ I); theorem :: GROUP_5:65 a in H1 & b in H2 implies [.a,b.] in [.H1,H2.]; theorem :: GROUP_5:66 H1 is Subgroup of H2 & H3 is Subgroup of H4 implies [.H1,H3.] is Subgroup of [.H2,H4.]; theorem :: GROUP_5:67 for N being strict normal Subgroup of G holds [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N; theorem :: GROUP_5:68 for N1,N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G; theorem :: GROUP_5:69 [.N1,N2.] = [.N2,N1.]; theorem :: GROUP_5:70 for N1,N2,N3 being strict normal Subgroup of G holds [.N1 "\/" N2,N3.] = [.N1,N3.] "\/" [.N2,N3.]; theorem :: GROUP_5:71 for N1,N2,N3 being strict normal Subgroup of G holds [.N1,N2 "\/" N3.] = [.N1,N2.] "\/" [.N1,N3.]; definition let G be Group; func G` -> strict normal Subgroup of G equals :: GROUP_5:def 9 [.(Omega).G,(Omega).G.]; end; theorem :: GROUP_5:72 for G being Group holds G` = gr commutators G; theorem :: GROUP_5:73 for G being Group holds x in G` iff ex F being FinSequence of the carrier of G,I st len F = len I & rng F c= commutators G & x = Product(F |^ I); theorem :: GROUP_5:74 for G being strict Group, a,b be Element of G holds [.a,b.] in G `; theorem :: GROUP_5:75 for G being strict Group holds G is commutative Group iff G` = (1).G; theorem :: GROUP_5:76 for G being Group, H being strict Subgroup of G holds Left_Cosets H is finite & index H = 2 implies G` is Subgroup of H; begin :: Center of a Group. definition let G; func center G -> strict Subgroup of G means :: GROUP_5:def 10 the carrier of it = {a : for b holds a * b = b * a}; end; theorem :: GROUP_5:77 a in center G iff for b holds a * b = b * a; theorem :: GROUP_5:78 center G is normal Subgroup of G; theorem :: GROUP_5:79 for H being Subgroup of G holds H is Subgroup of center G implies H is normal Subgroup of G; theorem :: GROUP_5:80 center G is commutative; theorem :: GROUP_5:81 a in center G iff con_class a = {a}; theorem :: GROUP_5:82 for G being strict Group holds G is commutative Group iff center G = G;