Theory Secondary_Sylow.SndSylow

(*  Title:      Secondary Sylow Theorems
    Author:     Jakob von Raumer, Karlsruhe Institute of Technology
    Maintainer: Jakob von Raumer <jakob.raumer at student.kit.edu>
*)

theory SndSylow
imports SubgroupConjugation
begin

no_notation Multiset.subset_mset  (infix "<#" 50) (*prevent a clash with the same syntax for l_coset*)

section ‹The Secondary Sylow Theorems›

subsection ‹Preliminaries›

lemma singletonI:
  assumes "x. x  A  x = y"
  assumes "y  A"
  shows "A = {y}"
using assms by fastforce

context group
begin

lemma set_mult_inclusion:
  assumes H:"subgroup H G"
  assumes Q:"P  carrier G"
  assumes PQ:"H <#> P  H"
  shows "P  H"
proof
  fix x
  from H have "𝟭  H" by (rule subgroup.one_closed)
  moreover assume x:"x  P"
  ultimately have "𝟭  x  H <#> P" unfolding set_mult_def by auto
  with PQ have "𝟭  x  H" by auto
  with H Q x show  "x  H" by (metis in_mono l_one)
qed

lemma card_subgrp_dvd:
  assumes "subgroup H G"
  shows "card H dvd order G"
proof(cases "finite (carrier G)")
  case True
  with assms have "card (rcosets H) * card H = order G" by (metis lagrange)
  thus ?thesis by (metis dvd_triv_left mult.commute)
next
  case False
  hence "order G = 0" unfolding order_def by (metis card.infinite)
  thus ?thesis by (metis dvd_0_right)
qed

lemma subgroup_finite:
  assumes subgroup:"subgroup H G"
  assumes finite:"finite (carrier G)"
  shows "finite H"
by (metis finite finite_subset subgroup subgroup.subset)

end

subsection ‹Extending the Sylow Locale›

text ‹This locale extends the originale @{term sylow} locale by adding
the constraint that the @{term p} must not divide the remainder @{term m},
i.e. @{term "p ^ a"} is the maximal size of a @{term p}-subgroup of
@{term G}.›

locale snd_sylow = sylow +
  assumes pNotDvdm:"¬ (p dvd m)"

context snd_sylow
begin

lemma pa_not_zero: "p ^ a  0"
  by (simp add: prime_gt_0_nat prime_p)

lemma sylow_greater_zero:
  shows "card (subgroups_of_size (p ^ a)) > 0"
proof -
  obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a" by (metis sylow_thm)
  hence "P  subgroups_of_size (p ^ a)" unfolding subgroups_of_size_def by auto
  hence "subgroups_of_size (p ^ a)  {}" by auto
  moreover from finite_G have "finite (subgroups_of_size (p ^ a))" unfolding subgroups_of_size_def subgroup_def by auto
  ultimately show ?thesis by auto
qed

lemma is_snd_sylow: "snd_sylow G p a m" by (rule snd_sylow_axioms)

subsection ‹Every $p$-group is Contained in a conjugate of a $p$-Sylow-Group›

lemma ex_conj_sylow_group:
  assumes H:"H  subgroups_of_size (p ^ b)"
  assumes Psize:"P  subgroups_of_size (p ^ a)"
  obtains g where "g  carrier G" "H  g <# (P #> inv g)"
proof -
  from H have HsubG:"subgroup H G" unfolding subgroups_of_size_def by auto
  hence HG:"H  carrier G" unfolding subgroups_of_size_def by (simp add:subgroup.subset)
  from Psize have PG:"subgroup P G" and cardP:"card P = p ^ a" unfolding subgroups_of_size_def by auto
  define H' where "H' = Gcarrier := H"
  from HsubG interpret Hgroup: group H' unfolding H'_def by (metis subgroup_imp_group)
  from H have orderH':"order H' =  p ^ b" unfolding H'_def subgroups_of_size_def order_def by simp
  define φ where "φ = (λg. λUrcosets P. U #> inv g)"
  with PG interpret Gact: group_action G φ "rcosets P" unfolding φ_def by (metis inv_mult_on_rcosets_action)
  from H interpret H'act: group_action H' φ "rcosets P" unfolding H'_def subgroups_of_size_def by (metis (mono_tags) Gact.subgroup_action mem_Collect_eq)
  from finite_G PG have "finite (rcosets P)" unfolding RCOSETS_def r_coset_def by (metis (lifting) finite.emptyI finite_UN_I finite_insert)
  with orderH' sylow_axioms cardP have "card H'act.fixed_points mod p = card (rcosets P) mod p" unfolding sylow_def sylow_axioms_def by (metis H'act.fixed_point_congruence)
  moreover from finite_G PG order_G cardP  have "card (rcosets P) * p ^ a  = p ^ a * m" by (metis lagrange)
  with prime_p have "card (rcosets P) = m" by (metis less_nat_zero_code mult_cancel2 mult_is_0 mult.commute order_G zero_less_o_G)
  hence "card (rcosets P) mod p = m mod p" by simp
  moreover from pNotDvdm prime_p have "...  0" by (metis dvd_eq_mod_eq_0)
  ultimately have "card H'act.fixed_points  0" by (metis mod_0)
  then obtain N where N:"N  H'act.fixed_points" by fastforce
  hence Ncoset:"N  rcosets P" unfolding H'act.fixed_points_def by simp
  then obtain g where g:"g  carrier G" "N = P #> g" unfolding RCOSETS_def by auto
  hence invg:"inv g  carrier G" by (metis inv_closed)
  hence invinvg:"inv (inv g)  carrier G" by (metis inv_closed)
  from N have "carrier H'  H'act.stabilizer N" unfolding H'act.fixed_points_def by simp
  hence "hH. φ h N = N" unfolding H'act.stabilizer_def using H'_def by auto
  with HG Ncoset have a1:"hH. N #> inv h  N" unfolding φ_def by simp
  have "N <#> H  N" unfolding set_mult_def r_coset_def
  proof(auto)
    fix n h
    assume n:"n  N" and h:"h  H"
    with H have "inv h  H" by (metis (mono_tags) mem_Collect_eq subgroup.m_inv_closed subgroups_of_size_def)
    with n HG PG a1 have "n  inv (inv h)  N" unfolding r_coset_def by auto
    with HG h show  "n  h  N" by (metis in_mono inv_inv)
  qed
  with g have "((P #> g) <#> H) #> inv g  (P #> g) #> inv g" unfolding r_coset_def by auto
  with PG g invg have "((P #> g) <#> H) #> inv g  P" by (metis coset_mult_assoc coset_mult_one r_inv subgroup.subset)
  with g HG PG invg have "P <#> (g <# H #> inv g)  P" by (metis lr_coset_assoc r_coset_subset_G rcos_assoc_lcos setmult_rcos_assoc subgroup.subset)
  with PG HG g invg have "g <# H #> inv g  P" by (metis l_coset_subset_G r_coset_subset_G set_mult_inclusion)
  with g have "(g <# H #> inv g) #> inv (inv g)  P #> inv (inv g)" unfolding r_coset_def by auto
  with HG g invg invinvg have "g <# H  P #> inv (inv g)" by (metis coset_mult_assoc coset_mult_inv2 l_coset_subset_G)
  with g have "(inv g) <# (g <# H)  inv g <# (P #> inv (inv g))" unfolding l_coset_def by auto
  with HG g invg invinvg have "H  inv g <# (P #> inv (inv g))" by (metis inv_inv lcos_m_assoc lcos_mult_one r_inv)
  with invg show thesis by (auto dest:that)
qed

subsection‹Every $p$-Group is Contained in a $p$-Sylow-Group›

theorem sylow_contained_in_sylow_group:
  assumes H:"H  subgroups_of_size (p ^ b)"
  obtains S where "H  S" and "S  subgroups_of_size (p ^ a)"
proof -
  from H have HG:"H  carrier G" unfolding subgroups_of_size_def by (simp add:subgroup.subset)
  obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a" by (metis sylow_thm)
  hence Psize:"P  subgroups_of_size (p ^ a)" unfolding subgroups_of_size_def by simp
  with H obtain g where g:"g  carrier G" "H  g <# (P #> inv g)" by (metis ex_conj_sylow_group)
  moreover note Psize g
  moreover with finite_G have "conjugation_action (p ^ a) g P  subgroups_of_size (p ^ a)" by (metis conjugation_is_size_invariant)
  ultimately show thesis unfolding conjugation_action_def by (auto dest:that)
qed

subsection‹$p$-Sylow-Groups are conjugates of each other›

theorem sylow_conjugate:
  assumes P:"P  subgroups_of_size (p ^ a)"
  assumes Q:"Q  subgroups_of_size (p ^ a)"
  obtains g where "g  carrier G" "Q = g <# (P #> inv g)"
proof -
  from P have "card P = p ^ a" unfolding subgroups_of_size_def by simp
  from Q have Qcard:"card Q = p ^ a" unfolding subgroups_of_size_def by simp
  from Q P obtain g where g:"g  carrier G" "Q  g <# (P #> inv g)" by (rule ex_conj_sylow_group)
  moreover with P finite_G have "conjugation_action (p ^ a) g P  subgroups_of_size (p ^ a)" by (metis conjugation_is_size_invariant)
  moreover from g P have "conjugation_action (p ^ a) g P = g <# (P #> inv g)" unfolding conjugation_action_def by simp
  ultimately have conjSize:"g <# (P #> inv g)  subgroups_of_size (p ^ a)" unfolding conjugation_action_def by simp
  with Qcard have  card:"card (g <# (P #> inv g)) = card Q"  unfolding subgroups_of_size_def by simp
  from conjSize finite_G have "finite (g <# (P #> inv g))" by (metis (mono_tags) finite_subset mem_Collect_eq subgroup.subset subgroups_of_size_def)
  with g card have "Q = g <# (P #> inv g)" by (metis card_subset_eq)
  with g show thesis by (metis that)
qed

corollary sylow_conj_orbit_rel:
  assumes P:"P  subgroups_of_size (p ^ a)"
  assumes Q:"Q  subgroups_of_size (p ^ a)"
  shows "(P,Q)  group_action.same_orbit_rel G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a))"
unfolding group_action.same_orbit_rel_def 
proof -
  from Q P obtain g where g:"g  carrier G" "P = g <# (Q #> inv g)" by (rule sylow_conjugate)
  with Q P have g':"conjugation_action (p ^ a) g Q = P" unfolding conjugation_action_def by simp
  from finite_G interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))" by (rule acts_on_subsets)
  have "conj.same_orbit_rel = {X  (subgroups_of_size (p ^ a) × subgroups_of_size (p ^ a)). g  carrier G. ((conjugation_action (p ^ a)) g) (snd X) = (fst X)}" by (rule conj.same_orbit_rel_def)
  with g g' P Q show ?thesis by auto
qed

subsection‹Counting Sylow-Groups›

text ‹The number of sylow groups is the orbit size of one of them:›

theorem num_eq_card_orbit:
  assumes P:"P  subgroups_of_size (p ^ a)"
  shows "subgroups_of_size (p ^ a) = group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P"
proof(auto)
  from finite_G interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))" by (rule acts_on_subsets)
  have "group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P = group_action.same_orbit_rel G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) `` {P}" by (rule conj.orbit_def)
  fix Q
  {
    assume Q:"Q  subgroups_of_size (p ^ a)"
    from P Q obtain g where g:"g  carrier G" "Q = g <# (P #> inv g) " by (rule sylow_conjugate)
    with P conj.orbit_char show "Q  group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P"
      unfolding conjugation_action_def by auto
  } {
    assume "Q  group_action.orbit G (conjugation_action (p ^ a)) (subgroups_of_size (p ^ a)) P"
    with P conj.orbit_char obtain g where g:"g  carrier G" "Q = conjugation_action (p ^ a) g P" by auto
    with finite_G P show "Q  subgroups_of_size (p ^ a)"  by (metis conjugation_is_size_invariant)
  }
qed

theorem num_sylow_normalizer:
  assumes Psize:"P  subgroups_of_size (p ^ a)"
  shows "card (rcosetsGcarrier := group_action.stabilizer G (conjugation_action (p ^ a)) PP) * p ^ a = card (group_action.stabilizer G (conjugation_action (p ^ a)) P)"
proof -
  from finite_G interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))" by (rule acts_on_subsets)
  from Psize have PG:"subgroup P G" and cardP:"card P = p ^ a" unfolding subgroups_of_size_def by auto
  with finite_G have "order G = card (conj.orbit P) * card (conj.stabilizer P)" by (metis Psize acts_on_subsets group_action.orbit_size)
  with order_G Psize have "p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)" by (metis num_eq_card_orbit)
  moreover from Psize interpret stabGroup: group "Gcarrier := conj.stabilizer P" by (metis conj.stabilizer_is_subgroup subgroup_imp_group)
  from finite_G Psize have PStab:"subgroup P (Gcarrier := conj.stabilizer P)" by (rule stabilizer_supergrp_P)
  from finite_G Psize have "finite (conj.stabilizer P)" by (metis card.infinite conj.stabilizer_is_subgroup less_nat_zero_code subgroup.finite_imp_card_positive)
  with finite_G PStab stabGroup.lagrange have "card (rcosetsGcarrier := conj.stabilizer PP) * card P = order (Gcarrier := conj.stabilizer P)" by force
  with cardP show ?thesis unfolding order_def by auto 
qed

theorem (in snd_sylow) num_sylow_dvd_remainder:
  shows "card (subgroups_of_size (p ^ a)) dvd m"
proof -
  from finite_G interpret conj: group_action G "(conjugation_action (p ^ a))" "(subgroups_of_size (p ^ a))" by (rule acts_on_subsets)
  obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a" by (metis sylow_thm)
  hence Psize:"P  subgroups_of_size (p ^ a)" unfolding subgroups_of_size_def by simp
  with finite_G have "order G = card (conj.orbit P) * card (conj.stabilizer P)" by (metis Psize acts_on_subsets group_action.orbit_size)
  with order_G Psize have orderEq:"p ^ a * m = card (subgroups_of_size (p ^ a)) * card (conj.stabilizer P)" by (metis num_eq_card_orbit)
  define k where "k = card (rcosetsGcarrier := conj.stabilizer PP)"
  with Psize have "k * p ^ a = card (conj.stabilizer P)" by (metis num_sylow_normalizer)
  with orderEq have "p ^ a * m = card (subgroups_of_size (p ^ a)) * p ^ a * k" by (auto simp:mult.assoc mult.commute)
  hence "p ^ a * m = p ^ a * card (subgroups_of_size (p ^ a)) * k" by auto
  then have "m = card (subgroups_of_size (p ^ a)) * k"
    using pa_not_zero by auto
  then show ?thesis ..
qed

text ‹We can restrict this locale to refer to a subgroup of order at
least @{term "(p ^ a)"}:›

lemma (in snd_sylow) restrict_locale:
  assumes subgrp:"subgroup P G"
  assumes card:"p ^ a dvd card P"
  shows "snd_sylow (Gcarrier := P) p a ((card P) div (p ^ a))"
proof -
  from subgrp interpret groupP: group "Gcarrier := P" by (metis subgroup_imp_group)
  define k where "k = (card P) div (p ^ a)"
  with card have cardP:"card P = p ^ a * k" by auto
  hence orderP:"order (Gcarrier := P) = p ^ a * k" unfolding order_def by simp
  from cardP subgrp order_G have "p ^ a * k dvd p ^ a * m" by (metis card_subgrp_dvd)
  hence "k dvd m"
    by (metis nat_mult_dvd_cancel_disj pa_not_zero) 
  with pNotDvdm have ndvd:"¬ p dvd k"
    by (blast intro: dvd_trans)
  define PcalM where "PcalM = {s. s  carrier (Gcarrier := P)  card s = p ^ a}"
  define PRelM where "PRelM = {(N1, N2). N1  PcalM  N2  PcalM  (gcarrier (Gcarrier := P). N1 = N2 #>Gcarrier := Pg)}"
  from subgrp finite_G have finite_groupP:"finite (carrier (Gcarrier := P))" by (auto simp:subgroup_finite)
  interpret Nsylow: snd_sylow "Gcarrier := P" p a k PcalM PRelM
     unfolding snd_sylow_def snd_sylow_axioms_def sylow_def sylow_axioms_def k_def
     using groupP.is_group prime_p orderP finite_groupP ndvd PcalM_def PRelM_def k_def by fastforce+
  show ?thesis using k_def by (metis Nsylow.is_snd_sylow)
qed

theorem (in snd_sylow) p_sylow_mod_p:
  shows "card (subgroups_of_size (p ^ a)) mod p = 1"
proof -
  obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a" by (metis sylow_thm)
  hence orderP:"order (Gcarrier := P) = p ^ a" unfolding order_def by auto
  from PG have PsubG:"P  carrier G" by (metis subgroup.subset)
  from PG cardP have PSize:"P  subgroups_of_size (p ^ a)" unfolding subgroups_of_size_def by auto
  from PG interpret groupP:group "(Gcarrier := P)" by (rule subgroup_imp_group)
  from cardP have PSize2:"P  groupP.subgroups_of_size (p ^ a)" using groupP.subgroups_of_size_def groupP.subgroup_self by auto
  from finite_G interpret conjG: group_action G "conjugation_action (p ^ a)" "subgroups_of_size (p ^ a)" by (rule acts_on_subsets)
  from PG interpret conjP: group_action "Gcarrier := P" "conjugation_action (p ^ a)" "subgroups_of_size (p ^ a)" by (rule conjG.subgroup_action)
  from finite_G have "finite (subgroups_of_size (p ^ a))" unfolding subgroups_of_size_def subgroup_def by auto
  with orderP prime_p have "card (subgroups_of_size (p ^ a)) mod p = card conjP.fixed_points mod p" by (rule conjP.fixed_point_congruence)
  also have "... = 1"
  proof -
    have "Q. Q  conjP.fixed_points  Q = P"
    proof -
      fix Q
      assume Qfixed:"Q  conjP.fixed_points"
      hence Qsize:"Q  subgroups_of_size (p ^ a)" unfolding conjP.fixed_points_def by simp
      hence cardQ:"card Q = p ^ a" unfolding subgroups_of_size_def by simp
      ― ‹The normalizer of @{term Q} in @{term G}
      ― ‹Let's first show some basic propertiers of @{text N}
      define N where "N = conjG.stabilizer Q"
      define k where "k = (card N) div (p ^ a)"
      from N_def Qsize have NG:"subgroup N G" by (metis conjG.stabilizer_is_subgroup)
      then interpret groupN: group "Gcarrier := N" by (metis subgroup_imp_group)
      from Qsize N_def have QN:"subgroup Q (Gcarrier := N)" using stabilizer_supergrp_P by auto
      ― ‹The following proposition is used to show that $P = Q$ later›
      from Qsize have NfixesQ:"gN. conjugation_action (p ^ a) g Q = Q" unfolding N_def conjG.stabilizer_def by auto
      from Qfixed have PfixesQ:"gP. conjugation_action (p ^ a) g Q = Q" unfolding conjP.fixed_points_def conjP.stabilizer_def by auto
      with PsubG have  "P  N" unfolding N_def conjG.stabilizer_def by auto
      with PG N_def Qsize have PN:"subgroup P (Gcarrier := N)" by (metis conjG.stabilizer_is_subgroup is_group subgroup.subgroup_of_subset)
      with cardP have "p ^ a dvd order (Gcarrier := N)" using groupN.card_subgrp_dvd by force
      hence "p ^ a dvd card N" unfolding order_def by simp
      with NG have smaller_sylow:"snd_sylow (Gcarrier := N) p a k" unfolding k_def by (rule restrict_locale)
      ― ‹Instantiate the @{term snd_sylow} Locale a second time for the normalizer of @{term Q}
      define NcalM where "NcalM = {s. s  carrier (Gcarrier := N)  card s = p ^ a}"
      define NRelM where "NRelM = {(N1, N2). N1  NcalM  N2  NcalM  (gcarrier (Gcarrier := N). N1 = N2 #>Gcarrier := Ng)}"
      interpret Nsylow: snd_sylow "Gcarrier := N" p a k NcalM NRelM
        unfolding NcalM_def NRelM_def using smaller_sylow .
      ― ‹@{term P} and @{term Q} are conjugate in @{term N}:›
      from cardP PN have PsizeN:"P  groupN.subgroups_of_size (p ^ a)" unfolding groupN.subgroups_of_size_def by auto
      from cardQ QN have QsizeN:"Q  groupN.subgroups_of_size (p ^ a)" unfolding groupN.subgroups_of_size_def by auto
      from QsizeN PsizeN obtain g where g:"g  carrier (Gcarrier := N)" "P = g <#Gcarrier := N(Q #>Gcarrier := NinvGcarrier := Ng)" by (rule Nsylow.sylow_conjugate)
      with NG have "P = g <# (Q #> inv g)" unfolding r_coset_def l_coset_def by (auto simp:m_inv_consistent)
      with NG g Qsize have "conjugation_action (p ^ a) g Q = P" unfolding conjugation_action_def using subgroup.subset by force
      with g NfixesQ show "Q = P" by auto
    qed
    moreover from finite_G PSize have "P  conjP.fixed_points" using P_fixed_point_of_P_conj by auto
    ultimately have "conjP.fixed_points = {P}" by fastforce
    hence one:"card conjP.fixed_points = 1" by (auto simp: card_Suc_eq)
    with prime_p have "card conjP.fixed_points < p" unfolding prime_nat_iff by auto
    with one show ?thesis using mod_pos_pos_trivial by auto
  qed
  finally show ?thesis.
qed

end

end