:: Commutator and Center of a Group
:: by Wojciech A. Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2021 Association of Mizar Users

theorem Th1: :: GROUP_5:1

for x being set
for G being Group holds
( x in (1). G iff x = 1_ G )

proof end;

theorem :: GROUP_5:2

for G being Group
for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
a |^ b in H

proof end;

theorem Th3: :: GROUP_5:3

for G being Group
for a, b being Element of G
for N being strict normal Subgroup of G st a in N holds
a |^ b in N

proof end;

theorem Th4: :: GROUP_5:4

for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in H1 * H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )

proof end;

theorem Th5: :: GROUP_5:5

for x being set
for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )

proof end;

theorem :: GROUP_5:6

for x being set
for G being Group
for H1, H2 being Subgroup of G st G is commutative Group holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )

proof end;

theorem Th7: :: GROUP_5:7

for x being set
for G being Group
for N1, N2 being strict normal Subgroup of G holds
( x in N1 "\/" N2 iff ex a, b being Element of G st
( x = a * b & a in N1 & b in N2 ) )

proof end;

theorem :: GROUP_5:8

for G being Group
for H being Subgroup of G
for N being normal Subgroup of G holds H * N = N * H

proof end;

definition

let G be Group;
let F be FinSequence of the carrier of G;
let a be Element of G;

func F |^ a -> FinSequence of the carrier of G means :Def1: :: GROUP_5:def 1
( len it = len F & ( for k being Nat st k in dom F holds
it . k = (F /. k) |^ a ) );

existence
ex b₁ being FinSequence of the carrier of G st
( len b₁ = len F & ( for k being Nat st k in dom F holds
b₁ . k = (F /. k) |^ a ) )

proof end;

correctness
uniqueness
for b₁, b₂ being FinSequence of the carrier of G st len b₁ = len F & ( for k being Nat st k in dom F holds
b₁ . k = (F /. k) |^ a ) & len b₂ = len F & ( for k being Nat st k in dom F holds
b₂ . k = (F /. k) |^ a ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def1 defines |^ GROUP_5:def 1 :
for G being Group
for F being FinSequence of the carrier of G
for a being Element of G
for b₄ being FinSequence of the carrier of G holds
( b₄ = F |^ a iff ( len b₄ = len F & ( for k being Nat st k in dom F holds
b₄ . k = (F /. k) |^ a ) ) );

theorem Th9: :: GROUP_5:9

for G being Group
for a being Element of G
for F1, F2 being FinSequence of the carrier of G holds (F1 |^ a) ^ (F2 |^ a) = (F1 ^ F2) |^ a

proof end;

theorem Th10: :: GROUP_5:10

for G being Group
for a being Element of G holds (<*> the carrier of G) |^ a = {}

proof end;

theorem Th11: :: GROUP_5:11

for G being Group
for a, b being Element of G holds <*a*> |^ b = <*(a |^ b)*>

proof end;

theorem Th12: :: GROUP_5:12

for G being Group
for a, b, c being Element of G holds <*a,b*> |^ c = <*(a |^ c),(b |^ c)*>

proof end;

theorem :: GROUP_5:13

for G being Group
for a, b, c, d being Element of G holds <*a,b,c*> |^ d = <*(a |^ d),(b |^ d),(c |^ d)*>

proof end;

theorem Th14: :: GROUP_5:14

for G being Group
for a being Element of G
for F being FinSequence of the carrier of G holds Product (F |^ a) = (Product F) |^ a

proof end;

theorem Th15: :: GROUP_5:15

for G being Group
for a being Element of G
for F being FinSequence of the carrier of G
for I being FinSequence of INT holds (F |^ a) |^ I = (F |^ I) |^ a

proof end;

definition

let G be Group;
let a, b be Element of G;

func [.a,b.] -> Element of G equals :: GROUP_5:def 2
(((a ") * (b ")) * a) * b;

correctness
coherence
(((a ") * (b ")) * a) * b is Element of G;
;

end;

:: deftheorem defines [. GROUP_5:def 2 :
for G being Group
for a, b being Element of G holds [.a,b.] = (((a ") * (b ")) * a) * b;

theorem Th16: :: GROUP_5:16

for G being Group
for a, b being Element of G holds
( [.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) )

proof end;

theorem Th17: :: GROUP_5:17

for G being Group
for a, b being Element of G holds [.a,b.] = ((b * a) ") * (a * b)

proof end;

theorem :: GROUP_5:18

for G being Group
for a, b being Element of G holds
( [.a,b.] = ((b ") |^ a) * b & [.a,b.] = (a ") * (a |^ b) ) by Th16;

theorem Th19: :: GROUP_5:19

for G being Group
for a being Element of G holds
( [.(1_ G),a.] = 1_ G & [.a,(1_ G).] = 1_ G )

proof end;

theorem Th20: :: GROUP_5:20

for G being Group
for a being Element of G holds [.a,a.] = 1_ G

proof end;

theorem :: GROUP_5:21

for G being Group
for a being Element of G holds
( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )

proof end;

theorem Th22: :: GROUP_5:22

for G being Group
for a, b being Element of G holds [.a,b.] " = [.b,a.]

proof end;

theorem Th23: :: GROUP_5:23

for G being Group
for a, b, c being Element of G holds [.a,b.] |^ c = [.(a |^ c),(b |^ c).]

proof end;

theorem :: GROUP_5:24

for G being Group
for a, b being Element of G holds [.a,b.] = (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2)

proof end;

theorem Th25: :: GROUP_5:25

for G being Group
for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] |^ b) * [.b,c.]

proof end;

theorem :: GROUP_5:26

for G being Group
for a, b, c being Element of G holds [.a,(b * c).] = [.a,c.] * ([.a,b.] |^ c)

proof end;

theorem Th27: :: GROUP_5:27

for G being Group
for a, b being Element of G holds [.(a "),b.] = [.b,a.] |^ (a ")

proof end;

theorem Th28: :: GROUP_5:28

for G being Group
for a, b being Element of G holds [.a,(b ").] = [.b,a.] |^ (b ")

proof end;

theorem :: GROUP_5:29

for G being Group
for a, b being Element of G holds
( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )

proof end;

theorem :: GROUP_5:30

for G being Group
for a, b being Element of G holds [.a,(b |^ (a ")).] = [.b,(a ").]

proof end;

theorem :: GROUP_5:31

for G being Group
for a, b being Element of G holds [.(a |^ (b ")),b.] = [.(b "),a.]

proof end;

theorem :: GROUP_5:32

for n being Nat
for G being Group
for a, b being Element of G holds [.(a |^ n),b.] = (a |^ (- n)) * ((a |^ b) |^ n)

proof end;

theorem :: GROUP_5:33

for n being Nat
for G being Group
for a, b being Element of G holds [.a,(b |^ n).] = ((b |^ a) |^ (- n)) * (b |^ n)

proof end;

theorem :: GROUP_5:34

for i being Integer
for G being Group
for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

proof end;

theorem :: GROUP_5:35

for i being Integer
for G being Group
for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)

proof end;

theorem Th36: :: GROUP_5:36

for G being Group
for a, b being Element of G holds
( [.a,b.] = 1_ G iff a * b = b * a )

proof end;

Lm1: for G being commutative Group
for a, b being Element of G holds a * b = b * a
;

theorem :: GROUP_5:37

for G being Group holds
( G is commutative Group iff for a, b being Element of G holds [.a,b.] = 1_ G )

proof end;

theorem Th38: :: GROUP_5:38

for G being Group
for a, b being Element of G
for H being Subgroup of G st a in H & b in H holds
[.a,b.] in H

proof end;

definition

let G be Group;
let a, b, c be Element of G;

func [.a,b,c.] -> Element of G equals :: GROUP_5:def 3
[.[.a,b.],c.];

correctness
coherence
[.[.a,b.],c.] is Element of G;
;

end;

:: deftheorem defines [. GROUP_5:def 3 :
for G being Group
for a, b, c being Element of G holds [.a,b,c.] = [.[.a,b.],c.];

theorem :: GROUP_5:39

for G being Group
for a, b being Element of G holds
( [.a,b,(1_ G).] = 1_ G & [.a,(1_ G),b.] = 1_ G & [.(1_ G),a,b.] = 1_ G )

proof end;

theorem :: GROUP_5:40

for G being Group
for a, b being Element of G holds [.a,a,b.] = 1_ G

proof end;

theorem :: GROUP_5:41

for G being Group
for a, b being Element of G holds [.a,b,a.] = [.(a |^ b),a.]

proof end;

theorem :: GROUP_5:42

for G being Group
for a, b being Element of G holds [.b,a,a.] = ([.b,(a ").] * [.b,a.]) |^ a

proof end;

theorem :: GROUP_5:43

for G being Group
for a, b being Element of G holds [.a,b,(b |^ a).] = [.b,[.b,a.].]

proof end;

theorem :: GROUP_5:44

for G being Group
for a, b, c being Element of G holds [.(a * b),c.] = ([.a,c.] * [.a,c,b.]) * [.b,c.]

proof end;

theorem :: GROUP_5:45

for G being Group
for a, b, c being Element of G holds [.a,(b * c).] = ([.a,c.] * [.a,b.]) * [.a,b,c.]

proof end;

::
:: P. Hall Identity.
::

theorem :: GROUP_5:46

for G being Group
for a, b, c being Element of G holds (([.a,(b "),c.] |^ b) * ([.b,(c "),a.] |^ c)) * ([.c,(a "),b.] |^ a) = 1_ G

proof end;

definition

let G be Group;
let A, B be Subset of G;

func commutators (A,B) -> Subset of G equals :: GROUP_5:def 4
{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } ;

coherence
{ [.a,b.] where a, b is Element of G : ( a in A & b in B ) } is Subset of G

proof end;

end;

:: deftheorem defines commutators GROUP_5:def 4 :
for G being Group
for A, B being Subset of G holds commutators (A,B) = { [.a,b.] where a, b is Element of G : ( a in A & b in B ) } ;

theorem Th47: :: GROUP_5:47

for x being set
for G being Group
for A, B being Subset of G holds
( x in commutators (A,B) iff ex a, b being Element of G st
( x = [.a,b.] & a in A & b in B ) ) ;

theorem :: GROUP_5:48

for G being Group
for A being Subset of G holds
( commutators (({} the carrier of G),A) = {} & commutators (A,({} the carrier of G)) = {} )

proof end;

theorem :: GROUP_5:49

for G being Group
for a, b being Element of G holds commutators ({a},{b}) = {[.a,b.]}

proof end;

theorem Th50: :: GROUP_5:50

for G being Group
for A, B, C, D being Subset of G st A c= B & C c= D holds
commutators (A,C) c= commutators (B,D)

proof end;

theorem Th51: :: GROUP_5:51

for G being Group holds
( G is commutative Group iff for A, B being Subset of G st A <> {} & B <> {} holds
commutators (A,B) = {(1_ G)} )

proof end;

definition

let G be Group;
let H1, H2 be Subgroup of G;

func commutators (H1,H2) -> Subset of G equals :: GROUP_5:def 5
commutators ((carr H1),(carr H2));

correctness
coherence
commutators ((carr H1),(carr H2)) is Subset of G;
;

end;

:: deftheorem defines commutators GROUP_5:def 5 :
for G being Group
for H1, H2 being Subgroup of G holds commutators (H1,H2) = commutators ((carr H1),(carr H2));

theorem Th52: :: GROUP_5:52

for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in commutators (H1,H2) iff ex a, b being Element of G st
( x = [.a,b.] & a in H1 & b in H2 ) )

proof end;

theorem Th53: :: GROUP_5:53

for G being Group
for H1, H2 being Subgroup of G holds 1_ G in commutators (H1,H2)

proof end;

theorem :: GROUP_5:54

for G being Group
for H being Subgroup of G holds
( commutators (((1). G),H) = {(1_ G)} & commutators (H,((1). G)) = {(1_ G)} )

proof end;

theorem Th55: :: GROUP_5:55

for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( commutators (H,N) c= carr N & commutators (N,H) c= carr N )

proof end;

theorem Th56: :: GROUP_5:56

for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
commutators (H1,H3) c= commutators (H2,H4)

proof end;

theorem Th57: :: GROUP_5:57

for G being Group holds
( G is commutative Group iff for H1, H2 being Subgroup of G holds commutators (H1,H2) = {(1_ G)} )

proof end;

definition

let G be Group;

func commutators G -> Subset of G equals :: GROUP_5:def 6
commutators (((Omega). G),((Omega). G));

correctness
coherence
commutators (((Omega). G),((Omega). G)) is Subset of G;
;

end;

:: deftheorem defines commutators GROUP_5:def 6 :
for G being Group holds commutators G = commutators (((Omega). G),((Omega). G));

theorem Th58: :: GROUP_5:58

for x being set
for G being Group holds
( x in commutators G iff ex a, b being Element of G st x = [.a,b.] )

proof end;

theorem :: GROUP_5:59

for G being Group holds
( G is commutative Group iff commutators G = {(1_ G)} )

proof end;

definition

let G be Group;
let A, B be Subset of G;

func [.A,B.] -> strict Subgroup of G equals :: GROUP_5:def 7
gr (commutators (A,B));

correctness
coherence
gr (commutators (A,B)) is strict Subgroup of G;
;

end;

:: deftheorem defines [. GROUP_5:def 7 :
for G being Group
for A, B being Subset of G holds [.A,B.] = gr (commutators (A,B));

theorem Th60: :: GROUP_5:60

for G being Group
for a, b being Element of G
for A, B being Subset of G st a in A & b in B holds
[.a,b.] in [.A,B.]

proof end;

theorem Th61: :: GROUP_5:61

for x being set
for G being Group
for A, B being Subset of G holds
( x in [.A,B.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (A,B) & x = Product (F |^ I) ) )

proof end;

theorem :: GROUP_5:62

for G being Group
for A, B, C, D being Subset of G st A c= C & B c= D holds
[.A,B.] is Subgroup of [.C,D.] by Th50, GROUP_4:32;

definition

let G be Group;
let H1, H2 be Subgroup of G;

func [.H1,H2.] -> strict Subgroup of G equals :: GROUP_5:def 8
[.(carr H1),(carr H2).];

correctness
coherence
[.(carr H1),(carr H2).] is strict Subgroup of G;
;

end;

:: deftheorem defines [. GROUP_5:def 8 :
for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = [.(carr H1),(carr H2).];

theorem :: GROUP_5:63

for G being Group
for H1, H2 being Subgroup of G holds [.H1,H2.] = gr (commutators (H1,H2)) ;

theorem :: GROUP_5:64

for x being set
for G being Group
for H1, H2 being Subgroup of G holds
( x in [.H1,H2.] iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators (H1,H2) & x = Product (F |^ I) ) ) by Th61;

theorem Th65: :: GROUP_5:65

for G being Group
for a, b being Element of G
for H1, H2 being Subgroup of G st a in H1 & b in H2 holds
[.a,b.] in [.H1,H2.]

proof end;

theorem :: GROUP_5:66

for G being Group
for H1, H2, H3, H4 being Subgroup of G st H1 is Subgroup of H2 & H3 is Subgroup of H4 holds
[.H1,H3.] is Subgroup of [.H2,H4.]

proof end;

theorem :: GROUP_5:67

for G being Group
for H being Subgroup of G
for N being strict normal Subgroup of G holds
( [.N,H.] is Subgroup of N & [.H,N.] is Subgroup of N )

proof end;

theorem Th68: :: GROUP_5:68

for G being Group
for N1, N2 being strict normal Subgroup of G holds [.N1,N2.] is normal Subgroup of G

proof end;

Lm2: for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] is Subgroup of [.N2,N1.]

proof end;

theorem Th69: :: GROUP_5:69

for G being Group
for N1, N2 being normal Subgroup of G holds [.N1,N2.] = [.N2,N1.]

proof end;

theorem Th70: :: GROUP_5:70

for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.(N1 "\/" N2),N3.] = [.N1,N3.] "\/" [.N2,N3.]

proof end;

theorem :: GROUP_5:71

for G being Group
for N1, N2, N3 being strict normal Subgroup of G holds [.N1,(N2 "\/" N3).] = [.N1,N2.] "\/" [.N1,N3.]

proof end;

definition

let G be Group;

func G ` -> strict normal Subgroup of G equals :: GROUP_5:def 9
[.((Omega). G),((Omega). G).];

coherence
[.((Omega). G),((Omega). G).] is strict normal Subgroup of G

proof end;

end;

:: deftheorem defines ` GROUP_5:def 9 :
for G being Group holds G ` = [.((Omega). G),((Omega). G).];

theorem :: GROUP_5:72

for G being Group holds G ` = gr (commutators G) ;

theorem Th73: :: GROUP_5:73

for x being set
for G being Group holds
( x in G ` iff ex F being FinSequence of the carrier of G ex I being FinSequence of INT st
( len F = len I & rng F c= commutators G & x = Product (F |^ I) ) )

proof end;

theorem Th74: :: GROUP_5:74

for G being strict Group
for a, b being Element of G holds [.a,b.] in G `

proof end;

theorem :: GROUP_5:75

for G being strict Group holds
( G is commutative Group iff G ` = (1). G )

proof end;

theorem :: GROUP_5:76

for G being Group
for H being strict Subgroup of G st Left_Cosets H is finite & index H = 2 holds
G ` is Subgroup of H

proof end;

definition

let G be Group;

func center G -> strict Subgroup of G means :Def10: :: GROUP_5:def 10
the carrier of it = { a where a is Element of G : for b being Element of G holds a * b = b * a } ;

existence
ex b₁ being strict Subgroup of G st the carrier of b₁ = { a where a is Element of G : for b being Element of G holds a * b = b * a }

proof end;

uniqueness
for b₁, b₂ being strict Subgroup of G st the carrier of b₁ = { a where a is Element of G : for b being Element of G holds a * b = b * a } & the carrier of b₂ = { a where a is Element of G : for b being Element of G holds a * b = b * a } holds
b₁ = b₂ by GROUP_2:59;

end;

:: deftheorem Def10 defines center GROUP_5:def 10 :
for G being Group
for b₂ being strict Subgroup of G holds
( b₂ = center G iff the carrier of b₂ = { a where a is Element of G : for b being Element of G holds a * b = b * a } );

theorem Th77: :: GROUP_5:77

for G being Group
for a being Element of G holds
( a in center G iff for b being Element of G holds a * b = b * a )

proof end;

theorem :: GROUP_5:78

for G being Group holds center G is normal Subgroup of G

proof end;

theorem :: GROUP_5:79

for G being Group
for H being Subgroup of G st H is Subgroup of center G holds
H is normal Subgroup of G

proof end;

theorem :: GROUP_5:80

for G being Group holds center G is commutative

proof end;

theorem :: GROUP_5:81

for G being Group
for a being Element of G holds
( a in center G iff con_class a = {a} )

proof end;

theorem :: GROUP_5:82

for G being strict Group holds
( G is commutative Group iff center G = G )

proof end;