(* Title: Group Actions Author: Jakob von Raumer, Karlsruhe Institute of Technology Maintainer: Jakob von Raumer <jakob.raumer at student.kit.edu> *) theory GroupAction imports "HOL-Algebra.Bij" "HOL-Algebra.Sylow" begin section ‹Group Actions› text ‹This is an implemention of group actions based on the group implementation of HOL-Algebra. An action a group $G$ on a set $M$ is represented by a group homomorphism between $G$ and the group of bijections on $M$› subsection ‹Preliminaries and Definition› text ‹First, we need two theorems about singletons and sets of singletons which unfortunately are not included in the library.› theorem singleton_intersection: assumes A:"card A = 1" assumes B:"card B = 1" assumes noteq:"A ≠ B" shows "A ∩ B = {}" using assms by(auto simp:card_Suc_eq) theorem card_singleton_set: assumes cardOne:"∀x ∈ A.(card x = 1)" shows "card (⋃A) = card A" proof - have "card (⋃A) = (∑x∈A. card x)" proof(rule card_Union_disjoint) from cardOne show "⋀a. a∈A ⟹ finite a" by (auto intro: card_ge_0_finite) next show "pairwise disjnt A" unfolding pairwise_def disjnt_def proof(clarify) fix x y assume x:"x ∈ A" and y:"y ∈ A" and "x ≠ y" with cardOne have "card x = 1" "card y = 1" by auto with ‹x ≠ y› show "x ∩ y = {}" by (metis singleton_intersection) qed qed also from cardOne have "... = card A" by simp finally show ?thesis. qed text ‹Intersecting Cosets are equal:› lemma (in subgroup) repr_independence2: assumes group:"group G" assumes U:"U ∈ rcosets⇘G⇙ H" assumes g:"g ∈ U" shows "U = H #> g" proof - from U obtain h where h:"h ∈ carrier G" "U = H #> h" unfolding RCOSETS_def by auto with g have "g ∈ H #> h" by simp with group h show "U = H #> g" by (metis group.repr_independence is_subgroup) qed locale group_action = group + fixes φ M assumes grouphom:"group_hom G (BijGroup M) φ" context group_action begin lemma is_group_action:"group_action G φ M".. text ‹The action of @{term "𝟭⇘G⇙"} has no effect:› lemma one_is_id: assumes "m ∈ M" shows "(φ 𝟭) m = m" proof - from grouphom have "(φ 𝟭) m = 𝟭⇘(BijGroup M)⇙ m" by (metis group_hom.hom_one) also have "... = (λx∈M. x) m" unfolding BijGroup_def by (metis monoid.select_convs(2)) also from assms have "... = m" by simp finally show ?thesis. qed lemma action_closed: assumes m:"m ∈ M" assumes g:"g ∈ carrier G" shows "φ g m ∈ M" using assms grouphom group_hom.hom_closed unfolding BijGroup_def Bij_def bij_betw_def by fastforce lemma img_in_bij: assumes "g ∈ carrier G" shows "(φ g) ∈ Bij M" using assms grouphom unfolding BijGroup_def by (auto dest: group_hom.hom_closed) text ‹The action of @{term "inv g"} reverts the action of @{term g}› lemma group_inv_rel: assumes g:"g ∈ carrier G" assumes mn:"m ∈ M" "n ∈ M" assumes phi:"(φ g) n = m" shows "(φ (inv g)) m = n" proof - from g have bij:"(φ g) ∈ Bij M" unfolding BijGroup_def by (metis img_in_bij) with g grouphom have "φ (inv g) = restrict (inv_into M (φ g)) M" by(metis inv_BijGroup group_hom.hom_inv) hence "φ (inv g) m = (restrict (inv_into M (φ g)) M) m" by simp also from mn have "... = (inv_into M (φ g)) m" by (metis restrict_def) also from g phi have "... = (inv_into M (φ g)) ((φ g) n)" by simp also from ‹φ g ∈ Bij M› Bij_def have "bij_betw (φ g) M M" by auto hence "inj_on (φ g) M" by (metis bij_betw_imp_inj_on) with g mn have "(inv_into M (φ g)) ((φ g) n) = n" by (metis inv_into_f_f) finally show "φ (inv g) m = n". qed lemma images_are_bij: assumes g:"g ∈ carrier G" shows "bij_betw (φ g) M M" proof - from g have bij:"(φ g) ∈ Bij M" unfolding BijGroup_def by (metis img_in_bij) with Bij_def show "bij_betw (φ g) M M" by auto qed lemma action_mult: assumes g:"g ∈ carrier G" assumes h:"h ∈ carrier G" assumes m:"m ∈ M" shows "(φ g) ((φ h) m) = (φ (g ⊗ h)) m" proof - from g have φg:"(φ g) ∈ Bij M" unfolding BijGroup_def by (rule img_in_bij) from h have φh:"(φ h) ∈ Bij M" unfolding BijGroup_def by (rule img_in_bij) from h have "bij_betw (φ h) M M" by (rule images_are_bij) hence "(φ h) ` M = M" by (metis bij_betw_def) with m have hm:"(φ h) m ∈ M" by (metis imageI) from grouphom g h have "(φ (g ⊗ h)) = ((φ g) ⊗⇘(BijGroup M)⇙ (φ h))" by (rule group_hom.hom_mult) hence "φ (g ⊗ h) m = ((φ g) ⊗⇘(BijGroup M)⇙ (φ h)) m" by simp also from φg φh have "... = (compose M (φ g) (φ h)) m" unfolding BijGroup_def by simp also from φg φh hm have "... = (φ g) ((φ h) m)" by (metis compose_eq m) finally show "(φ g) ((φ h) m) = (φ (g ⊗ h)) m".. qed subsection ‹The orbit relation› text ‹The following describes the relation containing the information whether two elements of @{term M} lie in the same orbit of the action› definition same_orbit_rel where "same_orbit_rel = {p ∈ M × M. ∃g ∈ carrier G. (φ g) (snd p) = (fst p)}" text ‹Use the library about equivalence relations to define the set of orbits and the map assigning to each element of @{term M} its orbit› definition orbits where "orbits = M // same_orbit_rel" definition orbit :: "'c ⇒ 'c set" where "orbit m = same_orbit_rel `` {m}" text ‹Next, we define a more easy-to-use characterization of an orbit.› lemma orbit_char: assumes m:"m ∈ M" shows "orbit m = {n. ∃g. g ∈ carrier G ∧ (φ g) m = n}" using assms unfolding orbit_def Image_def same_orbit_rel_def proof(auto) fix x g assume g:"g ∈ carrier G" and "φ g x ∈ M" "x ∈ M" hence "φ (inv g) (φ g x) = x" by (metis group_inv_rel) moreover from g have "inv g ∈ carrier G" by (rule inv_closed) ultimately show "∃h. h ∈ carrier G ∧ φ h (φ g x) = x" by auto next fix g assume g:"g ∈ carrier G" with m show "φ g m ∈ M" by (metis action_closed) with m g have "φ (inv g) (φ g m) = m" by (metis group_inv_rel) moreover from g have "inv g ∈ carrier G" by (rule inv_closed) ultimately show "∃h∈carrier G. φ h (φ g m) = m" by auto qed lemma same_orbit_char: assumes "m ∈ M" "n ∈ M" shows "(m, n) ∈ same_orbit_rel = (∃g ∈ carrier G. ((φ g) n = m))" unfolding same_orbit_rel_def using assms by auto text ‹Now we show that the relation we've defined is, indeed, an equivalence relation:› lemma same_orbit_is_equiv: shows "equiv M same_orbit_rel" proof(rule equivI) show "refl_on M same_orbit_rel" proof(rule refl_onI) show "same_orbit_rel ⊆ M × M" unfolding same_orbit_rel_def by auto next fix m assume "m ∈ M" hence "(φ 𝟭) m = m" by(rule one_is_id) with ‹m ∈ M› show "(m, m) ∈ same_orbit_rel" unfolding same_orbit_rel_def by (auto simp:same_orbit_char) qed next show "sym same_orbit_rel" proof(rule symI) fix m n assume mn:"(m, n) ∈ same_orbit_rel" then obtain g where g:"g ∈ carrier G" "φ g n = m" unfolding same_orbit_rel_def by auto hence invg:"inv g ∈ carrier G" by (metis inv_closed) from mn have "(m, n) ∈ M × M" unfolding same_orbit_rel_def by simp hence mn2:"m ∈ M" "n ∈ M" by auto from g mn2 have "φ (inv g) m = n" by (metis group_inv_rel) with invg mn2 show "(n, m) ∈ same_orbit_rel" unfolding same_orbit_rel_def by auto qed next show "trans same_orbit_rel" proof(rule transI) fix x y z assume xy:"(x, y) ∈ same_orbit_rel" then obtain g where g:"g ∈ carrier G" and grel:"(φ g) y = x" unfolding same_orbit_rel_def by auto assume yz:"(y, z) ∈ same_orbit_rel" then obtain h where h:"h ∈ carrier G" and hrel:"(φ h) z = y" unfolding same_orbit_rel_def by auto from g h have gh:"g ⊗ h ∈ carrier G" by simp from xy yz have "x ∈ M" "z ∈ M" unfolding same_orbit_rel_def by auto with g h have "φ (g ⊗ h) z = (φ g) ((φ h) z)" by (metis action_mult) also from hrel grel have "... = x" by simp finally have "φ (g ⊗ h) z = x". with gh ‹x ∈ M› ‹z ∈ M› show "(x, z) ∈ same_orbit_rel" unfolding same_orbit_rel_def by auto qed qed subsection ‹Stabilizer and fixed points› text ‹The following definition models the stabilizer of a group action:› definition stabilizer :: "'c ⇒ _" where "stabilizer m = {g ∈ carrier G. (φ g) m = m}" text ‹This shows that the stabilizer of @{term m} is a subgroup of @{term G}.› lemma stabilizer_is_subgroup: assumes m:"m ∈ M" shows "subgroup (stabilizer m) G" proof(rule subgroupI) show "stabilizer m ⊆ carrier G" unfolding stabilizer_def by auto next from m have "(φ 𝟭) m = m" by (rule one_is_id) hence "𝟭 ∈ stabilizer m" unfolding stabilizer_def by simp thus "stabilizer m ≠ {}" by auto next fix g assume g:"g ∈ stabilizer m" hence "g ∈ carrier G" "(φ g) m = m" unfolding stabilizer_def by simp+ with m have ginv:"(φ (inv g)) m = m" by (metis group_inv_rel) from ‹g ∈ carrier G› have "inv g ∈ carrier G" by (metis inv_closed) with ginv show "(inv g) ∈ stabilizer m" unfolding stabilizer_def by simp next fix g h assume g:"g ∈ stabilizer m" hence g2:"g ∈ carrier G" unfolding stabilizer_def by simp assume h:"h ∈ stabilizer m" hence h2:"h ∈ carrier G" unfolding stabilizer_def by simp with g2 have gh:"g ⊗ h ∈ carrier G" by (rule m_closed) from g2 h2 m have "φ (g ⊗ h) m = (φ g) ((φ h) m)" by (metis action_mult) also from g h have "... = m" unfolding stabilizer_def by simp finally have "φ (g ⊗ h) m = m". with gh show "g ⊗ h ∈ stabilizer m" unfolding stabilizer_def by simp qed text ‹Next, we define and characterize the fixed points of a group action.› definition fixed_points :: "'c set" where "fixed_points = {m ∈ M. carrier G ⊆ stabilizer m}" lemma fixed_point_char: assumes "m ∈ M" shows "(m ∈ fixed_points) = (∀g∈carrier G. φ g m = m)" using assms unfolding fixed_points_def stabilizer_def by force lemma orbit_contains_rep: assumes m:"m ∈ M" shows "m ∈ orbit m" unfolding orbit_def using assms by (metis equiv_class_self same_orbit_is_equiv) lemma singleton_orbit_eq_fixed_point: assumes m:"m ∈ M" shows "(card (orbit m) = 1) = (m ∈ fixed_points)" proof assume card:"card (orbit m) = 1" from m have "m ∈ orbit m" by (rule orbit_contains_rep) from m show "m ∈ fixed_points" unfolding fixed_points_def proof(auto) fix g assume gG:"g ∈ carrier G" with m have "φ g m ∈ orbit m" by (auto dest:orbit_char) with ‹m ∈ orbit m› card have "φ g m = m" by (auto simp add: card_Suc_eq) with gG show "g ∈ stabilizer m" unfolding stabilizer_def by simp qed next assume "m ∈ fixed_points" hence fixed:"carrier G ⊆ stabilizer m" unfolding fixed_points_def by simp from m have "orbit m = {m}" proof(auto simp add: orbit_contains_rep) fix n assume "n ∈ orbit m" with m obtain g where g:"g ∈ carrier G" "φ g m = n" by (auto dest: orbit_char) moreover with fixed have "φ g m = m" unfolding stabilizer_def by auto ultimately show "n = m" by simp qed thus "card (orbit m) = 1" by simp qed subsection ‹The Orbit-Stabilizer Theorem› text ‹This section contains some theorems about orbits and their quotient groups. The first one is the well-known orbit-stabilizer theorem which establishes a bijection between the the quotient group of the an element's stabilizer and its orbit.› theorem orbit_thm: assumes m:"m ∈ M" assumes rep:"⋀U. U ∈ (carrier (G Mod (stabilizer m))) ⟹ rep U ∈ U" shows "bij_betw (λH. (φ (inv (rep H)) m)) (carrier (G Mod (stabilizer m))) (orbit m)" proof(auto simp add:bij_betw_def) show "inj_on (λH. φ (inv (rep H)) m) (carrier (G Mod stabilizer m))" proof(rule inj_onI) fix U V assume U:"U ∈ carrier (G Mod (stabilizer m))" assume V:"V ∈ carrier (G Mod (stabilizer m))" define h where "h = rep V" define g where "g = rep U" have stabSubset:"(stabilizer m) ⊆ carrier G" unfolding stabilizer_def by auto from m have stabSubgroup: "subgroup (stabilizer m) G" by (metis stabilizer_is_subgroup) from V rep have hV:"h ∈ V" unfolding h_def by simp from V stabSubset have "V ⊆ carrier G" unfolding FactGroup_def RCOSETS_def r_coset_def by auto with hV have hG:"h ∈ carrier G" by auto hence hinvG:"inv h ∈ carrier G" by (metis inv_closed) from U rep have gU:"g ∈ U" unfolding g_def by simp from U stabSubset have "U ⊆ carrier G" unfolding FactGroup_def RCOSETS_def r_coset_def by auto with gU have gG:"g ∈ carrier G" by auto hence ginvG:"inv g ∈ carrier G" by (metis inv_closed) from gG hinvG have ginvhG: "g ⊗ inv h ∈ carrier G" by (metis m_closed) assume reps:"φ (inv rep U) m = φ (inv rep V) m" hence gh:"φ (inv g) m = φ (inv h) m" unfolding g_def h_def. from gG hinvG m have "φ (g ⊗ (inv h)) m = φ g (φ (inv h) m)" by (metis action_mult) also from gh ginvG gG m have "... = φ (g ⊗ inv g) m" by (metis action_mult) also from m gG have "... = m" by (auto simp: one_is_id) finally have "φ (g ⊗ inv h) m = m". with ginvhG have "(g ⊗ inv h) ∈ stabilizer m" unfolding stabilizer_def by simp hence "(stabilizer m) #> (g ⊗ inv h) = (stabilizer m) #> 𝟭" by (metis coset_join2 coset_mult_one m stabSubset stabilizer_is_subgroup subgroup.mem_carrier) with hinvG hG gG stabSubset have stabgstabh:"(stabilizer m) #> g = (stabilizer m) #> h" by (metis coset_mult_inv1 group.coset_mult_one is_group) from stabSubgroup is_group U gU have "U = (stabilizer m) #> g" unfolding FactGroup_def by (simp add:subgroup.repr_independence2) also from stabgstabh is_group stabSubgroup V hV subgroup.repr_independence2 have "... = V" unfolding FactGroup_def by force finally show "U = V". qed next have stabSubset:"stabilizer m ⊆ carrier G" unfolding stabilizer_def by auto fix H assume H:"H ∈ carrier (G Mod stabilizer m)" with rep have "rep H ∈ H" by simp moreover with H stabSubset have "H ⊆ carrier G" unfolding FactGroup_def RCOSETS_def r_coset_def by auto ultimately have "rep H ∈ carrier G".. hence "inv rep H ∈ carrier G" by (rule inv_closed) with m show "φ (inv rep H) m ∈ orbit m" by (auto dest:orbit_char) next fix n assume "n ∈ orbit m" with m obtain g where g:"g ∈ carrier G" "φ g m = n" by (auto dest:orbit_char) hence invg:"inv g ∈ carrier G" by simp hence stabinvg:"((stabilizer m) #> (inv g)) ∈ carrier (G Mod stabilizer m)" unfolding FactGroup_def RCOSETS_def by auto hence "rep ((stabilizer m) #> (inv g)) ∈ (stabilizer m) #> (inv g)" by (metis rep) then obtain h where h:"h ∈ stabilizer m" "rep ((stabilizer m) #> (inv g)) = h ⊗ (inv g)" unfolding r_coset_def by auto with g have "φ (inv rep ((stabilizer m) #> (inv g))) m = φ (inv (h ⊗ (inv g))) m" by simp also from h have hG:"h ∈ carrier G" unfolding stabilizer_def by simp with g have "φ (inv (h ⊗ (inv g))) m = φ (g ⊗ (inv h)) m" by (metis inv_closed inv_inv inv_mult_group) also from g hG m have "... = φ g (φ (inv h) m)" by (metis action_mult inv_closed) also from h m have "inv h ∈ stabilizer m" by (metis stabilizer_is_subgroup subgroup.m_inv_closed) hence "φ g (φ (inv h) m) = φ g m" unfolding stabilizer_def by simp also from g have "... = n" by simp finally have "n = φ (inv rep ((stabilizer m) #> (inv g))) m".. with stabinvg show "n ∈ (λH. φ (inv rep H) m) ` carrier (G Mod stabilizer m)" by simp qed text ‹In the case of @{term G} being finite, the last theorem can be reduced to a statement about the cardinality of orbit and stabilizer:› corollary orbit_size: assumes fin:"finite (carrier G)" assumes m:"m ∈ M" shows "order G = card (orbit m) * card (stabilizer m)" proof - define rep where "rep = (λU ∈ (carrier (G Mod (stabilizer m))). SOME x. x ∈ U)" have "⋀U. U ∈ (carrier (G Mod (stabilizer m))) ⟹ rep U ∈ U" proof - fix U assume U:"U ∈ carrier (G Mod stabilizer m)" then obtain g where "g ∈ carrier G" " U = (stabilizer m) #> g" unfolding FactGroup_def RCOSETS_def by auto with m have "(SOME x. x ∈ U) ∈ U" by (metis rcos_self stabilizer_is_subgroup someI_ex) with U show "rep U ∈ U" unfolding rep_def by simp qed with m have bij:"card (carrier (G Mod (stabilizer m))) = card (orbit m)" by (metis bij_betw_same_card orbit_thm) from fin m have "card (carrier (G Mod (stabilizer m))) * card (stabilizer m) = order G" unfolding FactGroup_def by (simp add: stabilizer_is_subgroup lagrange) with bij show ?thesis by simp qed lemma orbit_not_empty: assumes fin:"finite M" assumes A:"A ∈ orbits" shows "card A > 0" proof - from A obtain m where "m ∈ M" "A = orbit m" unfolding orbits_def quotient_def orbit_def by auto hence "m ∈ A" by (metis orbit_contains_rep) hence "A ≠ {}" unfolding orbits_def by auto moreover from fin A have "finite A" unfolding orbits_def quotient_def Image_def same_orbit_rel_def by auto ultimately show ?thesis by auto qed lemma fin_set_imp_fin_orbits: assumes finM:"finite M" shows "finite orbits" using assms unfolding orbits_def quotient_def by simp (*One-Element-Orbits are Fixed Points*) lemma singleton_orbits: shows "⋃{N∈orbits. card N = 1} = fixed_points" proof show "⋃{N ∈ orbits. card N = 1} ⊆ fixed_points" proof fix x assume a:"x ∈ ⋃{N ∈ orbits. card N = 1}" hence "x ∈ M" unfolding orbits_def quotient_def Image_def same_orbit_rel_def by auto from a obtain N where N:"N ∈ orbits" "card N = 1" "x ∈ N" by auto then obtain y where Norbit:"N = orbit y" "y ∈ M" unfolding orbits_def quotient_def orbit_def by auto hence "y ∈ N" by (metis orbit_contains_rep) with N have Nsing:"N = {x}" "N = {y}" by (auto simp: card_Suc_eq) hence "x = y" by simp with Norbit have Norbit2:"N = orbit x" by simp have "{g ∈ carrier G. φ g x = x} = carrier G" proof(auto) fix g assume "g ∈ carrier G" with ‹x ∈ M› have "φ g x ∈ orbit x" by (auto dest:orbit_char) with Nsing show "φ g x = x" by (metis Norbit2 singleton_iff) qed with ‹x ∈ M› show "x ∈ fixed_points" unfolding fixed_points_def stabilizer_def by simp qed next show "fixed_points ⊆ ⋃{N ∈ orbits. card N = 1}" proof fix m assume m:"m ∈ fixed_points" hence mM:"m ∈ M" unfolding fixed_points_def by simp hence orbit:"orbit m ∈ orbits" unfolding orbits_def quotient_def orbit_def by auto from mM m have "card (orbit m) = 1" by (metis singleton_orbit_eq_fixed_point) with orbit have "orbit m ∈ {N ∈ orbits. card N = 1}" by simp with mM show "m ∈ ⋃{N ∈ orbits. card N = 1}" by (auto dest: orbit_contains_rep) qed qed text ‹If @{term G} is a @{term p}-group acting on a finite set, a given orbit is either a singleton or @{term p} divides its cardinality.› lemma p_dvd_orbit_size: assumes orderG:"order G = p ^ a" assumes prime:"prime p" assumes finM:"finite M" assumes Norbit:"N ∈ orbits" assumes "card N > 1" shows "p dvd card N" proof - from Norbit obtain m where m:"m ∈ M" "N = orbit m" unfolding orbits_def quotient_def orbit_def by auto from prime have "0 < p ^ a" by (simp add: prime_gt_0_nat) with orderG have "finite (carrier G)" unfolding order_def by (metis card.infinite less_nat_zero_code) with m have "order G = card (orbit m) * card (stabilizer m)" by (metis orbit_size) with orderG m have "p ^ a = card N * card (stabilizer m)" by simp with ‹card N > 1› show ?thesis by (metis dvd_mult2 dvd_mult_cancel1 nat_dvd_not_less nat_mult_1 prime prime_dvd_power_nat prime_factor_nat prime_nat_iff zero_less_one) qed text ‹As a result of the last lemma the only orbits that count modulo @{term p} are the fixed points› lemma fixed_point_congruence: assumes "order G = p ^ a" assumes "prime p" assumes finM:"finite M" shows "card M mod p = card fixed_points mod p" proof - define big_orbits where "big_orbits = {N∈orbits. card N > 1}" from finM have orbit_part:"orbits = big_orbits ∪ {N∈orbits. card N = 1}" unfolding big_orbits_def by (auto dest:orbit_not_empty) have orbit_disj:"big_orbits ∩ {N∈orbits. card N = 1} = {}" unfolding big_orbits_def by auto from finM have orbits_fin:"finite orbits" by (rule fin_set_imp_fin_orbits) hence fin_parts:"finite big_orbits" "finite {N∈orbits. card N = 1}" unfolding big_orbits_def by simp+ from assms have "⋀N. N ∈ big_orbits ⟹ p dvd card N" unfolding big_orbits_def by (auto simp: p_dvd_orbit_size) hence orbit_div:"⋀N. N ∈ big_orbits ⟹ card N = (card N div p) * p" by (metis dvd_mult_div_cancel mult.commute) have "card M = card (⋃ orbits)" unfolding orbits_def by (metis Union_quotient same_orbit_is_equiv) also have "card (⋃ orbits) = (∑N∈orbits. card N)" unfolding orbits_def proof (rule card_Union_disjoint) show "pairwise disjnt (M // same_orbit_rel)" unfolding pairwise_def disjnt_def by(metis same_orbit_is_equiv quotient_disj) show "⋀A. A ∈ M // same_orbit_rel ⟹ finite A" using finM same_orbit_rel_def by (auto dest:finite_equiv_class) qed also from orbit_part orbit_disj fin_parts have "... = (∑N∈big_orbits. card N) + (∑N∈{N'∈orbits. card N' = 1}. card N)" by (metis (lifting) sum.union_disjoint) also from assms orbit_div fin_parts have "... = (∑N∈big_orbits. (card N div p) * p) + card (⋃{N'∈orbits. card N' = 1})" by (auto simp: card_singleton_set) also have "... = (∑N∈big_orbits. card N div p) * p + card fixed_points" using singleton_orbits by (auto simp:sum_distrib_right) finally have "card M = (∑N∈big_orbits. card N div p) * p + card fixed_points". hence "card M mod p = ((∑N∈big_orbits. card N div p) * p + card fixed_points) mod p" by simp also have "... = (card fixed_points) mod p" by (metis mod_mult_self3) finally show ?thesis. qed text ‹We can restrict any group action to the action of a subgroup:› lemma subgroup_action: assumes H:"subgroup H G" shows "group_action (G⦇carrier := H⦈) φ M" unfolding group_action_def group_action_axioms_def group_hom_def group_hom_axioms_def hom_def using assms proof (auto simp add: is_group subgroup.subgroup_is_group group_BijGroup) fix x assume "x ∈ H" with H have "x ∈ carrier G" by (metis subgroup.mem_carrier) with grouphom show "φ x ∈ carrier (BijGroup M)" by (metis group_hom.hom_closed) next fix x y assume x:"x ∈ H" and y:"y ∈ H" with H have "x ∈ carrier G" "y ∈ carrier G" by (metis subgroup.mem_carrier)+ with grouphom show "φ (x ⊗ y) = φ x ⊗⇘BijGroup M⇙ φ y" by (simp add: group_hom.hom_mult) qed end subsection ‹Some Examples for Group Actions› lemma (in group) right_mult_is_bij: assumes h:"h ∈ carrier G" shows "(λg ∈ carrier G. h ⊗ g) ∈ Bij (carrier G)" proof(auto simp add:Bij_def bij_betw_def inj_on_def) fix x y assume x:"x ∈ carrier G" and y:"y ∈ carrier G" and "h ⊗ x = h ⊗ y" with h show "x = y" by simp next fix x assume x:"x ∈ carrier G" with h show "h ⊗ x ∈ carrier G" by (metis m_closed) from x h have "inv h ⊗ x ∈ carrier G" by (metis m_closed inv_closed) moreover from x h have "h ⊗ (inv h ⊗ x) = x" by (metis inv_closed r_inv m_assoc l_one) ultimately show "x ∈ (⊗) h ` carrier G" by force qed lemma (in group) right_mult_group_action: shows "group_action G (λh. λg ∈ carrier G. h ⊗ g) (carrier G)" unfolding group_action_def group_action_axioms_def group_hom_def group_hom_axioms_def hom_def proof(auto simp add:is_group group_BijGroup) fix h assume "h ∈ carrier G" thus "(λg ∈ carrier G. h ⊗ g) ∈ carrier (BijGroup (carrier G))" unfolding BijGroup_def by (auto simp:right_mult_is_bij) next fix x y assume x:"x ∈ carrier G" and y:"y ∈ carrier G" define multx multy where "multx = (λg∈carrier G. x ⊗ g)" and "multy = (λg∈carrier G. y ⊗ g)" with x y have "multx ∈ (Bij (carrier G))" "multy ∈ (Bij (carrier G))" by (metis right_mult_is_bij)+ hence "multx ⊗⇘BijGroup (carrier G)⇙ multy = (λg∈carrier G. multx (multy g))" unfolding BijGroup_def by (auto simp: compose_def) also have "... = (λg∈carrier G. (x ⊗ y) ⊗ g)" unfolding multx_def multy_def proof(rule restrict_ext) fix g assume g:"g ∈ carrier G" with x y have "x ⊗ y ∈ carrier G" "y ⊗ g ∈ carrier G" by simp+ with x y g show "(λg∈carrier G. x ⊗ g) ((λg∈carrier G. y ⊗ g) g) = x ⊗ y ⊗ g" by (auto simp:m_assoc) qed finally show "(λg∈carrier G. (x ⊗ y) ⊗ g) = (λg∈carrier G. x ⊗ g) ⊗⇘BijGroup (carrier G)⇙ (λg∈carrier G. y ⊗ g)" unfolding multx_def multy_def by simp qed lemma (in group) rcosets_closed: assumes HG:"subgroup H G" assumes g:"g ∈ carrier G" assumes M:"M ∈ rcosets H" shows "M #> g ∈ rcosets H" proof - from M obtain h where h:"h ∈ carrier G" "M = H #> h" unfolding RCOSETS_def by auto with g HG have "M #> g = H #> (h ⊗ g)" by (metis coset_mult_assoc subgroup.subset) with HG g h show "M #> g ∈ rcosets H" by (metis rcosetsI subgroup.m_closed subgroup.subset subgroup_self) qed lemma (in group) inv_mult_on_rcosets_is_bij: assumes HG:"subgroup H G" assumes g:"g ∈ carrier G" shows "(λU ∈ rcosets H. U #> inv g) ∈ Bij (rcosets H)" proof(auto simp add:Bij_def bij_betw_def inj_on_def) fix M assume "M ∈ rcosets H" with HG g show "M #> inv g ∈ rcosets H" by (metis inv_closed rcosets_closed) next fix M assume M:"M ∈ rcosets H" with HG g have "M #> g ∈ rcosets H" by (rule rcosets_closed) moreover from M HG g have "M #> g #> inv g = M" by (metis coset_mult_assoc coset_mult_inv2 inv_closed is_group subgroup.rcosets_carrier) ultimately show " M ∈ (λU. U #> inv g) ` (rcosets H)" by auto next fix M N x assume M:"M ∈ rcosets H" and N:"N ∈ rcosets H" and "M #> inv g = N #> inv g" hence "(M #> inv g) #> g = (N #> inv g) #> g" by simp with HG M N g have "M #> (inv g ⊗ g) = N #> (inv g ⊗ g)" by (metis coset_mult_assoc is_group subgroup.m_inv_closed subgroup.rcosets_carrier subgroup_self) with HG M N g have a1:"M = N" by (metis l_inv coset_mult_one is_group subgroup.rcosets_carrier) { assume "x ∈ M" with a1 show "x ∈ N" by simp } { assume "x ∈ N" with a1 show "x ∈ M" by simp } qed lemma (in group) inv_mult_on_rcosets_action: assumes HG:"subgroup H G" shows "group_action G (λg. λU ∈ rcosets H. U #> inv g) (rcosets H)" unfolding group_action_def group_action_axioms_def group_hom_def group_hom_axioms_def hom_def proof(auto simp add:is_group group_BijGroup) fix h assume "h ∈ carrier G" with HG show "(λU ∈ rcosets H. U #> inv h) ∈ carrier (BijGroup (rcosets H))" unfolding BijGroup_def by (auto simp:inv_mult_on_rcosets_is_bij) next fix x y assume x:"x ∈ carrier G" and y:"y ∈ carrier G" define cosx cosy where "cosx = (λU∈rcosets H. U #> inv x)" and "cosy = (λU∈rcosets H. U #> inv y)" with x y HG have "cosx ∈ (Bij (rcosets H))" "cosy ∈ (Bij (rcosets H))" by (metis inv_mult_on_rcosets_is_bij)+ hence "cosx ⊗⇘BijGroup (rcosets H)⇙ cosy = (λU∈rcosets H. cosx (cosy U))" unfolding BijGroup_def by (auto simp: compose_def) also have "... = (λU∈rcosets H. U #> inv (x ⊗ y))" unfolding cosx_def cosy_def proof(rule restrict_ext) fix U assume U:"U ∈ rcosets H" with HG y have "U #> inv y ∈ rcosets H" by (metis inv_closed rcosets_closed) with x y HG U have "(λU∈rcosets H. U #> inv x) ((λU∈rcosets H. U #> inv y) U) = U #> inv y #> inv x" by auto also from x y U HG have "... = U #> inv (x ⊗ y)" by (metis inv_mult_group coset_mult_assoc inv_closed is_group subgroup.rcosets_carrier) finally show "(λU∈rcosets H. U #> inv x) ((λU∈rcosets H. U #> inv y) U) = U #> inv (x ⊗ y)". qed finally show "(λU∈rcosets H. U #> inv (x ⊗ y)) = (λU∈rcosets H. U #> inv x) ⊗⇘BijGroup (rcosets H)⇙ (λU∈rcosets H. U #> inv y)" unfolding cosx_def cosy_def by simp qed end