Theory Secondary_Sylow.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) = (xA. card x)"
  proof(rule card_Union_disjoint)
    from cardOne show "a. aA  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  rcosetsGH"
  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 "... = (λxM. 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 "hcarrier 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) = (gcarrier 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 "{Norbits. 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 = {Norbits. card N > 1}"
  from finM have orbit_part:"orbits = big_orbits  {Norbits. card N = 1}" unfolding big_orbits_def by (auto dest:orbit_not_empty)
  have orbit_disj:"big_orbits  {Norbits. 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 {Norbits. 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) = (Norbits. 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 "... = (Nbig_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 "... = (Nbig_orbits. (card N div p) * p) + card ({N'orbits. card N' = 1})" by (auto simp: card_singleton_set)
  also have "... = (Nbig_orbits. card N div p) * p + card fixed_points" using singleton_orbits by (auto simp:sum_distrib_right)
  finally have "card M = (Nbig_orbits. card N div p) * p + card fixed_points".
  hence "card M mod p = ((Nbig_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 (Gcarrier := 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 = (λgcarrier G. x  g)"
      and "multy = (λgcarrier 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 = (λgcarrier G. multx (multy g))" unfolding BijGroup_def by (auto simp: compose_def)
  also have "... = (λgcarrier 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 "(λgcarrier G. x  g) ((λgcarrier G. y  g) g) = x  y  g" by (auto simp:m_assoc)
  qed
  finally show "(λgcarrier G. (x  y)  g) = (λgcarrier G. x  g) BijGroup (carrier G)(λgcarrier 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 = (λUrcosets H. U #> inv x)"
      and "cosy = (λUrcosets 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 = (λUrcosets H. cosx (cosy U))"
    unfolding BijGroup_def by (auto simp: compose_def)
  also have "... = (λUrcosets 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 "(λUrcosets H. U #> inv x) ((λUrcosets 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 "(λUrcosets H. U #> inv x) ((λUrcosets H. U #> inv y) U) = U #> inv (x  y)".
  qed
  finally show "(λUrcosets H. U #> inv (x  y)) = (λUrcosets H. U #> inv x) BijGroup (rcosets H)(λUrcosets H. U #> inv y)"
    unfolding cosx_def cosy_def by simp
qed

end