Theory 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' = G⦇carrier := 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. λU∈rcosets 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 "∀h∈H. φ h N = N" unfolding H'act.stabilizer_def using H'_def by auto
  with HG Ncoset have a1:"∀h∈H. 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 (rcosets⇘G⦇carrier := group_action.stabilizer G (conjugation_action (p ^ a)) P⦈⇙ P) * 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 "G⦇carrier := conj.stabilizer P⦈" by (metis conj.stabilizer_is_subgroup subgroup_imp_group)
  from finite_G Psize have PStab:"subgroup P (G⦇carrier := 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 (rcosets⇘G⦇carrier := conj.stabilizer P⦈⇙ P) * card P = order (G⦇carrier := 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 (rcosets⇘G⦇carrier := conj.stabilizer P⦈⇙ P)"
  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 (G⦇carrier := P⦈) p a ((card P) div (p ^ a))"
proof -
  from subgrp interpret groupP: group "G⦇carrier := 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 (G⦇carrier := 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 (G⦇carrier := P⦈) ∧ card s = p ^ a}"
  define PRelM where "PRelM = {(N1, N2). N1 ∈ PcalM ∧ N2 ∈ PcalM ∧ (∃g∈carrier (G⦇carrier := P⦈). N1 = N2 #>⇘G⦇carrier := P⦈⇙ g)}"
  from subgrp finite_G have finite_groupP:"finite (carrier (G⦇carrier := P⦈))" by (auto simp:subgroup_finite)
  interpret Nsylow: snd_sylow "G⦇carrier := 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 (G⦇carrier := 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 "(G⦇carrier := 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 "G⦇carrier := 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 "G⦇carrier := N⦈" by (metis subgroup_imp_group)
      from Qsize N_def have QN:"subgroup Q (G⦇carrier := N⦈)" using stabilizer_supergrp_P by auto
      ― ‹The following proposition is used to show that $P = Q$ later›
      from Qsize have NfixesQ:"∀g∈N. conjugation_action (p ^ a) g Q = Q" unfolding N_def conjG.stabilizer_def by auto
      from Qfixed have PfixesQ:"∀g∈P. 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 (G⦇carrier := N⦈)" by (metis conjG.stabilizer_is_subgroup is_group subgroup.subgroup_of_subset)
      with cardP have "p ^ a dvd order (G⦇carrier := 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 (G⦇carrier := 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 (G⦇carrier := N⦈) ∧ card s = p ^ a}"
      define NRelM where "NRelM = {(N1, N2). N1 ∈ NcalM ∧ N2 ∈ NcalM ∧ (∃g∈carrier (G⦇carrier := N⦈). N1 = N2 #>⇘G⦇carrier := N⦈⇙ g)}"
      interpret Nsylow: snd_sylow "G⦇carrier := 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 (G⦇carrier := N⦈)" "P = g <#⇘G⦇carrier := N⦈⇙ (Q #>⇘G⦇carrier := N⦈⇙ inv⇘G⦇carrier := N⦈⇙ g)" 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