:: The Sylow Theorems :: by Marco Riccardi :: :: Received August 13, 2007 :: Copyright (c) 2007-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 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);