(* Title: Subgroup Conjugation Author: Jakob von Raumer, Karlsruhe Institute of Technology Maintainer: Jakob von Raumer <jakob.raumer at student.kit.edu> *) theory SubgroupConjugation imports GroupAction begin section ‹Conjugation of Subgroups and Cosets› text ‹This theory examines properties of the conjugation of subgroups of a fixed group as a group action› subsection ‹Definitions and Preliminaries› text ‹We define the set of all subgroups of @{term G} which have a certain cardinality. @{term G} will act on those sets. Afterwards some theorems which are already available for right cosets are dualized into statements about left cosets.› lemma (in subgroup) subgroup_of_subset: assumes G:"group G" assumes PH:"H ⊆ K" assumes KG:"subgroup K G" shows "subgroup H (G⦇carrier := K⦈)" using assms subgroup_def group.m_inv_consistent m_inv_closed by fastforce context group begin definition subgroups_of_size ::"nat ⇒ _" where "subgroups_of_size p = {H. subgroup H G ∧ card H = p}" lemma lcosI: "[| h ∈ H; H ⊆ carrier G; x ∈ carrier G|] ==> x ⊗ h ∈ x <# H" by (auto simp add: l_coset_def) lemma lcoset_join2: assumes H:"subgroup H G" assumes g:"g ∈ H" shows "g <# H = H" proof auto fix x assume x:"x ∈ g <# H" then obtain h where h:"h ∈ H" "x = g ⊗ h" unfolding l_coset_def by auto with g H show "x ∈ H" by (metis subgroup.m_closed) next fix x assume x:"x ∈ H" with g H have "inv g ⊗ x ∈ H" by (metis subgroup.m_closed subgroup.m_inv_closed) with x g H show "x ∈ g <# H" by (metis is_group subgroup.lcos_module_rev subgroup.mem_carrier) qed lemma cardeq_rcoset: assumes "finite (carrier G)" assumes "M ⊆ carrier G" assumes "g ∈ carrier G" shows "card (M #> g) = card M" proof - have "M #> g ∈ rcosets M" by (metis assms(2) assms(3) rcosetsI) thus "card (M #> g) = card M" using assms(2) card_rcosets_equal by auto qed lemma cardeq_lcoset: assumes "finite (carrier G)" assumes M:"M ⊆ carrier G" assumes g:"g ∈ carrier G" shows "card (g <# M) = card M" proof - have "bij_betw (λm. g ⊗ m) M (g <# M)" proof(auto simp add: bij_betw_def) show "inj_on ((⊗) g) M" proof(rule inj_onI) from g have invg:"inv g ∈ carrier G" by (rule inv_closed) fix x y assume x:"x ∈ M" and y:"y ∈ M" with M have xG:"x ∈ carrier G" and yG:"y ∈ carrier G" by auto assume "g ⊗ x = g ⊗ y" hence "(inv g) ⊗ (g ⊗ x) = (inv g) ⊗ (g ⊗ y)" by simp with g invg xG yG have "(inv g ⊗ g) ⊗ x = (inv g ⊗ g) ⊗ y" by (metis m_assoc) with g invg xG yG show "x = y" by simp qed next fix x assume "x ∈ M" thus "g ⊗ x ∈ g <# M" unfolding l_coset_def by auto next fix x assume x:"x ∈ g <# M" then obtain m where "x = g ⊗ m" "m ∈ M" unfolding l_coset_def by auto thus "x ∈ (⊗) g ` M" by simp qed thus "card (g <# M) = card M" by (metis bij_betw_same_card) qed subsection ‹Conjugation is a group action› text ‹We will now prove that conjugation acts on the subgroups of a certain group. A large part of this proof consists of showing that the conjugation of a subgroup with a group element is, again, a subgroup.› lemma conjugation_subgroup: assumes HG:"subgroup H G" assumes gG:"g ∈ carrier G" shows "subgroup (g <# (H #> inv g)) G" proof from gG have "inv g ∈ carrier G" by (rule inv_closed) with HG have "(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset) with gG show "g <# (H #> inv g) ⊆ carrier G" by (metis l_coset_subset_G) next from gG have invgG:"inv g ∈ carrier G" by (metis inv_closed) with HG have lcosSubset:"(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset) fix x y assume x:"x ∈ g <# (H #> inv g)" and y:"y ∈ g <# (H #> inv g)" then obtain x' y' where x':"x' ∈ H #> inv g" "x = g ⊗ x'" and y':"y' ∈ H #> inv g" "y = g ⊗ y'" unfolding l_coset_def by auto then obtain hx hy where hx:"hx ∈ H" "x' = hx ⊗ inv g" and hy:"hy ∈ H" "y' = hy ⊗ inv g" unfolding r_coset_def by auto with x' y' have x2:"x = g ⊗ (hx ⊗ inv g)" and y2:"y = g ⊗ (hy ⊗ inv g)" by auto hence "x ⊗ y = (g ⊗ (hx ⊗ inv g)) ⊗ (g ⊗ (hy ⊗ inv g))" by simp also from hx hy HG have hxG:"hx ∈ carrier G" and hyG:"hy ∈ carrier G" by (metis subgroup.mem_carrier)+ with gG hy x2 invgG have "(g ⊗ (hx ⊗ inv g)) ⊗ (g ⊗ (hy ⊗ inv g)) = g ⊗ hx ⊗ (inv g ⊗ g) ⊗ hy ⊗ inv g" by (metis m_assoc m_closed) also from invgG gG have "... = g ⊗ hx ⊗ 𝟭 ⊗ hy ⊗ inv g" by simp also from gG hxG have "... = g ⊗ hx ⊗ hy ⊗ inv g" by (metis m_closed r_one) also from gG hxG invgG have "... = g ⊗ ((hx ⊗ hy) ⊗ inv g)" by (metis gG hxG hyG invgG m_assoc m_closed) finally have xy:"x ⊗ y = g ⊗ (hx ⊗ hy ⊗ inv g)". from hx hy HG have "hx ⊗ hy ∈ H" by (metis subgroup.m_closed) with invgG HG have "(hx ⊗ hy) ⊗ inv g ∈ H #> inv g" by (metis rcosI subgroup.subset) with gG lcosSubset have "g ⊗ (hx ⊗ hy ⊗ inv g) ∈ g <# (H #> inv g)" by (metis lcosI) with xy show "x ⊗ y ∈ g <# (H #> inv g)" by simp next from gG have invgG:"inv g ∈ carrier G" by (metis inv_closed) with HG have lcosSubset:"(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset) from HG have "𝟭 ∈ H" by (rule subgroup.one_closed) with invgG HG have "𝟭 ⊗ inv g ∈ H #> inv g" by (metis rcosI subgroup.subset) with gG lcosSubset have "g ⊗ (𝟭 ⊗ inv g) ∈ g <# (H #> inv g)" by (metis lcosI) with gG invgG show "𝟭 ∈ g <# (H #> inv g)" by simp next from gG have invgG:"inv g ∈ carrier G" by (metis inv_closed) with HG have lcosSubset:"(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset) fix x assume "x ∈ g <# (H #> inv g)" then obtain x' where x':"x' ∈ H #> inv g" "x = g ⊗ x'" unfolding l_coset_def by auto then obtain hx where hx:"hx ∈ H" "x' = hx ⊗ inv g" unfolding r_coset_def by auto with HG have invhx:"inv hx ∈ H" by (metis subgroup.m_inv_closed) from x' hx have "inv x = inv (g ⊗ (hx ⊗ inv g))" by simp also from x' hx HG gG invgG have "... = inv (inv g) ⊗ inv hx ⊗ inv g" by (metis calculation in_mono inv_mult_group lcosSubset subgroup.mem_carrier) also from gG have "... = g ⊗ inv hx ⊗ inv g" by simp also from gG invgG invhx HG have "... = g ⊗ (inv hx ⊗ inv g)" by (metis m_assoc subgroup.mem_carrier) finally have invx:"inv x = g ⊗ (inv hx ⊗ inv g)". with invhx invgG HG have "(inv hx) ⊗ inv g ∈ H #> inv g" by (metis rcosI subgroup.subset) with gG lcosSubset have "g ⊗ (inv hx ⊗ inv g) ∈ g <# (H #> inv g)" by (metis lcosI) with invx show "inv x ∈ g <# (H #> inv g)" by simp qed definition conjugation_action::"nat ⇒ _" where "conjugation_action p = (λg∈carrier G. λP∈subgroups_of_size p. g <# (P #> inv g))" lemma conjugation_is_size_invariant: assumes fin:"finite (carrier G)" assumes P:"P ∈ subgroups_of_size p" assumes g:"g ∈ carrier G" shows "conjugation_action p g P ∈ subgroups_of_size p" proof - from g have invg:"inv g ∈ carrier G" by (metis inv_closed) from P have PG:"subgroup P G" and card:"card P = p" unfolding subgroups_of_size_def by simp+ hence PsubG:"P ⊆ carrier G" by (metis subgroup.subset) hence PinvgsubG:"P #> inv g ⊆ carrier G" by (metis invg r_coset_subset_G) have " g <# (P #> inv g) ∈ subgroups_of_size p" proof(auto simp add:subgroups_of_size_def) show "subgroup (g <# (P #> inv g)) G" by (metis g PG conjugation_subgroup) next from card PsubG fin invg have "card (P #> inv g) = p" by (metis cardeq_rcoset) with g PinvgsubG fin show "card (g <# (P #> inv g)) = p" by (metis cardeq_lcoset) qed with P g show ?thesis unfolding conjugation_action_def by simp qed lemma conjugation_is_Bij: assumes fin:"finite (carrier G)" assumes g:"g ∈ carrier G" shows "conjugation_action p g ∈ Bij (subgroups_of_size p)" proof - from g have invg:"inv g ∈ carrier G" by (rule inv_closed) from g have "conjugation_action p g ∈ extensional (subgroups_of_size p)" unfolding conjugation_action_def by simp moreover have "bij_betw (conjugation_action p g) (subgroups_of_size p) (subgroups_of_size p)" proof(auto simp add:bij_betw_def) show "inj_on (conjugation_action p g) (subgroups_of_size p)" proof(rule inj_onI) fix U V assume U:"U ∈ subgroups_of_size p" and V:"V ∈ subgroups_of_size p" hence subsetG:"U ⊆ carrier G" "V ⊆ carrier G" unfolding subgroups_of_size_def by (metis (lifting) mem_Collect_eq subgroup.subset)+ hence subsetL:"U #> inv g ⊆ carrier G" "V #> inv g ⊆ carrier G" by (metis invg r_coset_subset_G)+ assume "conjugation_action p g U = conjugation_action p g V" with g U V have "g <# (U #> inv g) = g <# (V #> inv g)" unfolding conjugation_action_def by simp hence "(inv g) <# (g <# (U #> inv g)) = (inv g) <# (g <# (V #> inv g))" by simp hence "(inv g ⊗ g) <# (U #> inv g) = (inv g ⊗ g) <# (V #> inv g)" by (metis g invg lcos_m_assoc r_coset_subset_G subsetG) hence "𝟭 <# (U #> inv g) = 𝟭 <# (V #> inv g)" by (metis g l_inv) hence "U #> inv g = V #> inv g" by (metis subsetL lcos_mult_one) hence "(U #> inv g) #> g = (V #> inv g) #> g" by simp hence "U #> (inv g ⊗ g) = V #> (inv g ⊗ g)" by (metis coset_mult_assoc g inv_closed subsetG) hence "U #> 𝟭 = V #> 𝟭" by (metis g l_inv) thus "U = V" by (metis coset_mult_one subsetG) qed next fix P assume "P ∈ subgroups_of_size p" thus "conjugation_action p g P ∈ subgroups_of_size p" by (metis fin g conjugation_is_size_invariant) next fix P assume P:"P ∈ subgroups_of_size p" with invg have "conjugation_action p (inv g) P ∈ subgroups_of_size p" by (metis fin invg conjugation_is_size_invariant) with invg P have "(inv g) <# (P #> (inv (inv g))) ∈ subgroups_of_size p" unfolding conjugation_action_def by simp hence 1:"(inv g) <# (P #> g) ∈ subgroups_of_size p" by (metis g inv_inv) have "g <# (((inv g) <# (P #> g)) #> inv g) = (⋃p ∈ P. {g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g)})" unfolding r_coset_def l_coset_def by (simp add:m_assoc) also from P have PG:"P ⊆ carrier G" unfolding subgroups_of_size_def by (auto simp add:subgroup.subset) have "∀p ∈ P. g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g) = p" proof(auto) fix p assume "p ∈ P" with PG have p:"p ∈ carrier G".. with g invg have "g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g) = (g ⊗ inv g) ⊗ p ⊗ (g ⊗ inv g)" by (metis m_assoc m_closed) also with g invg g p have "... = p" by (metis l_one r_inv r_one) finally show "g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g) = p". qed hence "(⋃p ∈ P. {g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g)}) = P" by simp finally have "g <# (((inv g) <# (P #> g)) #> inv g) = P". with 1 have "P ∈ (λP. g <# (P #> inv g)) ` subgroups_of_size p" by auto with P g show "P ∈ conjugation_action p g ` subgroups_of_size p" unfolding conjugation_action_def by simp qed ultimately show ?thesis unfolding BijGroup_def Bij_def by simp qed lemma lr_coset_assoc: assumes g:"g ∈ carrier G" assumes h:"h ∈ carrier G" assumes P:"P ⊆ carrier G" shows "g <# (P #> h) = (g <# P) #> h" proof(auto) fix x assume "x ∈ g <# (P #> h)" then obtain p where "p ∈ P" and p:"x = g ⊗ (p ⊗ h)" unfolding l_coset_def r_coset_def by auto with P have "p ∈ carrier G" by auto with g h p have "x = (g ⊗ p) ⊗ h" by (metis m_assoc) with ‹p ∈ P› show "x ∈ (g <# P) #> h" unfolding l_coset_def r_coset_def by auto next fix x assume "x ∈ (g <# P) #> h" then obtain p where "p ∈ P" and p:"x = (g ⊗ p) ⊗ h" unfolding l_coset_def r_coset_def by auto with P have "p ∈ carrier G" by auto with g h p have "x = g ⊗ (p ⊗ h)" by (metis m_assoc) with ‹p ∈ P› show "x ∈ g <# (P #> h)" unfolding l_coset_def r_coset_def by auto qed theorem acts_on_subsets: assumes fin:"finite (carrier G)" shows "group_action G (conjugation_action p) (subgroups_of_size p)" unfolding group_action_def group_action_axioms_def group_hom_def group_hom_axioms_def hom_def apply(auto simp add:is_group group_BijGroup) proof - fix g assume g:"g ∈ carrier G" with fin show "conjugation_action p g ∈ carrier (BijGroup (subgroups_of_size p))" unfolding BijGroup_def by (metis conjugation_is_Bij partial_object.select_convs(1)) next fix x y assume x:"x ∈ carrier G" and y:"y ∈ carrier G" hence invx:"inv x ∈ carrier G" and invy:"inv y ∈ carrier G" by (metis inv_closed)+ from x y have xyG:"x ⊗ y ∈ carrier G" by (metis m_closed) define conjx where "conjx = conjugation_action p x" define conjy where "conjy = conjugation_action p y" from fin x have xBij:"conjx ∈ Bij (subgroups_of_size p)" unfolding conjx_def by (metis conjugation_is_Bij) from fin y have yBij:"conjy ∈ Bij (subgroups_of_size p)" unfolding conjy_def by (metis conjugation_is_Bij) have "conjx ⊗⇘BijGroup (subgroups_of_size p)⇙ conjy = (λg∈Bij (subgroups_of_size p). restrict (compose (subgroups_of_size p) g) (Bij (subgroups_of_size p))) conjx conjy" unfolding BijGroup_def by simp also from xBij yBij have "... = compose (subgroups_of_size p) conjx conjy" by simp also have "... = (λP∈subgroups_of_size p. conjx (conjy P))" by (metis compose_def) also have "... = (λP∈subgroups_of_size p. x ⊗ y <# (P #> inv (x ⊗ y)))" proof(rule restrict_ext) fix P assume P:"P ∈ subgroups_of_size p" hence PG:"P ⊆ carrier G" unfolding subgroups_of_size_def by (auto simp:subgroup.subset) with y have yPG:"y <# P ⊆ carrier G" by (metis l_coset_subset_G) from x y have invxyG:"inv (x ⊗ y) ∈ carrier G" and xyG:"x ⊗ y ∈ carrier G" using inv_closed m_closed by auto from yBij have "conjy ` subgroups_of_size p = subgroups_of_size p" unfolding Bij_def bij_betw_def by simp with P have conjyP:"conjy P ∈ subgroups_of_size p" unfolding Bij_def bij_betw_def by (metis (full_types) imageI) with x y P have "conjx (conjy P) = x <# ((y <# (P #> inv y)) #> inv x)" unfolding conjy_def conjx_def conjugation_action_def by simp also from y invy PG have "... = x <# (((y <# P) #> inv y) #> inv x)" by (metis lr_coset_assoc) also from PG invx invy y have "... = x <# ((y <# P) #> (inv y ⊗ inv x))" by (metis coset_mult_assoc yPG) also from x y have "... = x <# ((y <# P) #> inv (x ⊗ y))" by (metis inv_mult_group) also from invxyG x yPG have "... = (x <# (y <# P)) #> inv (x ⊗ y)" by (metis lr_coset_assoc) also from x y PG have "... = ((x ⊗ y) <# P) #> inv (x ⊗ y)" by (metis lcos_m_assoc) also from xyG invxyG PG have "... = (x ⊗ y) <# (P #> inv (x ⊗ y))" by (metis lr_coset_assoc) finally show "conjx (conjy P) = x ⊗ y <# (P #> inv (x ⊗ y))". qed finally have "conjx ⊗⇘BijGroup (subgroups_of_size p)⇙ conjy = (λP∈subgroups_of_size p. x ⊗ y <# (P #> inv (x ⊗ y)))". with xyG show "conjugation_action p (x ⊗ y) = conjugation_action p x ⊗⇘BijGroup (subgroups_of_size p)⇙ conjugation_action p y" unfolding conjx_def conjy_def conjugation_action_def by simp qed subsection ‹Properties of the Conjugation Action› lemma stabilizer_contains_P: assumes fin:"finite (carrier G)" assumes P:"P ∈ subgroups_of_size p" shows "P ⊆ group_action.stabilizer G (conjugation_action p) P" proof from P have PG:"subgroup P G" unfolding subgroups_of_size_def by simp from fin interpret conj:group_action G "(conjugation_action p)" "(subgroups_of_size p)" by (rule acts_on_subsets) fix x assume x:"x ∈ P" with PG have "inv x ∈ P" by (metis subgroup.m_inv_closed) from x P have xG:"x ∈ carrier G" unfolding subgroups_of_size_def subgroup_def by auto with P have "conjugation_action p x P = x <# (P #> inv x)" unfolding conjugation_action_def by simp also from ‹inv x ∈ P› PG have "... = x <# P" by (metis coset_join2 subgroup.mem_carrier) also from PG x have "... = P" by (rule lcoset_join2) finally have "conjugation_action p x P = P". with xG show "x ∈ group_action.stabilizer G (conjugation_action p) P" unfolding conj.stabilizer_def by simp qed corollary stabilizer_supergrp_P: assumes fin:"finite (carrier G)" assumes P:"P ∈ subgroups_of_size p" shows "subgroup P (G⦇carrier := group_action.stabilizer G (conjugation_action p) P⦈)" proof - from assms have "P ⊆ group_action.stabilizer G (conjugation_action p) P" by (rule stabilizer_contains_P) moreover from P have "subgroup P G" unfolding subgroups_of_size_def by simp moreover from P fin have "subgroup (group_action.stabilizer G (conjugation_action p) P) G" by (metis acts_on_subsets group_action.stabilizer_is_subgroup) ultimately show ?thesis by (metis is_group subgroup.subgroup_of_subset) qed lemma (in group) P_fixed_point_of_P_conj: assumes fin:"finite (carrier G)" assumes P:"P ∈ subgroups_of_size p" shows "P ∈ group_action.fixed_points (G⦇carrier := P⦈) (conjugation_action p) (subgroups_of_size p)" proof - from fin interpret conjG: group_action G "conjugation_action p" "subgroups_of_size p" by (rule acts_on_subsets) from P have "subgroup P G" unfolding subgroups_of_size_def by simp with fin interpret conjP: group_action "G⦇carrier := P⦈" "(conjugation_action p)" "(subgroups_of_size p)" by (metis acts_on_subsets group_action.subgroup_action) from fin P have "P ⊆ conjG.stabilizer P" by (rule stabilizer_contains_P) hence "P ⊆ conjP.stabilizer P" using conjG.stabilizer_def conjP.stabilizer_def by auto with P show "P ∈ conjP.fixed_points" unfolding conjP.fixed_points_def by auto qed lemma conj_wo_inv: assumes QG:"subgroup Q G" assumes PG:"subgroup P G" assumes g:"g ∈ carrier G" assumes conj:"inv g <# (Q #> g) = P" shows "Q #> g = g <# P" proof - from g have invg:"inv g ∈ carrier G" by (metis inv_closed) from conj have "g <# (inv g <# (Q #> g)) = g <# P" by simp with QG g invg have "(g ⊗ inv g) <# (Q #> g) = g <# P" by (metis lcos_m_assoc r_coset_subset_G subgroup.subset) with g invg have "𝟭 <# (Q #> g) = g <# P" by (metis r_inv) with QG g show "Q #> g = g <# P" by (metis lcos_mult_one r_coset_subset_G subgroup.subset) qed end end