Theory Secondary_Sylow.SndSylow
theory SndSylow
imports SubgroupConjugation
begin
no_notation Multiset.subset_mset (infix "<#" 50)
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
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
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)
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 .
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