:: Commutator and Center of a Group
:: by Wojciech A. Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2019 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;