:: 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);