# Theory GroupAction

```(*  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}"
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)"
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"
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)"
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
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)"
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
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
```