:: The Sylow Theorems
:: by Marco Riccardi
::
:: Received August 13, 2007
:: Copyright (c) 2007-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 NUMBERS, XBOOLE_0, STRUCT_0, GROUP_9, SUBSET_1, ORDINAL4,
FUNCT_1, RELAT_1, TARSKI, GROUP_1, ALGSTR_0, ZFMISC_1, FUNCT_2, BINOP_1,
SETFAM_1, CARD_1, FINSET_1, ORDINAL1, CARD_FIN, GROUP_2, EQREL_1, INT_2,
NEWTON, INT_1, XXREAL_0, ARYTM_3, FINSEQ_1, NAT_1, PARTFUN1, CQC_SIM1,
CARD_3, FUNCOP_1, FINSEQ_2, NAT_3, GR_CY_1, BINOP_2, XCMPLX_0, ARYTM_1,
RLSUB_1, GROUP_4, GRAPH_1, GROUP_3, REALSET1, GROUP_10, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, ZFMISC_1, XXREAL_0, XREAL_0, INT_2, NAT_1, NAT_D, FINSET_1,
RELAT_1, REALSET1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_2,
RVSUM_1, STRUCT_0, ALGSTR_0, GROUP_1, GROUP_2, GROUP_3, EQREL_1,
FUNCOP_1, WSIERP_1, NEWTON, DOMAIN_1, GR_CY_1, GROUP_4, CARD_FIN,
PARTFUN1, NAT_3, TOPGRP_1;
constructors WELLORD2, NAT_D, BINARITH, WSIERP_1, REALSET2, GR_CY_1, GROUP_4,
CARD_FIN, NAT_3, TOPGRP_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, NEWTON, STRUCT_0,
GROUP_2, GROUP_1, GROUP_3, GR_CY_1, FUNCT_2, NAT_3, REALSET1, VALUED_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Group Operating on a Set
notation
let S be non empty 1-sorted;
let E be set;
let A be Action of (the carrier of S), E;
let s be Element of S;
synonym A^s for A.s;
end;
definition
let S be non empty 1-sorted;
let E be set;
let A be Action of (the carrier of S), E;
let s be Element of S;
redefine func A^s -> Function of E, E;
end;
definition
let S be unital non empty multMagma;
let E be set;
let A be Action of (the carrier of S), E;
attr A is being_left_operation means
:: GROUP_10:def 1
A^(1_S) = id E &
for s1,s2 being Element of S holds A^(s1*s2) = A^s1 * (A^s2);
end;
registration
let S be unital non empty multMagma;
let E be set;
cluster being_left_operation for Action of (the carrier of S), E;
end;
:: ALG I.5.1 DEF 1
definition
let S be unital non empty multMagma;
let E be set;
mode LeftOperation of S, E is
being_left_operation Action of (the carrier of S), E;
end;
scheme :: GROUP_10:sch 1
ExLeftOperation {E()->set, S()->Group-like non empty multMagma, f(Element
of S())->Function of E(),E()}: ex T being LeftOperation of S(), E() st for s
being Element of S() holds T.s = f(s)
provided
f(1_S()) = id E() and
for s1,s2 being Element of S() holds f(s1*s2) = f(s1) * f(s2);
registration
let E be non empty set, S be Group-like non empty multMagma,
s be Element of S, LO be LeftOperation of S, E;
cluster LO^s -> one-to-one for Function of E,E;
end;
:: left translation
:: ALG I.3.1
notation
let S be non empty multMagma;
let s be Element of S;
synonym the_left_translation_of s for s*;
end;
definition
let S be Group-like associative non empty multMagma;
func the_left_operation_of S -> LeftOperation of S, the carrier of S means
:: GROUP_10:def 2
for s being Element of S holds it.s = the_left_translation_of s;
end;
definition
let E be set;
let n be set;
func the_subsets_of_card(n, E) -> Subset-Family of E equals
:: GROUP_10:def 3
{X where X is Subset of E: card X = n};
end;
registration
let E be finite set;
let n be set;
cluster the_subsets_of_card(n, E) -> finite;
end;
theorem :: GROUP_10:1
for n being Nat, E being non empty set st card n c=
card E holds the_subsets_of_card(n, E) is non empty;
theorem :: GROUP_10:2
for E being non empty finite set, k being Element of NAT, x1,x2
being set st x1<>x2 holds card Choose(E,k,x1,x2) = card the_subsets_of_card(k,E
);
definition
let E be non empty set;
let n be Nat;
let S be Group-like non empty multMagma;
let s be Element of S;
let LO be LeftOperation of S, E;
assume
card n c= card E;
func the_extension_of_left_translation_of(n,s,LO) -> Function of
the_subsets_of_card(n, E), the_subsets_of_card(n, E) means
:: GROUP_10:def 4
for X being Element of the_subsets_of_card(n, E) holds it.X = (LO^s) .: X;
end;
definition
let E be non empty set;
let n be Nat;
let S be Group-like non empty multMagma;
let LO be LeftOperation of S, E;
assume
card n c= card E;
func the_extension_of_left_operation_of(n,LO) -> LeftOperation of S,
the_subsets_of_card(n, E) means
:: GROUP_10:def 5
for s being Element of S holds it.s =
the_extension_of_left_translation_of(n,s,LO);
end;
definition
let S be non empty multMagma;
let s be Element of S;
let Z be non empty set;
func the_left_translation_of(s,Z) -> Function of [:the carrier of S,Z:],[:
the carrier of S,Z:] means
:: GROUP_10:def 6
for z1 being Element of [:the carrier of S,Z
:] holds ex z2 being Element of [:the carrier of S,Z:], s1,s2 being Element of
S, z being Element of Z st z2 = it.z1 & s2 = s * s1 & z1=[s1,z] & z2=[s2,z];
end;
definition
let S be Group-like associative non empty multMagma;
let Z be non empty set;
func the_left_operation_of(S,Z) -> LeftOperation of S,[:the carrier of S,Z:]
means
:: GROUP_10:def 7
for s being Element of S holds it.s = the_left_translation_of(s,Z);
end;
definition
let G be Group;
let H,P be Subgroup of G;
let h be Element of H;
func the_left_translation_of(h,P) -> Function of Left_Cosets P, Left_Cosets
P means
:: GROUP_10:def 8
for P1 being Element of Left_Cosets P holds ex P2 being Element
of Left_Cosets P, A1,A2 being Subset of G, g being Element of G st P2 = it.P1 &
A2 = g * A1 & A1=P1 & A2=P2 & g=h;
end;
definition
let G be Group;
let H,P be Subgroup of G;
func the_left_operation_of(H,P) -> LeftOperation of H, Left_Cosets P means
:: GROUP_10:def 9
for h being Element of H holds it.h = the_left_translation_of(h,P);
end;
begin :: Stabilizer and Orbits
:: stabilizer
:: ALG I.5.2 Definition 3
definition
let G be Group;
let E be non empty set;
let T be LeftOperation of G,E;
let A be Subset of E;
func the_strict_stabilizer_of(A,T) -> strict Subgroup of G means
:: GROUP_10:def 10
the carrier of it = {g where g is Element of G: (T^g) .: A = A};
end;
definition
let G be Group;
let E be non empty set;
let T be LeftOperation of G,E;
let x be Element of E;
func the_strict_stabilizer_of(x,T) -> strict Subgroup of G equals
:: GROUP_10:def 11
the_strict_stabilizer_of({x},T);
end;
definition
let S be unital non empty multMagma;
let E be set;
let T be LeftOperation of S, E;
let x be Element of E;
pred x is_fixed_under T means
:: GROUP_10:def 12
for s being Element of S holds x = (T^s).x;
end;
definition
let S be unital non empty multMagma;
let E be set;
let T be LeftOperation of S, E;
func the_fixed_points_of T -> Subset of E equals
:: GROUP_10:def 13
{x where x is
Element of E: x is_fixed_under T} if E is non empty otherwise {}E;
end;
:: ALG I.5.4 Definition 5
definition
let S be unital non empty multMagma;
let E be set;
let T be LeftOperation of S, E;
let x,y be Element of E;
pred x,y are_conjugated_under T means
:: GROUP_10:def 14
ex s being Element of S st y = (T^s).x;
end;
theorem :: GROUP_10:3
for S being unital non empty multMagma, E being non empty set,
x being Element of E, T being LeftOperation of S, E holds x,x
are_conjugated_under T;
theorem :: GROUP_10:4
for G being Group, E being non empty set, x,y being Element of E,
T being LeftOperation of G, E st x,y are_conjugated_under T holds y,x
are_conjugated_under T;
theorem :: GROUP_10:5
for S being unital non empty multMagma, E being non empty set,
x,y,z being Element of E, T being LeftOperation of S, E st x,y
are_conjugated_under T & y,z are_conjugated_under T holds x,z
are_conjugated_under T;
definition
let S be unital non empty multMagma;
let E be non empty set;
let T be LeftOperation of S, E;
let x be Element of E;
func the_orbit_of(x,T) -> Subset of E equals
:: GROUP_10:def 15
{y where y is Element of E: x,y
are_conjugated_under T};
end;
registration
let S be unital non empty multMagma, E be non empty set,
x be Element of E, T be LeftOperation of S, E;
cluster the_orbit_of(x,T) -> non empty;
end;
theorem :: GROUP_10:6
for G being Group, E being non empty set, x,y being Element of E,
T being LeftOperation of G, E holds the_orbit_of(x,T) misses the_orbit_of(y,T)
or the_orbit_of(x,T)=the_orbit_of(y,T);
theorem :: GROUP_10:7
for S being unital non empty multMagma, E being non empty
finite set, x being Element of E, T being LeftOperation of S, E st x
is_fixed_under T holds the_orbit_of(x,T) = {x};
:: the orbit-stabilizer theorem
theorem :: GROUP_10:8
for G being Group, E being non empty set, a being Element of E,
T being LeftOperation of G, E holds card the_orbit_of(a,T) = Index
the_strict_stabilizer_of(a,T);
definition
let G be Group;
let E be non empty set;
let T be LeftOperation of G, E;
func the_orbits_of T -> a_partition of E equals
:: GROUP_10:def 16
{X where X is Subset of E:
ex x being Element of E st X = the_orbit_of(x,T)};
end;
begin :: p-groups
:: ALG I.6.5 Definition 9
definition
let p be Nat;
let G be Group;
attr G is p-group means
:: GROUP_10:def 17
ex r being Nat st card G = p |^ r;
end;
registration
let p be non zero Nat;
cluster INT.Group(p) -> p-group;
end;
registration
let p be non zero Nat;
cluster p-group finite cyclic commutative strict for Group;
end;
:: like WEDDWITT:39
:: ALG I.6.5 PRO 11
theorem :: GROUP_10:9
for E being non empty finite set, G being finite Group,
p being prime Nat, T being LeftOperation of G, E st
G is p-group
holds card the_fixed_points_of T mod p = card E mod p;
begin :: The Sylow Theorems
:: ALG I.6.6 Definition 10
definition
let p be Nat;
let G be Group;
let P be Subgroup of G;
pred P is_Sylow_p-subgroup_of_prime p means
:: GROUP_10:def 18
P is p-group & not p divides index P;
end;
:: ALG I.6.6 Theorem 2
:: The first Sylow theorem
::$N First Sylow Theorem
theorem :: GROUP_10:10
for G being finite Group, p being prime Nat ex P
being strict Subgroup of G st P is_Sylow_p-subgroup_of_prime p;
:: ALG I.6.6 Corollary
:: The Cauchy theorem
theorem :: GROUP_10:11
for G being finite Group, p being prime Nat st p divides
card G ex g being Element of G st ord g = p;
:: ALG I.6.6 Theorem 3
:: The second Sylow theorem
::$N Second Sylow Theorem
theorem :: GROUP_10:12
for G being finite Group, p being prime Nat holds (
for H being Subgroup of G st H is p-group holds ex P being Subgroup
of G st P is_Sylow_p-subgroup_of_prime p & H is Subgroup of P) & (for P1,P2
being Subgroup of G st P1 is_Sylow_p-subgroup_of_prime p & P2
is_Sylow_p-subgroup_of_prime p holds P1,P2 are_conjugated);
definition
let G be Group;
let p be Nat;
func the_sylow_p-subgroups_of_prime(p,G) -> Subset of Subgroups G equals
:: GROUP_10:def 19
{H where H is Element of Subgroups G: ex P being strict Subgroup of G st
P = H & P is_Sylow_p-subgroup_of_prime p};
end;
registration
let G be finite Group;
let p be prime Nat;
cluster the_sylow_p-subgroups_of_prime(p,G) -> non empty finite;
end;
definition
let G be finite Group;
let p be prime Nat;
let H be Subgroup of G;
let h be Element of H;
func the_left_translation_of(h,p) -> Function of
the_sylow_p-subgroups_of_prime(p,G), the_sylow_p-subgroups_of_prime(p,G) means
:: GROUP_10:def 20
for P1 being Element of the_sylow_p-subgroups_of_prime(p,G) holds ex P2
being Element of the_sylow_p-subgroups_of_prime(p,G), H1,H2 being strict
Subgroup of G, g being Element of G st P2 = it.P1 & P1=H1 & P2=H2 & h"=g & H2 =
H1 |^ g;
end;
definition
let G be finite Group;
let p be prime Nat;
let H be Subgroup of G;
func the_left_operation_of(H,p) -> LeftOperation of H,
the_sylow_p-subgroups_of_prime(p,G) means
:: GROUP_10:def 21
for h being Element of H holds it.h = the_left_translation_of(h,p);
end;
:: ALG I.6.6 Theorem 3
:: The third Sylow theorem
::$N Third Sylow Theorem
theorem :: GROUP_10:13
for G being finite Group, p being prime Nat holds card
the_sylow_p-subgroups_of_prime(p,G) mod p = 1 & card
the_sylow_p-subgroups_of_prime(p,G) divides card G;
begin :: Appendix
theorem :: GROUP_10:14
for X,Y being non empty set holds card the set of all
[:X,{y}:] where y is Element
of Y = card Y;
theorem :: GROUP_10:15
for n,m,r being Nat, p being prime Nat st n =
p |^ r * m & not p divides m holds (n choose p|^r) mod p <> 0;
theorem :: GROUP_10:16
for n being non zero Nat holds card INT.Group(n) = n;
theorem :: GROUP_10:17
for G being Group, A being non empty Subset of G, g being Element of G
holds card A = card (A * g);