:: Some Properties of $p$-Groups and Commutative $p$-Groups
:: by Xiquan Liang and Dailu Li
::
:: Received April 29, 2010
:: Copyright (c) 2010-2026 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 ARYTM_3, RELAT_1, FUNCT_1, SUBSET_1, BINOP_1, GROUP_1, NAT_1,
CARD_1, GROUP_2, FUNCT_2, FINSET_1, GRAPH_1, NEWTON, XBOOLE_0, NAT_3,
GROUP_10, ALGSTR_0, NUMBERS, INT_2, XXREAL_0, GROUP_6, PRE_TOPC,
STRUCT_0, GROUP_5, QC_LANG1, CQC_SIM1, WELLORD1, MOEBIUS1, GROUPP_1;
notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_2, FUNCT_2,
STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, NEWTON, DOMAIN_1, GR_CY_1,
GROUP_4, NAT_3, GROUP_10, MOEBIUS1, GROUP_5, GROUP_6, INT_1;
constructors NAT_D, GR_CY_1, GROUP_4, NAT_3, GROUP_10, BINOP_1, BINOP_2,
GROUP_5, MOEBIUS1, GROUP_6, REALSET1;
registrations RELSET_1, FINSET_1, XREAL_0, NAT_1, INT_1, CARD_1, NEWTON,
STRUCT_0, GROUP_2, GROUP_1, GROUP_3, GR_CY_1, FUNCT_2, NAT_3, GROUP_10,
GROUP_6, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions GROUP_10;
equalities STRUCT_0, ALGSTR_0, GROUP_4, GROUP_6;
expansions STRUCT_0, GROUP_10, GROUP_6;
theorems GROUP_2, GROUP_3, GROUP_6, NAT_1, GROUP_1, ORDINAL1, NAT_D, GR_CY_1,
NEWTON, PEPIN, GROUP_8, NAT_3, GROUP_10, INT_2, GROUP_5, MOEBIUS1, NAT_5,
GROUP_11, GROUP_4, TARSKI;
schemes NAT_1;
begin :: $p$-Groups
reserve G for Group,
a,b for Element of G,
m, n for Nat,
p for Prime;
theorem Th1:
(for r being Nat holds n <> p |^ r) implies
ex s being Element of NAT st s is prime & s divides n & s <> p
proof
assume
A1: for r being Nat holds n <> p |^ r;
per cases;
suppose
A2: n = 0;
per cases;
suppose
A3: p = 2;
take s = 3;
thus s is prime by PEPIN:41;
thus s divides n by A2,INT_2:12;
thus s <> p by A3;
end;
suppose
A4: p <> 2;
take s = 2;
thus s is prime by INT_2:28;
thus s divides n by A2,INT_2:12;
thus s <> p by A4;
end;
end;
suppose
A5: n <> 0;
A6: p > 1 by INT_2:def 4;
reconsider r1 = p |-count n as Element of NAT;
A7: p |^ r1 divides n by A5,A6,NAT_3:def 7;
A8: not p |^ (r1+1) divides n by A5,A6,NAT_3:def 7;
consider s1 be Nat such that
A9: n = p |^ r1 * s1 by A7,NAT_D:def 3;
s1 >= 2
proof
assume not s1 >= 2;
then s1 < 1 + 1;
then s1 <= 1 by NAT_1:13;
then s1 = 0 or s1 = 1 by NAT_1:25;
hence contradiction by A5,A1,A9;
end;
then consider s be Element of NAT such that
A10: s is prime and
A11: s divides s1 by INT_2:31;
A12: s1 divides n by A9,NAT_D:def 3;
take s;
s <> p
proof
assume s = p;
then consider s2 be Nat such that
A13: s1 = p * s2 by A11,NAT_D:def 3;
n = p |^ r1 * p * s2 by A9,A13
.= p |^ (r1+1) * s2 by NEWTON:6;
hence contradiction by A8,NAT_D:def 3;
end;
hence thesis by A10,A11,A12,NAT_D:4;
end;
end;
theorem Th2:
for n,m being Nat holds n divides p |^ m implies
ex r be Nat st n = p |^ r & r <= m
proof
let n,m be Nat;
assume
A1: n divides p |^ m;
n > 0
proof
assume n <= 0;
then n = 0;
hence contradiction by A1,INT_2:3;
end;
then n in NatDivisors (p|^ m) by A1,MOEBIUS1:39;
then n in {p|^ k where k is Element of NAT : k <= m} by NAT_5:19;
then consider r be Element of NAT such that
A2: n = p|^ r & r <= m;
take r;
thus thesis by A2;
end;
theorem Th3:
a |^ n = 1_G implies a" |^ n = 1_G
proof
assume a |^ n = 1_G;
then a" |^ n = (1_G)" by GROUP_1:37
.= 1_G by GROUP_1:8;
hence thesis;
end;
theorem Th4:
a" |^ n = 1_G implies a |^ n = 1_G
proof
a"" = a;
hence thesis by Th3;
end;
theorem Th5:
ord (a") = ord a
proof
a |^ ord a = 1_G by GROUP_1:41;
then a" |^ ord a = 1_G by Th3; then
A1: ord (a") divides ord a by GROUP_1:44;
a" |^ ord (a") = 1_G by GROUP_1:41;
then a |^ ord (a") = 1_G by Th4;
then ord a divides ord (a") by GROUP_1:44;
hence thesis by A1,NAT_D:5;
end;
theorem Th6:
ord (a |^ b) = ord a
proof
(a |^ b) |^ ord a = (a |^ ord a) |^ b by GROUP_3:27
.= (1_G) |^ b by GROUP_1:41
.= 1_G by GROUP_3:17; then
A1: ord (a |^ b) divides ord a by GROUP_1:44;
(a |^ ord (a |^ b)) |^ b = (a |^ b) |^ ord (a |^ b) by GROUP_3:27
.= 1_G by GROUP_1:41;
then ord a divides ord (a |^ b) by GROUP_1:44,GROUP_3:18;
hence thesis by A1,NAT_D:5;
end;
theorem Th7:
for G being Group, N being Subgroup of G
for a,b being Element of G holds
N is normal & b in N implies
for n ex g being Element of G st g in N & (a * b)|^ n = a |^ n * g
proof
let G be Group;
let N be Subgroup of G;
let a,b be Element of G;
assume
A1: N is normal & b in N;
defpred P[Nat] means for n ex g being Element of G
st g in N & (a * b)|^ $1 = a |^ $1 * g;
A2: (a * b)|^ 0 = 1_G by GROUP_1:25;
a |^ 0 * 1_G = 1_G * 1_G by GROUP_1:25
.= 1_G by GROUP_1:def 4;
then
A3: P[0] by A2,GROUP_2:46;
A4: now let n;
assume P[n];
then consider g1 be Element of G such that
A5: g1 in N & (a * b)|^ n = a |^ n * g1;
A6: (a * b)|^ (n + 1) = a |^ n * g1 * (a * b) by A5,GROUP_1:34
.= a |^ n * (g1 * (a * b)) by GROUP_1:def 3
.= a |^ n * ((g1 * a) * b) by GROUP_1:def 3;
a * N = N * a by A1,GROUP_3:117;
then g1 * a in a * N by A5,GROUP_2:104;
then consider g2 be Element of G such that
A7: g1 * a = a * g2 & g2 in N by GROUP_2:103;
(g1 * a) * b = a * (g2 * b) by A7,GROUP_1:def 3;
then a |^ n * ((g1 * a) * b) = a |^ n * a * (g2 * b) by GROUP_1:def 3
.= a |^ (n + 1) * (g2 * b) by GROUP_1:34;
hence P[n+1] by A1,A6,A7,GROUP_2:50;
end;
for n holds P[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th8:
for G being Group, N being normal Subgroup of G,
a being Element of G, S being Element of G./.N holds
S = a * N implies
for n holds S |^ n = (a |^ n) * N
proof
let G be Group;
let N be normal Subgroup of G;
let a be Element of G;
let S be Element of G./.N;
assume
A1: S = a * N;
defpred P[Nat] means for n holds S |^ $1 = (a |^ $1) * N;
A2: S |^ 0 = 1_ (G./.N) by GROUP_1:25;
(a |^ 0) * N = 1_G * N by GROUP_1:25
.= carr N by GROUP_2:109;
then
A3: P[0] by A2,GROUP_6:24;
A4: now
let n;
assume
A5: P[n];
S |^ (n + 1) = S |^ n * S by GROUP_1:34
.= @ (S |^ n) * @ S by GROUP_6:def 3
.= ((a |^ n) * N) * (a * N) by A1,A5
.= ((a |^ n) * a) * N by GROUP_11:1
.= (a |^ (n + 1)) * N by GROUP_1:34;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem Th9:
for G being Group, H being Subgroup of G, a,b being Element of G
holds a * H = b * H implies ex h being Element of G st a = b * h & h in H
by GROUP_2:108,GROUP_2:103;
theorem Th10:
for G being finite Group, N being normal Subgroup of G holds
N is Subgroup of center G & G./.N is cyclic
implies G is commutative
proof
let G be finite Group;
let N be normal Subgroup of G;
assume that
A1: N is Subgroup of center G and
A2: G./.N is cyclic;
reconsider I = G./.N as finite Group;
consider S be Element of I such that
A3: for T being Element of I ex n being Nat st T = S |^ n
by A2,GR_CY_1:18;
consider a1 be Element of G such that
A4: S = a1 * N & S = N * a1 by GROUP_6:21;
for a,b being Element of G holds a * b = b * a
proof
let a,b be Element of G;
A5: a * N is Element of I & b * N is Element of I by GROUP_6:22;
then consider r1 be Nat such that
A6: a * N = S |^ r1 by A3;
a * N = (a1 |^ r1) * N by A4,Th8,A6;
then consider c1 be Element of G such that
A7: a = (a1 |^ r1) * c1 & c1 in N by Th9;
A8: c1 in center G by A1,A7,GROUP_2:40;
consider r2 be Nat such that
A9: b * N = S |^ r2 by A3,A5;
b * N = (a1 |^ r2) * N by A4,Th8,A9;
then consider c2 be Element of G such that
A10: b = (a1 |^ r2) * c2 & c2 in N by Th9;
A11: c2 in center G by A1,A10,GROUP_2:40;
a * b = (a1 |^ r1) * (c1 * ((a1 |^ r2) * c2)) by A7,A10,GROUP_1:def 3
.= (a1 |^ r1) * (((a1 |^ r2) * c2) * c1) by A8,GROUP_5:77
.= (a1 |^ r1) * ((a1 |^ r2) * (c2 * c1)) by GROUP_1:def 3
.= ((a1 |^ r1) * (a1 |^ r2)) * (c2 * c1) by GROUP_1:def 3
.= (a1 |^ (r1 + r2)) * (c2 * c1) by GROUP_1:33
.= ((a1 |^ r2) * (a1 |^ r1)) * (c2 * c1) by GROUP_1:33
.= (a1 |^ r2) * ((a1 |^ r1) * (c2 * c1)) by GROUP_1:def 3
.= (a1 |^ r2) * ((a1 |^ r1) * c2 * c1) by GROUP_1:def 3
.= (a1 |^ r2) * (c2 * (a1 |^ r1) * c1) by A11,GROUP_5:77
.= (a1 |^ r2) * (c2 * ((a1 |^ r1) * c1)) by GROUP_1:def 3
.= b * a by A7,A10,GROUP_1:def 3;
hence thesis;
end;
hence thesis by GROUP_1:def 12;
end;
theorem
for G being finite Group, N being normal Subgroup of G holds
N = center G & G./.N is cyclic implies G is commutative
proof
let G be finite Group;
let N be normal Subgroup of G;
assume
A1: N = center G & G./.N is cyclic;
then N is Subgroup of center G by GROUP_2:54;
hence thesis by A1,Th10;
end;
theorem
for G being finite Group, H being Subgroup of G holds
card H <> card G implies ex a being Element of G st not a in H
proof
let G be finite Group;
let H be Subgroup of G;
assume
A1: card H <> card G;
assume not ex a being Element of G st not a in H;
then the multMagma of H = the multMagma of G by GROUP_2:62;
hence contradiction by A1;
end;
definition
let p be Nat;
let G be Group;
let a be Element of G;
attr a is p-power means :Def1:
ex r being Nat st ord a = p |^ r;
end;
theorem Th13:
1_G is m-power
proof
A1: ord 1_G = 1 by GROUP_1:42;
m |^ 0 = 1 by NEWTON:4;
hence thesis by A1;
end;
registration
let G,m;
cluster m-power for Element of G;
existence
proof
take 1_G;
thus thesis by Th13;
end;
end;
registration
let p,G;
let a be p-power Element of G;
cluster a" -> p-power;
coherence
proof
consider n be Nat such that
A1:ord a = p |^ n by Def1;
ord (a") = p |^ n by A1,Th5;
hence thesis;
end;
end;
theorem
a |^ b is p-power implies a is p-power
proof
assume a |^ b is p-power;
then consider r be Nat such that
A1: ord (a |^ b) = p |^ r;
ord a = p |^ r by A1,Th6;
hence thesis;
end;
registration
let p,G,b;
let a be p-power Element of G;
cluster a |^ b -> p-power;
coherence
proof
consider n be Nat such that
A1: ord a = p |^ n by Def1;
ord (a |^ b) = p |^ n by A1,Th6;
hence thesis;
end;
end;
registration
let p;
let G be commutative Group, a,b be p-power Element of G;
cluster a * b -> p-power;
coherence
proof
consider n be Nat such that
A1: ord a = p |^ n by Def1;
consider m be Nat such that
A2: ord b = p |^ m by Def1;
A3: a |^ (p |^(n + m)) = a |^ (p |^ n * p |^ m) by NEWTON:8
.= a |^ (p |^ n) |^ (p |^ m) by GROUP_1:35
.= (1_G) |^ (p |^ m) by A1,GROUP_1:41
.= 1_G by GROUP_1:31;
b |^ (p |^(n + m)) = b |^ (p |^ m * p |^ n) by NEWTON:8
.= b |^ (p |^ m) |^ (p |^ n) by GROUP_1:35
.= (1_G) |^ (p |^ n) by A2,GROUP_1:41
.= 1_G by GROUP_1:31;
then (a * b) |^ (p |^(n + m)) = 1_G * 1_G by A3,GROUP_1:48
.= 1_G by GROUP_1:def 4;
then consider r be Nat such that
A4: ord (a * b) = p |^ r & r <= (n + m) by Th2,GROUP_1:44;
take r;
thus thesis by A4;
end;
end;
registration
let p;
let G be finite p-group Group;
cluster -> p-power for Element of G;
coherence
proof
let a be Element of G;
consider m be Nat such that
A1: card G = p |^ m by GROUP_10:def 17;
ex r be Nat st
ord a = p |^ r & r <= m by A1,Th2,GR_CY_1:8;
hence thesis;
end;
end;
theorem Th15:
for G being finite Group,H being Subgroup of G
for a being Element of G st H is p-group & a in H
holds a is p-power
proof
let G be finite Group;
let H be Subgroup of G;
let a be Element of G;
assume that
A1: H is p-group and
A2: a in H;
a is Element of H by A2;
then consider b be Element of H such that
A3: b= a;
consider r be Nat such that
A4: ord b = p |^ r by A1,Def1;
ord a = p |^ r by A3,A4,GROUP_8:5;
hence thesis;
end;
registration
let p;
let G be finite p-group Group;
cluster -> p-group for Subgroup of G;
coherence
proof
let H be Subgroup of G;
consider m be Nat such that
A1: card G = p |^ m by GROUP_10:def 17;
ex r be Nat st card H = p |^ r & r <= m by A1,Th2,GROUP_2:148;
hence thesis;
end;
end;
theorem Th16:
(1).G is p-group
proof
take 0;
thus card (1).G = 1 by GROUP_2:69
.= p |^ 0 by NEWTON:4;
end;
registration
let p;
let G be Group;
cluster p-group for Subgroup of G;
existence
proof
take (1).G;
thus thesis by Th16;
end;
end;
registration
let p;
let G be finite Group, G1 be p-group Subgroup of G, G2 be Subgroup of G;
cluster G1 /\ G2 -> p-group;
coherence
proof
reconsider H1 = G1 /\ G2 as Subgroup of G1 by GROUP_2:88;
H1 is p-group;
hence thesis;
end;
cluster G2 /\ G1 -> p-group;
coherence;
end;
theorem Th17:
for G being finite Group st for a being Element of G holds a is p-power
holds G is p-group
proof
let G be finite Group;
assume
A1: for a being Element of G holds a is p-power;
assume not G is p-group;
then for r being Nat holds card G <> p |^ r;
then consider s be Element of NAT such that
A2: s is prime & s divides card G and
A3: s <> p by Th1;
consider b be Element of G such that
A4: ord b = s by A2,GROUP_10:11;
b is p-power by A1;
then ex r1 be Nat st ord b = p |^ r1;
hence contradiction by A2,A4,A3,NAT_3:6;
end;
registration
let p;
let G be finite p-group Group, N being normal Subgroup of G;
cluster G./.N -> p-group;
coherence
proof
consider r be Nat such that
A1: card G = p |^ r by GROUP_10:def 17;
A2: card G = card N * index N by GROUP_2:147;
A3: card(G./.N) = index N by GROUP_6:27;
reconsider n = card(G./.N) as Nat;
n divides p |^ r by A1,A2,A3,NAT_D:def 3;
then ex r1 be Nat st
n = p |^ r1 & r1 <= r by Th2;
hence thesis;
end;
end;
theorem
for G being finite Group, N being normal Subgroup of G
st N is p-group & G./.N is p-group holds
G is p-group
proof
let G be finite Group;
let N be normal Subgroup of G;
assume that
A1: N is p-group and
A2: G./.N is p-group;
consider r1 be Nat such that
A3: card N = p |^ r1 by A1;
consider r2 be Nat such that
A4: card (G./.N) = p |^ r2 by A2;
card(G./.N) = index N by GROUP_6:27;
then card G = p |^ r1 * p |^ r2 by A3,A4,GROUP_2:147
.= p |^ (r1 + r2) by NEWTON:8;
hence thesis;
end;
theorem Th19:
for G being finite commutative Group,H,H1,H2 being Subgroup of G st
H1 is p-group & H2 is p-group &
the carrier of H = H1 * H2 holds H is p-group
proof
let G be finite commutative Group;
let H,H1,H2 be Subgroup of G;
assume that
A1: H1 is p-group & H2 is p-group and
A2: the carrier of H = H1 * H2;
for a being Element of H holds a is p-power
proof
let a be Element of H;
a in H1 * H2 by A2;
then consider b1,b2 be Element of G such that
A3: a = b1 * b2 & b1 in H1 & b2 in H2 by GROUP_11:6;
b1 is p-power & b2 is p-power by A1,A3,Th15;
then consider r be Nat such that
A4: ord (b1 * b2) = p |^ r by Def1;
ord a = p |^ r by A3,A4,GROUP_8:5;
hence thesis;
end;
hence thesis by Th17;
end;
theorem Th20:
for G being finite Group, H,N being Subgroup of G holds
N is normal Subgroup of G &
H is p-group & N is p-group
implies ex P being strict Subgroup of G st the carrier of P = H * N &
P is p-group
proof
let G be finite Group;
let H,N be Subgroup of G;
assume that
A1: N is normal Subgroup of G and
A2: H is p-group & N is p-group;
H * N = N * H by A1,GROUP_5:8;
then consider P be strict Subgroup of G such that
A3: the carrier of P = H * N by GROUP_2:78;
A4: for a being Element of P holds a is p-power
proof
let a be Element of P;
a in H * N by A3;
then consider b,c be Element of G such that
A5: a = b * c & b in H & c in N by GROUP_11:6;
b is p-power by A5,A2,Th15;
then consider n be Nat such that
A6: ord b = p |^ n;
A7: b |^(p |^ n) = 1_G by A6,GROUP_1:41;
consider d be Element of G such that
A8: d in N & (b * c) |^(p |^ n) = b |^(p |^ n) * d by A1,A5,Th7;
d is p-power by A2,A8,Th15;
then consider m be Nat such that
A9: ord d = p |^ m;
A10: d |^(p |^ m) = 1_G by A9,GROUP_1:41;
A11:a |^(p |^ (n + m)) = (b * c) |^(p |^ (n + m)) by A5,GROUP_8:4
.= (b * c) |^(p |^ n * (p |^ m)) by NEWTON:8
.= (b * c) |^(p |^ n) |^ (p |^ m) by GROUP_1:35
.= 1_G by A7,A8,A10,GROUP_1:def 4;
reconsider a1 = a as Element of G by GROUP_2:42;
a1 |^(p |^ (n + m)) = 1_G by A11,GROUP_8:4;
then consider r be Nat such that
A12: ord a1 = p |^ r & r <= n + m by Th2,GROUP_1:44;
ord a = p |^ r by A12,GROUP_8:5;
hence thesis;
end;
take P;
thus thesis by A3,A4,Th17;
end;
theorem Th21:
for G being finite Group,N1,N2 being normal Subgroup of G
holds N1 is p-group &
N2 is p-group implies ex N being strict normal Subgroup of G
st the carrier of N = N1 * N2 & N is p-group
proof
let G be finite Group;
let N1,N2 be normal Subgroup of G;
assume N1 is p-group & N2 is p-group; then
consider N be strict Subgroup of G such that
A1: the carrier of N = N1 * N2 & N is p-group by Th20;
for x,y be Element of G st y in N holds x * y * x" in N
proof
let x,y be Element of G;
assume y in N;
then y in the carrier of N;
then consider a,b be Element of G such that
A2: y = a * b & a in N1 & b in N2 by A1,GROUP_11:6;
A3: x * y * x" =((x * a) * b) * x" by A2,GROUP_1:def 3
.=(x * a) * (b * x") by GROUP_1:def 3
.=(x * a) * 1_G * (b * x") by GROUP_1:def 4
.=(x * a) * (x" * x) * (b * x") by GROUP_1:def 5
.=(x * a) * x" * x * (b * x") by GROUP_1:def 3
.=((x * a) * x") * (x * (b * x")) by GROUP_1:def 3
.=(x * a * x") * (x * b * x") by GROUP_1:def 3;
x * a * x" in N1 & x * b * x" in N2 by A2,GROUP_11:4;
then x * y * x" in N1 * N2 by A3,GROUP_11:6;
hence thesis by A1;
end;
then N is normal Subgroup of G by GROUP_11:5;
hence thesis by A1;
end;
registration
let p;
let G be p-group finite Group, H be finite Group, g be Homomorphism of G,H;
cluster Image g -> p-group;
coherence
proof
for h being Element of Image g holds h is p-power
proof
let h be Element of Image g;
h in Image g;
then consider a be Element of G such that
A1: h = g.a by GROUP_6:45;
consider n be Nat such that
A2: ord a = p |^ n by Def1;
A3: g.(a |^(p |^ n)) = (g.a) |^(p |^ n) by GROUP_6:37
.= h |^(p |^ n) by A1,GROUP_8:4;
A4: g.(a |^(p |^ n)) = g.(1_G) by A2,GROUP_1:41
.= 1_H by GROUP_6:31;
reconsider h1 = h as Element of H by GROUP_2:42;
h1 |^(p |^ n) = 1_H by A3,A4,GROUP_8:4;
then consider r be Nat such that
A5: ord h1 = p |^ r & r <= n by Th2,GROUP_1:44;
ord h = p |^ r by A5,GROUP_8:5;
hence thesis;
end;
hence thesis by Th17;
end;
end;
theorem Th22:
for G,H being strict Group holds G,H are_isomorphic &
G is p-group implies H is p-group
by GROUP_6:73;
definition
let p be Prime;
let G be Group such that
A1: G is p-group;
func expon (G,p) -> Nat means
:Def2:
card G = p |^ it;
existence by A1;
uniqueness
proof
let a,b be Nat such that
A2: card G = p |^ a and
A3: card G = p |^ b;
p > 1 by INT_2:def 4;
hence thesis by A2,A3,PEPIN:30;
end;
end;
definition
let p be Prime;
let G be Group;
redefine func expon (G,p) -> Element of NAT; :: redefines expon (GROUPP_1, definition)
coherence by ORDINAL1:def 12;
end;
theorem
for G being finite Group, H being Subgroup of G st
G is p-group holds expon (H,p) <= expon (G,p)
proof
let G be finite Group;
let H be Subgroup of G;
assume
A1: G is p-group;
then card G = p |^ expon (G,p) by Def2;
then ex r be Nat st
card H = p |^ r & r <= expon (G,p) by Th2,GROUP_2:148;
hence thesis by A1,Def2;
end;
theorem Th24:
for G being strict finite Group st G is p-group & expon (G,p) = 0 holds
G = (1).G
proof
let G be strict finite Group;
assume G is p-group & expon (G,p) = 0; then
A1: card G = p |^ 0 by Def2
.= 1 by NEWTON:4;
card (1).G = 1 by GROUP_2:69;
hence thesis by A1,GROUP_2:73;
end;
theorem Th25:
for G being strict finite Group holds G is p-group &
expon (G,p) = 1 implies G is cyclic
proof
let G be strict finite Group;
assume G is p-group & expon (G,p) = 1;
then card G = p |^ 1 by Def2
.= p;
hence thesis by GR_CY_1:21;
end;
theorem
for G being finite Group,p being Prime
for a being Element of G holds G is p-group & expon (G,p) = 2 &
ord a = p |^2 implies G is commutative
proof
let G be finite Group;
let p be Prime;
let a be Element of G;
assume that
A1: G is p-group & expon (G,p) = 2 and
A2: ord a = p |^2;
card G = p |^2 by A1,Def2;
then G is cyclic by A2,GR_CY_1:19;
hence thesis;
end;
begin :: Commutative $p$-Groups
definition
let p be Nat;
let G be Group;
attr G is p-commutative-group-like means
:Def3:
for a,b be Element of G holds (a * b) |^ p = a |^ p * (b |^ p);
end;
definition
let p be Nat;
let G be Group;
attr G is p-commutative-group means
G is p-group p-commutative-group-like;
end;
registration
let p be Nat;
cluster p-commutative-group -> p-group p-commutative-group-like for Group;
coherence;
cluster p-group p-commutative-group-like -> p-commutative-group for Group;
coherence;
end;
theorem Th27:
(1).G is p-commutative-group-like
proof
let a,b be Element of (1).G;
A1: the carrier of (1).G = {1_G} by GROUP_2:def 7;
hence (a * b) |^ p = 1_G by TARSKI:def 1
.= a |^ p * (b |^ p) by A1,TARSKI:def 1;
end;
registration
let p;
cluster p-commutative-group finite cyclic commutative for Group;
existence
proof
take (1).the Group;
(1).the Group is p-commutative-group-like p-group by Th16,Th27;
hence thesis;
end;
end;
registration
let p;
let G be p-commutative-group-like finite Group;
cluster -> p-commutative-group-like for Subgroup of G;
coherence
proof
let H be Subgroup of G;
let a,b be Element of H;
reconsider a2 = a, b2 = b as Element of G by GROUP_2:42;
A1: a * b = a2 * b2 by GROUP_8:2;
A2:a |^ p = a2 |^ p & b |^ p = b2 |^ p by GROUP_8:4;
thus (a * b) |^ p = (a2 * b2) |^ p by A1,GROUP_8:4
.= a2 |^ p * (b2 |^ p) by Def3
.= a |^ p * (b |^ p) by A2,GROUP_8:2;
end;
end;
registration
let p;
cluster p-group finite commutative -> p-commutative-group for Group;
coherence
proof
let G be Group such that
A1: G is p-group finite commutative;
for a,b being Element of G holds (a * b) |^ p = a |^ p * (b |^ p)
by A1,GROUP_1:48;
then G is p-commutative-group-like;
hence thesis by A1;
end;
end;
theorem
for G being strict finite Group st card G = p holds
G is p-commutative-group
proof
let G be strict finite Group;
assume
A1: card G = p;
p = p |^1; then
A2: G is p-group by A1;
G is cyclic Group by A1,GR_CY_1:21;
hence thesis by A2;
end;
registration
let p,G;
cluster p-commutative-group finite for Subgroup of G;
existence
proof
take (1).G;
(1).G is p-commutative-group-like p-group by Th16,Th27;
hence thesis;
end;
end;
registration
let p;
let G be finite Group, H1 be p-commutative-group-like Subgroup of G,
H2 be Subgroup of G;
cluster H1 /\ H2 -> p-commutative-group-like;
coherence
proof
reconsider H = H1 /\ H2 as Subgroup of H1 by GROUP_2:88;
H is p-commutative-group-like;
hence thesis;
end;
cluster H2 /\ H1 -> p-commutative-group-like;
coherence;
end;
registration
let p;
let G be finite p-commutative-group-like Group,
N be normal Subgroup of G;
cluster G./.N -> p-commutative-group-like;
coherence
proof
let S,T be Element of G./.N;
consider a be Element of G such that
A1: S = a * N & S = N * a by GROUP_6:21;
consider b be Element of G such that
A2: T = b * N & T = N * b by GROUP_6:21;
A3: S * T = @ S * @ T by GROUP_6:19
.=(a * b) * N by A1,A2,GROUP_11:1;
set c = a * b;
A4: (S * T) |^ p = (c |^ p) * N by A3,Th8
.= (a |^ p * (b |^ p))* N by Def3
.= ((a |^ p) * N) * ((b |^ p) * N) by GROUP_11:1;
A5: S |^ p = (a |^ p) * N by A1,Th8;
T |^ p = (b |^ p) * N by A2,Th8;
hence thesis by A4,A5,GROUP_6:def 3;
end;
end;
theorem
for G being finite Group,a,b being Element of G st
G is p-commutative-group-like
holds for n holds (a * b) |^ (p |^n) = a |^ (p |^n) * (b |^ (p |^n))
proof
let G be finite Group;
let a,b be Element of G;
assume
A1: G is p-commutative-group-like;
defpred P[Nat] means for n holds
(a * b) |^ (p |^ $1) = a |^ (p |^$1) * (b |^ (p |^$1));
A2: (a * b) |^ (p |^0) = (a * b) |^ 1 by NEWTON:4
.= a * b by GROUP_1:26;
a |^ (p |^0) * (b |^ (p |^0)) = a |^ 1 * (b |^ (p |^0)) by NEWTON:4
.= a * (b |^ (p |^0)) by GROUP_1:26
.= a * (b |^1) by NEWTON:4
.= a * b by GROUP_1:26;
then
A3: P[0] by A2;
A4: now
let n;
assume
A5: P[n];
set a1 = a |^ (p |^n), b1 = b |^ (p |^n);
(a * b) |^ (p |^ (n + 1)) = (a * b) |^ (p |^ n * p) by NEWTON:6
.= ((a * b) |^ (p |^ n)) |^ p by GROUP_1:35
.= (a |^ (p |^n) * (b |^ (p |^n))) |^ p by A5
.= a1 |^ p * (b1 |^ p) by A1
.= a |^ ((p |^n) * p) * (b |^ (p |^n) |^ p) by GROUP_1:35
.= a |^ ((p |^n) * p) * (b |^ ((p |^n) * p)) by GROUP_1:35
.= a |^ (p |^(n +1)) * (b |^ ((p |^n) * p)) by NEWTON:6
.= a |^ (p |^(n +1)) * (b |^ (p |^(n +1))) by NEWTON:6;
hence P[n+1];
end;
for n holds P[n] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem
for G being finite commutative Group,H,H1,H2 being Subgroup of G st
H1 is p-commutative-group & H2 is p-commutative-group &
the carrier of H = H1 * H2 holds H is p-commutative-group
proof
let G be finite commutative Group;
let H,H1,H2 be Subgroup of G;
assume that
A1: H1 is p-commutative-group &
H2 is p-commutative-group and
A2: the carrier of H = H1 * H2;
H is p-group by A1,A2,Th19;
hence thesis;
end;
theorem
for G being finite Group, H being Subgroup of G,
N being strict normal Subgroup of G holds
N is Subgroup of center G &
H is p-commutative-group &
N is p-commutative-group implies
ex P being strict Subgroup of G st the carrier of P = H * N &
P is p-commutative-group
proof
let G be finite Group;
let H be Subgroup of G;
let N be strict normal Subgroup of G;
assume that
A1: N is Subgroup of center G and
A2: H is p-commutative-group & N is p-commutative-group;
consider P be strict Subgroup of G such that
A3: the carrier of P = H * N & P is p-group by A2,Th20;
set P1 = P;
for a,b being Element of P holds (a * b) |^ p = a |^ p * (b |^ p)
proof
let a,b be Element of P;
A4: a in H * N & b in H * N by A3;
then consider a1,a2 be Element of G such that
A5: a = a1 * a2 & a1 in H & a2 in N by GROUP_11:6;
A6: a2 in center G by A1,A5,GROUP_2:40;
consider b1,b2 be Element of G such that
A7: b = b1 * b2 & b1 in H & b2 in N by A4,GROUP_11:6;
A8: b2 in center G by A1,A7,GROUP_2:40;
then a2 * b2 in center G & b2 * a2 in center G by A6,GROUP_2:50;
then
A9: (a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1) by GROUP_5:77;
reconsider c1 = a1,d1 = b1 as Element of H by A5,A7;
A10: a1 |^ p = c1 |^ p & b1 |^ p = d1 |^ p by GROUP_4:2;
a1 * b1 = c1 * d1 by GROUP_2:43; then
A11: (a1 * b1) |^ p = (c1 * d1) |^ p by GROUP_8:4
.= c1 |^ p * (d1 |^ p) by A2,Def3
.= a1 |^ p * (b1 |^ p) by A10,GROUP_2:43;
reconsider c2 = a2,d2 = b2 as Element of N by A5,A7;
A12: a2 |^ p = c2 |^ p & b2 |^ p = d2 |^ p by GROUP_4:2;
b2 * a2 = d2 * c2 by GROUP_2:43; then
A13: (b2 * a2) |^ p = (d2 * c2) |^ p by GROUP_8:4
.= d2 |^ p * (c2 |^ p) by A2,Def3
.= b2 |^ p * (a2 |^ p) by A12,GROUP_2:43;
A14: a2 |^ p in center G by A6,GROUP_4:4;
A15: a1 * a2 = a2 * a1 by A6,GROUP_5:77;
A16: b1 * b2 = b2 * b1 by A8,GROUP_5:77;
a * b = (a1 * a2) * (b1 * b2) by A5,A7,GROUP_2:43; then
A17: (a * b) |^ p = (a1 * a2 * (b1 * b2))|^ p by GROUP_8:4
.= (a1 * (a2 * (b1 * b2)))|^ p by GROUP_1:def 3
.= (a1 * ((b1 * b2) * a2))|^ p by A6,GROUP_5:77
.= (a1 * (b1 * (b2 * a2)))|^ p by GROUP_1:def 3
.= ((a1 * b1) * (b2 * a2))|^ p by GROUP_1:def 3
.= (a1 * b1)|^ p * ((b2 * a2)|^ p) by A9,GROUP_1:38
.= a1 |^ p * (b1 |^ p) * (a2 |^ p * (b2 |^ p)) by A11,A13,A14,
GROUP_5:77
.= a1 |^ p * (b1 |^ p * (a2 |^ p * (b2 |^ p))) by GROUP_1:def 3
.= a1 |^ p * ((b1 |^ p * (a2 |^ p)) * (b2 |^ p)) by GROUP_1:def 3
.= a1 |^ p * ((a2 |^ p * (b1 |^ p)) * (b2 |^ p)) by A14,GROUP_5:77
.= (a1 |^ p * (a2 |^ p * (b1 |^ p))) * (b2 |^ p) by GROUP_1:def 3
.= (a1 |^ p * (a2 |^ p) * (b1 |^ p)) * (b2 |^ p) by GROUP_1:def 3
.= (a1 |^ p * (a2 |^ p)) * (b1 |^ p * (b2 |^ p)) by GROUP_1:def 3
.= (a1 * a2)|^ p * (b1 |^ p * (b2 |^ p)) by A15,GROUP_1:38
.= (a1 * a2)|^ p * ((b1 * b2) |^ p) by A16,GROUP_1:38;
A18: a |^ p = (a1 * a2)|^ p by A5,GROUP_4:2;
b |^ p = (b1 * b2)|^ p by A7,GROUP_4:2;
hence thesis by A17,A18,GROUP_2:43;
end;
then P1 is p-commutative-group-like;
hence thesis by A3;
end;
theorem
for G being finite Group,N1,N2 being normal Subgroup of G holds
N2 is Subgroup of center G & N1 is p-commutative-group &
N2 is p-commutative-group implies
ex N being strict normal Subgroup of G
st the carrier of N = N1 * N2 & N is p-commutative-group
proof
let G be finite Group;
let N1,N2 be normal Subgroup of G;
assume that
A1: N2 is Subgroup of center G and
A2: N1 is p-commutative-group & N2 is p-commutative-group;
consider N be strict normal Subgroup of G such that
A3: the carrier of N = N1 * N2 & N is p-group by A2,Th21;
for a,b being Element of N holds (a * b) |^ p = a |^ p * (b |^ p)
proof
let a,b be Element of N;
A4: a in N1 * N2 & b in N1 * N2 by A3;
then consider a1,a2 be Element of G such that
A5: a = a1 * a2 & a1 in N1 & a2 in N2 by GROUP_11:6;
A6: a2 in center G by A1,A5,GROUP_2:40;
consider b1,b2 be Element of G such that
A7: b = b1 * b2 & b1 in N1 & b2 in N2 by A4,GROUP_11:6;
A8: b2 in center G by A1,A7,GROUP_2:40;
then a2 * b2 in center G & b2 * a2 in center G by A6,GROUP_2:50;
then
A9: (a1 * b1) * (b2 * a2) = (b2 * a2) * (a1 * b1) by GROUP_5:77;
reconsider c1 = a1,d1 = b1 as Element of N1 by A5,A7;
A10: a1 |^ p = c1 |^ p & b1 |^ p = d1 |^ p by GROUP_4:2;
a1 * b1 = c1 * d1 by GROUP_2:43; then
A11: (a1 * b1) |^ p = (c1 * d1) |^ p by GROUP_8:4
.= c1 |^ p * (d1 |^ p) by A2,Def3
.= a1 |^ p * (b1 |^ p) by A10,GROUP_2:43;
reconsider c2 = a2,d2 = b2 as Element of N2 by A5,A7;
A12: a2 |^ p = c2 |^ p & b2 |^ p = d2 |^ p by GROUP_4:2;
b2 * a2 = d2 * c2 by GROUP_2:43; then
A13: (b2 * a2) |^ p = (d2 * c2) |^ p by GROUP_8:4
.= d2 |^ p * (c2 |^ p) by A2,Def3
.= b2 |^ p * (a2 |^ p) by A12,GROUP_2:43;
A14: a2 |^ p in center G by A6,GROUP_4:4;
A15: a1 * a2 = a2 * a1 by A6,GROUP_5:77;
A16: b1 * b2 = b2 * b1 by A8,GROUP_5:77;
a * b = (a1 * a2) * (b1 * b2) by A5,A7,GROUP_2:43; then
A17: (a * b) |^ p = (a1 * a2 * (b1 * b2))|^ p by GROUP_8:4
.= (a1 * (a2 * (b1 * b2)))|^ p by GROUP_1:def 3
.= (a1 * ((b1 * b2) * a2))|^ p by A6,GROUP_5:77
.= (a1 * (b1 * (b2 * a2)))|^ p by GROUP_1:def 3
.= ((a1 * b1) * (b2 * a2))|^ p by GROUP_1:def 3
.= (a1 * b1)|^ p * ((b2 * a2)|^ p) by A9,GROUP_1:38
.= a1 |^ p * (b1 |^ p) * (a2 |^ p * (b2 |^ p)) by A11,A13,A14,
GROUP_5:77
.= a1 |^ p * (b1 |^ p * (a2 |^ p * (b2 |^ p))) by GROUP_1:def 3
.= a1 |^ p * ((b1 |^ p * (a2 |^ p)) * (b2 |^ p)) by GROUP_1:def 3
.= a1 |^ p * ((a2 |^ p * (b1 |^ p)) * (b2 |^ p)) by A14,GROUP_5:77
.= (a1 |^ p * (a2 |^ p * (b1 |^ p))) * (b2 |^ p) by GROUP_1:def 3
.= (a1 |^ p * (a2 |^ p) * (b1 |^ p)) * (b2 |^ p) by GROUP_1:def 3
.= (a1 |^ p * (a2 |^ p)) * (b1 |^ p * (b2 |^ p)) by GROUP_1:def 3
.= (a1 * a2)|^ p * (b1 |^ p * (b2 |^ p)) by A15,GROUP_1:38
.= (a1 * a2)|^ p * ((b1 * b2) |^ p) by A16,GROUP_1:38;
A18: a |^ p = (a1 * a2)|^ p by A5,GROUP_4:2;
b |^ p = (b1 * b2)|^ p by A7,GROUP_4:2;
hence thesis by A17,A18,GROUP_2:43;
end;
then N is p-commutative-group-like;
hence thesis by A3;
end;
theorem Th33:
for G,H being Group holds G,H are_isomorphic &
G is p-commutative-group-like implies H is p-commutative-group-like
proof
let G,H be Group;
assume that
A1: G,H are_isomorphic and
A2: G is p-commutative-group-like;
let h1,h2 be Element of H;
consider h being Homomorphism of G,H such that
A3: h is bijective by A1;
consider a be Element of G such that
A4: h.a = h1 by A3,GROUP_6:58;
consider b be Element of G such that
A5: h.b = h2 by A3,GROUP_6:58;
h1 * h2 = h.(a * b) by A4,A5,GROUP_6:def 6;
then (h1 * h2) |^ p = h.((a * b) |^ p) by GROUP_6:37
.= h.(a |^ p * (b |^ p)) by A2
.= h.(a |^ p) * h.(b |^ p) by GROUP_6:def 6
.= (h.a) |^ p * h.(b |^ p) by GROUP_6:37
.= h1 |^ p * (h2 |^ p) by A4,A5,GROUP_6:37;
hence thesis;
end;
theorem
for G,H being strict Group holds G,H are_isomorphic &
G is p-commutative-group implies H is p-commutative-group
by Th22,Th33;
registration
let p;
let G be p-commutative-group-like finite Group, H be finite Group;
let g be Homomorphism of G,H;
cluster Image g -> p-commutative-group-like;
coherence
proof
let g1,g2 be Element of Image g;
reconsider h1 = g1,h2 = g2 as Element of H by GROUP_2:42;
g1 in Image g;
then consider a be Element of G such that
A1: g1 = g.a by GROUP_6:45;
g2 in Image g;
then consider b be Element of G such that
A2: g2 = g.b by GROUP_6:45;
g1 * g2 = h1 * h2 by GROUP_2:43
.= g.(a * b) by A1,A2,GROUP_6:def 6; then
A3: (g1 * g2) |^ p = (g.(a * b)) |^ p by GROUP_8:4
.= g.((a * b)|^ p) by GROUP_6:37
.= g.(a |^ p * (b |^ p)) by Def3
.= g.(a |^ p) * g.(b |^ p) by GROUP_6:def 6
.= g.(a) |^ p * g.(b |^ p) by GROUP_6:37
.= h1 |^ p * (h2 |^ p) by A1,A2,GROUP_6:37;
h1 |^ p = g1 |^ p & h2 |^ p = g2 |^ p by GROUP_8:4;
hence thesis by A3,GROUP_2:43;
end;
end;
theorem
for G being strict finite Group st G is p-group &
expon (G,p) = 0 holds G is p-commutative-group
proof
let G be strict finite Group;
assume
A1:G is p-group & expon (G,p) = 0;
then G = (1).G by Th24;
hence thesis by A1;
end;
theorem
for G being strict finite Group st G is p-group &
expon (G,p) = 1 holds G is p-commutative-group
proof
let G be strict finite Group;
assume
A1: G is p-group & expon (G,p) = 1;
then G is cyclic by Th25;
hence thesis by A1;
end;