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) = (∑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