:: Some Properties of $p$-Groups and Commutative $p$-Groups
:: by Xiquan Liang and Dailu Li
::
:: Received April 29, 2010
:: Copyright (c) 2010-2016 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;
begin :: $p$-Groups
reserve G for Group,
a,b for Element of G,
m, n for Nat,
p for prime Nat;
theorem :: GROUPP_1:1
(for r being Nat holds n <> p |^ r) implies
ex s being Element of NAT st s is prime & s divides n & s <> p;
theorem :: GROUPP_1:2
for n,m being Nat holds n divides p |^ m implies
ex r be Nat st n = p |^ r & r <= m;
theorem :: GROUPP_1:3
a |^ n = 1_G implies a" |^ n = 1_G;
theorem :: GROUPP_1:4
a" |^ n = 1_G implies a |^ n = 1_G;
theorem :: GROUPP_1:5
ord (a") = ord a;
theorem :: GROUPP_1:6
ord (a |^ b) = ord a;
theorem :: GROUPP_1:7
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;
theorem :: GROUPP_1:8
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;
theorem :: GROUPP_1:9
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;
theorem :: GROUPP_1:10
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;
theorem :: GROUPP_1:11
for G being finite Group, N being normal Subgroup of G holds
N = center G & G./.N is cyclic implies G is commutative;
theorem :: GROUPP_1:12
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;
definition
let p be Nat;
let G be Group;
let a be Element of G;
attr a is p-power means
:: GROUPP_1:def 1
ex r being Nat st ord a = p |^ r;
end;
theorem :: GROUPP_1:13
1_G is m-power;
registration
let G,m;
cluster m-power for Element of G;
end;
registration
let p,G;
let a be p-power Element of G;
cluster a" -> p-power;
end;
theorem :: GROUPP_1:14
a |^ b is p-power implies a is p-power;
registration
let p,G,b;
let a be p-power Element of G;
cluster a |^ b -> p-power;
end;
registration
let p;
let G be commutative Group, a,b be p-power Element of G;
cluster a * b -> p-power;
end;
registration
let p;
let G be finite p-group Group;
cluster -> p-power for Element of G;
end;
theorem :: GROUPP_1:15
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;
registration
let p;
let G be finite p-group Group;
cluster -> p-group for Subgroup of G;
end;
theorem :: GROUPP_1:16
(1).G is p-group;
registration
let p;
let G be Group;
cluster p-group for Subgroup of G;
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;
cluster G2 /\ G1 -> p-group;
end;
theorem :: GROUPP_1:17
for G being finite Group st for a being Element of G holds a is p-power
holds G is p-group;
registration
let p;
let G be finite p-group Group, N being normal Subgroup of G;
cluster G./.N -> p-group;
end;
theorem :: GROUPP_1:18
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;
theorem :: GROUPP_1:19
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;
theorem :: GROUPP_1:20
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;
theorem :: GROUPP_1:21
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;
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;
end;
theorem :: GROUPP_1:22
for G,H being strict Group holds G,H are_isomorphic &
G is p-group implies H is p-group;
definition
let p be prime Nat;
let G be Group such that
G is p-group;
func expon (G,p) -> Nat means
:: GROUPP_1:def 2
card G = p |^ it;
end;
definition
let p be prime Nat;
let G be Group;
redefine func expon (G,p) -> Element of NAT;
end;
theorem :: GROUPP_1:23
for G being finite Group, H being Subgroup of G st
G is p-group holds expon (H,p) <= expon (G,p);
theorem :: GROUPP_1:24
for G being strict finite Group st G is p-group & expon (G,p) = 0 holds
G = (1).G;
theorem :: GROUPP_1:25
for G being strict finite Group holds G is p-group &
expon (G,p) = 1 implies G is cyclic;
theorem :: GROUPP_1:26
for G being finite Group,p being prime Nat
for a being Element of G holds G is p-group & expon (G,p) = 2 &
ord a = p |^2 implies G is commutative;
begin :: Commutative $p$-Groups
definition
let p be Nat;
let G be Group;
attr G is p-commutative-group-like means
:: GROUPP_1:def 3
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
:: GROUPP_1:def 4
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;
cluster p-group p-commutative-group-like -> p-commutative-group for Group;
end;
theorem :: GROUPP_1:27
(1).G is p-commutative-group-like;
registration
let p;
cluster p-commutative-group finite cyclic commutative for Group;
end;
registration
let p;
let G be p-commutative-group-like finite Group;
cluster -> p-commutative-group-like for Subgroup of G;
end;
registration
let p;
cluster p-group finite commutative -> p-commutative-group for Group;
end;
theorem :: GROUPP_1:28
for G being strict finite Group st card G = p holds
G is p-commutative-group;
registration
let p,G;
cluster p-commutative-group finite for Subgroup of G;
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;
cluster H2 /\ H1 -> p-commutative-group-like;
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;
end;
theorem :: GROUPP_1:29
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));
theorem :: GROUPP_1:30
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;
theorem :: GROUPP_1:31
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;
theorem :: GROUPP_1:32
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;
theorem :: GROUPP_1:33
for G,H being Group holds G,H are_isomorphic &
G is p-commutative-group-like implies H is p-commutative-group-like;
theorem :: GROUPP_1:34
for G,H being strict Group holds G,H are_isomorphic &
G is p-commutative-group implies H is p-commutative-group;
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;
end;
theorem :: GROUPP_1:35
for G being strict finite Group st G is p-group &
expon (G,p) = 0 holds G is p-commutative-group;
theorem :: GROUPP_1:36
for G being strict finite Group st G is p-group &
expon (G,p) = 1 holds G is p-commutative-group;