(* 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