Theory HOL-Algebra.Group_Action

(*  Title:      HOL/Algebra/Group_Action.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Group_Action
imports Bij Coset Congruence
begin

section ‹Group Actions›

locale group_action =
  fixes G (structure) and E and φ
  assumes group_hom: "group_hom G (BijGroup E) φ"

definition
  orbit :: "[_, 'a  'b  'b, 'b]  'b set"
  where "orbit G φ x = {(φ g) x | g. g  carrier G}"

definition
  orbits :: "[_, 'b set, 'a  'b  'b]  ('b set) set"
  where "orbits G E φ = {orbit G φ x | x. x  E}"

definition
  stabilizer :: "[_, 'a  'b  'b, 'b]  'a set"
  where "stabilizer G φ x = {g  carrier G. (φ g) x = x}"

definition
  invariants :: "['b set, 'a  'b  'b, 'a]  'b set"
  where "invariants E φ g = {x  E. (φ g) x = x}"

definition
  normalizer :: "[_, 'a set]  'a set"
  where "normalizer G H =
         stabilizer G (λg. λH  {H. H  carrier G}. g <#GH #>G(invGg)) H"

locale faithful_action = group_action +
  assumes faithful: "inj_on φ (carrier G)"

locale transitive_action = group_action +
  assumes unique_orbit: " x  E; y  E   g  carrier G. (φ g) x = y"



subsection ‹Prelimineries›

text ‹Some simple lemmas to make group action's properties more explicit›

lemma (in group_action) id_eq_one: "(λx  E. x) = φ 𝟭"
  by (metis BijGroup_def group_hom group_hom.hom_one select_convs(2))

lemma (in group_action) bij_prop0:
  " g. g  carrier G  (φ g)  Bij E"
  by (metis BijGroup_def group_hom group_hom.hom_closed partial_object.select_convs(1))

lemma (in group_action) surj_prop:
  " g. g  carrier G  (φ g) ` E = E"
  using bij_prop0 by (simp add: Bij_def bij_betw_def)

lemma (in group_action) inj_prop:
  " g. g  carrier G  inj_on (φ g) E"
  using bij_prop0 by (simp add: Bij_def bij_betw_def)

lemma (in group_action) bij_prop1:
  " g y.  g  carrier G; y  E    ∃!x  E. (φ g) x = y"
proof -
  fix g y assume "g  carrier G" "y  E"
  hence "x  E. (φ g) x = y"
    using surj_prop by force
  moreover have " x1 x2.  x1  E; x2  E   (φ g) x1 = (φ g) x2  x1 = x2"
    using inj_prop by (meson g  carrier G inj_on_eq_iff)
  ultimately show "∃!x  E. (φ g) x = y"
    by blast
qed

lemma (in group_action) composition_rule:
  assumes "x  E" "g1  carrier G" "g2  carrier G"
  shows "φ (g1  g2) x = (φ g1) (φ g2 x)"
proof -
  have "φ (g1  g2) x = ((φ g1) BijGroup E(φ g2)) x"
    using assms(2) assms(3) group_hom group_hom.hom_mult by fastforce
  also have " ... = (compose E (φ g1) (φ g2)) x"
    unfolding BijGroup_def by (simp add: assms bij_prop0)
  finally show "φ (g1  g2) x = (φ g1) (φ g2 x)"
    by (simp add: assms(1) compose_eq)
qed

lemma (in group_action) element_image:
  assumes "g  carrier G" and "x  E" and "(φ g) x = y"
  shows "y  E"
  using surj_prop assms by blast



subsection ‹Orbits›

text‹We prove here that orbits form an equivalence relation›

lemma (in group_action) orbit_sym_aux:
  assumes "g  carrier G"
    and "x  E"
    and "(φ g) x = y"
  shows "(φ (inv g)) y = x"
proof -
  interpret group G
    using group_hom group_hom.axioms(1) by auto
  have "y  E"
    using element_image assms by simp
  have "inv g  carrier G"
    by (simp add: assms(1))

  have "(φ (inv g)) y = (φ (inv g)) ((φ g) x)"
    using assms(3) by simp
  also have " ... = compose E (φ (inv g)) (φ g) x"
    by (simp add: assms(2) compose_eq)
  also have " ... = ((φ (inv g)) BijGroup E(φ g)) x"
    by (simp add: BijGroup_def assms(1) bij_prop0)
  also have " ... = (φ ((inv g)  g)) x"
    by (metis inv g  carrier G assms(1) group_hom group_hom.hom_mult)
  finally show "(φ (inv g)) y = x"
    by (metis assms(1) assms(2) id_eq_one l_inv restrict_apply)
qed

lemma (in group_action) orbit_refl:
  "x  E  x  orbit G φ x"
proof -
  assume "x  E" hence "(φ 𝟭) x = x"
    using id_eq_one by (metis restrict_apply')
  thus "x  orbit G φ x" unfolding orbit_def
    using group.is_monoid group_hom group_hom.axioms(1) by force 
qed

lemma (in group_action) orbit_sym:
  assumes "x  E" and "y  E" and "y  orbit G φ x"
  shows "x  orbit G φ y"
proof -
  have " g  carrier G. (φ g) x = y"
    using assms by (auto simp: orbit_def)
  then obtain g where g: "g  carrier G  (φ g) x = y" by blast
  hence "(φ (inv g)) y = x"
    using orbit_sym_aux by (simp add: assms(1))
  thus ?thesis
    using g group_hom group_hom.axioms(1) orbit_def by fastforce 
qed

lemma (in group_action) orbit_trans:
  assumes "x  E" "y  E" "z  E"
    and "y  orbit G φ x" "z  orbit G φ y" 
  shows "z  orbit G φ x"
proof -
  interpret group G
    using group_hom group_hom.axioms(1) by auto
  obtain g1 where g1: "g1  carrier G  (φ g1) x = y" 
    using assms by (auto simp: orbit_def)
  obtain g2 where g2: "g2  carrier G  (φ g2) y = z" 
    using assms by (auto simp: orbit_def)  
  have "(φ (g2  g1)) x = ((φ g2) BijGroup E(φ g1)) x"
    using g1 g2 group_hom group_hom.hom_mult by fastforce
  also have " ... = (φ g2) ((φ g1) x)"
    using composition_rule assms(1) calculation g1 g2 by auto
  finally have "(φ (g2  g1)) x = z"
    by (simp add: g1 g2)
  thus ?thesis
    using g1 g2 orbit_def by force 
qed

lemma (in group_action) orbits_as_classes:
  "classes carrier = E, eq = λx. λy. y  orbit G φ x = orbits G E φ"
  unfolding eq_classes_def eq_class_of_def orbits_def orbit_def 
  using element_image by auto

theorem (in group_action) orbit_partition:
  "partition E (orbits G E φ)"
proof -
  have "equivalence  carrier = E, eq = λx. λy. y  orbit G φ x "
  unfolding equivalence_def apply simp
  using orbit_refl orbit_sym orbit_trans by blast
  thus ?thesis using equivalence.partition_from_equivalence orbits_as_classes by fastforce
qed

corollary (in group_action) orbits_coverture:
  " (orbits G E φ) = E"
  using partition.partition_coverture[OF orbit_partition] by simp

corollary (in group_action) disjoint_union:
  assumes "orb1  (orbits G E φ)" "orb2  (orbits G E φ)"
  shows "(orb1 = orb2)  (orb1  orb2) = {}"
  using partition.disjoint_union[OF orbit_partition] assms by auto

corollary (in group_action) disjoint_sum:
  assumes "finite E"
  shows "(orb(orbits G E φ). xorb. f x) = (xE. f x)"
  using partition.disjoint_sum[OF orbit_partition] assms by auto


subsubsection ‹Transitive Actions›

text ‹Transitive actions have only one orbit›

lemma (in transitive_action) all_equivalent:
  " x  E; y  E   x .=carrier = E, eq = λx y. y  orbit G φ xy"
proof -
  assume "x  E" "y  E"
  hence " g  carrier G. (φ g) x = y"
    using unique_orbit  by blast
  hence "y  orbit G φ x"
    using orbit_def by fastforce
  thus "x .=carrier = E, eq = λx y. y  orbit G φ xy" by simp
qed

proposition (in transitive_action) one_orbit:
  assumes "E  {}"
  shows "card (orbits G E φ) = 1"
proof -
  have "orbits G E φ  {}"
    using assms orbits_coverture by auto
  moreover have " orb1 orb2.  orb1  (orbits G E φ); orb2  (orbits G E φ)   orb1 = orb2"
  proof -
    fix orb1 orb2 assume orb1: "orb1  (orbits G E φ)"
                     and orb2: "orb2  (orbits G E φ)"
    then obtain x y where x: "orb1 = orbit G φ x" and x_E: "x  E" 
                      and y: "orb2 = orbit G φ y" and y_E: "y  E"
      unfolding orbits_def by blast
    hence "x  orbit G φ y" using all_equivalent by auto
    hence "orb1  orb2  {}" using x y x_E orbit_refl by auto
    thus "orb1 = orb2" using disjoint_union[of orb1 orb2] orb1 orb2 by auto
  qed
  ultimately show "card (orbits G E φ) = 1"
    by (meson is_singletonI' is_singleton_altdef)
qed



subsection ‹Stabilizers›

text ‹We show that stabilizers are subgroups from the acting group›

lemma (in group_action) stabilizer_subset:
  "stabilizer G φ x  carrier G"
  by (metis (no_types, lifting) mem_Collect_eq stabilizer_def subsetI)

lemma (in group_action) stabilizer_m_closed:
  assumes "x  E" "g1  (stabilizer G φ x)" "g2  (stabilizer G φ x)"
  shows "(g1  g2)  (stabilizer G φ x)"
proof -
  interpret group G
    using group_hom group_hom.axioms(1) by auto
  
  have "φ g1 x = x"
    using assms stabilizer_def by fastforce
  moreover have "φ g2 x = x"
    using assms stabilizer_def by fastforce
  moreover have g1: "g1  carrier G"
    by (meson assms contra_subsetD stabilizer_subset)
  moreover have g2: "g2  carrier G"
    by (meson assms contra_subsetD stabilizer_subset)
  ultimately have "φ (g1  g2) x = x"
    using composition_rule assms by simp

  thus ?thesis
    by (simp add: g1 g2 stabilizer_def) 
qed

lemma (in group_action) stabilizer_one_closed:
  assumes "x  E"
  shows "𝟭  (stabilizer G φ x)"
proof -
  have "φ 𝟭 x = x"
    by (metis assms id_eq_one restrict_apply')
  thus ?thesis
    using group_def group_hom group_hom.axioms(1) stabilizer_def by fastforce
qed

lemma (in group_action) stabilizer_m_inv_closed:
  assumes "x  E" "g  (stabilizer G φ x)"
  shows "(inv g)  (stabilizer G φ x)"
proof -
  interpret group G
    using group_hom group_hom.axioms(1) by auto

  have "φ g x = x"
    using assms(2) stabilizer_def by fastforce
  moreover have g: "g  carrier G"
    using assms(2) stabilizer_subset by blast
  moreover have inv_g: "inv g  carrier G"
    by (simp add: g)
  ultimately have "φ (inv g) x = x"
    using assms(1) orbit_sym_aux by blast

  thus ?thesis by (simp add: inv_g stabilizer_def) 
qed

theorem (in group_action) stabilizer_subgroup:
  assumes "x  E"
  shows "subgroup (stabilizer G φ x) G"
  unfolding subgroup_def
  using stabilizer_subset stabilizer_m_closed stabilizer_one_closed
        stabilizer_m_inv_closed assms by simp



subsection ‹The Orbit-Stabilizer Theorem›

text ‹In this subsection, we prove the Orbit-Stabilizer theorem.
      Our approach is to show the existence of a bijection between
      "rcosets (stabilizer G phi x)" and "orbit G phi x". Then we use
      Lagrange's theorem to find the cardinal of the first set.›

subsubsection ‹Rcosets - Supporting Lemmas›

corollary (in group_action) stab_rcosets_not_empty:
  assumes "x  E" "R  rcosets (stabilizer G φ x)"
  shows "R  {}"
  using subgroup.rcosets_non_empty[OF stabilizer_subgroup[OF assms(1)] assms(2)] by simp

corollary (in group_action) diff_stabilizes:
  assumes "x  E" "R  rcosets (stabilizer G φ x)"
  shows "g1 g2.  g1  R; g2  R   g1  (inv g2)  stabilizer G φ x"
  using group.diff_neutralizes[of G "stabilizer G φ x" R] stabilizer_subgroup[OF assms(1)]
        assms(2) group_hom group_hom.axioms(1) by blast


subsubsection ‹Bijection Between Rcosets and an Orbit - Definition and Supporting Lemmas›

(* This definition could be easier if lcosets were available, and it's indeed a considerable
   modification at Coset theory, since we could derive it easily from the definition of rcosets
   following the same idea we use here: f: rcosets → lcosets, s.t. f R = (λg. inv g) ` R
   is a bijection. *)

definition
  orb_stab_fun :: "[_, ('a  'b  'b), 'a set, 'b]  'b"
  where "orb_stab_fun G φ R x = (φ (invG(SOME h. h  R))) x"

lemma (in group_action) orbit_stab_fun_is_well_defined0:
  assumes "x  E" "R  rcosets (stabilizer G φ x)"
  shows "g1 g2.  g1  R; g2  R   (φ (inv g1)) x = (φ (inv g2)) x"
proof -
  fix g1 g2 assume g1: "g1  R" and g2: "g2  R"
  have R_carr: "R  carrier G"
    using subgroup.rcosets_carrier[OF stabilizer_subgroup[OF assms(1)]]
          assms(2) group_hom group_hom.axioms(1) by auto
  from R_carr have g1_carr: "g1  carrier G" using g1 by blast
  from R_carr have g2_carr: "g2  carrier G" using g2 by blast

  have "g1  (inv g2)  stabilizer G φ x"
    using diff_stabilizes[of x R g1 g2] assms g1 g2 by blast
  hence "φ (g1  (inv g2)) x = x"
    by (simp add: stabilizer_def)
  hence "(φ (inv g1)) x = (φ (inv g1)) (φ (g1  (inv g2)) x)" by simp
  also have " ... = φ ((inv g1)  (g1  (inv g2))) x"
    using group_def assms(1) composition_rule g1_carr g2_carr
          group_hom group_hom.axioms(1) monoid.m_closed by fastforce
  also have " ... = φ (((inv g1)  g1)  (inv g2)) x"
    using group_def g1_carr g2_carr group_hom group_hom.axioms(1) monoid.m_assoc by fastforce
  finally show "(φ (inv g1)) x = (φ (inv g2)) x"
    using group_def g1_carr g2_carr group.l_inv group_hom group_hom.axioms(1) by fastforce
qed

lemma (in group_action) orbit_stab_fun_is_well_defined1:
  assumes "x  E" "R  rcosets (stabilizer G φ x)"
  shows "g. g  R  (φ (inv (SOME h. h  R))) x = (φ (inv g)) x"
  by (meson assms orbit_stab_fun_is_well_defined0 someI_ex)

lemma (in group_action) orbit_stab_fun_is_inj:
  assumes "x  E"
    and "R1  rcosets (stabilizer G φ x)"
    and "R2  rcosets (stabilizer G φ x)"
    and "φ (inv (SOME h. h  R1)) x = φ (inv (SOME h. h  R2)) x"
  shows "R1 = R2"
proof -
  have "(g1. g1  R1)  (g2. g2  R2)"
    using assms(1-3) stab_rcosets_not_empty by auto
  then obtain g1 g2 where g1: "g1  R1" and g2: "g2  R2" by blast
  hence g12_carr: "g1  carrier G  g2  carrier G"
    using subgroup.rcosets_carrier assms(1-3) group_hom
          group_hom.axioms(1) stabilizer_subgroup by blast

  then obtain r1 r2 where r1: "r1  carrier G" "R1 = (stabilizer G φ x) #> r1"
                      and r2: "r2  carrier G" "R2 = (stabilizer G φ x) #> r2"
    using assms(1-3) unfolding RCOSETS_def by blast
  then obtain s1 s2 where s1: "s1  (stabilizer G φ x)" "g1 = s1  r1"
                      and s2: "s2  (stabilizer G φ x)" "g2 = s2  r2"
    using g1 g2 unfolding r_coset_def by blast

  have "φ (inv g1) x = φ (inv (SOME h. h  R1)) x"
    using orbit_stab_fun_is_well_defined1[OF assms(1) assms(2) g1] by simp
  also have " ... = φ (inv (SOME h. h  R2)) x"
    using assms(4) by simp
  finally have "φ (inv g1) x = φ (inv g2) x"
    using orbit_stab_fun_is_well_defined1[OF assms(1) assms(3) g2] by simp

  hence "φ g2 (φ (inv g1) x) = φ g2 (φ (inv g2) x)" by simp
  also have " ... = φ (g2  (inv g2)) x"
    using assms(1) composition_rule g12_carr group_hom group_hom.axioms(1) by fastforce
  finally have "φ g2 (φ (inv g1) x) = x"
    using g12_carr assms(1) group.r_inv group_hom group_hom.axioms(1)
          id_eq_one restrict_apply by metis
  hence "φ (g2  (inv g1)) x = x"
    using assms(1) composition_rule g12_carr group_hom group_hom.axioms(1) by fastforce
  hence "g2  (inv g1)  (stabilizer G φ x)"
    using g12_carr group.subgroup_self group_hom group_hom.axioms(1)
          mem_Collect_eq stabilizer_def subgroup_def by (metis (mono_tags, lifting))
  then obtain s where s: "s  (stabilizer G φ x)" "s = g2  (inv g1)" by blast

  let ?h = "s  g1"
  have "?h = s  (s1  r1)" by (simp add: s1)
  hence "?h = (s  s1)  r1"
    using stabilizer_subgroup[OF assms(1)] group_def group_hom
          group_hom.axioms(1) monoid.m_assoc r1 s s1 subgroup.mem_carrier by fastforce
  hence inR1: "?h  (stabilizer G φ x) #> r1" unfolding r_coset_def
    using stabilizer_subgroup[OF assms(1)] assms(1) s s1 stabilizer_m_closed by auto

  have "?h = g2" using s stabilizer_subgroup[OF assms(1)] g12_carr group.inv_solve_right
                       group_hom group_hom.axioms(1) subgroup.mem_carrier by metis
  hence inR2: "?h  (stabilizer G φ x) #> r2"
    using g2 r2 by blast

  have "R1  R2  {}" using inR1 inR2 r1 r2 by blast
  thus ?thesis
    using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G φ x"] assms group_hom group_hom.axioms(1) 
    unfolding disjnt_def pairwise_def  by blast
qed

lemma (in group_action) orbit_stab_fun_is_surj:
  assumes "x  E" "y  orbit G φ x"
  shows "R  rcosets (stabilizer G φ x). φ (inv (SOME h. h  R)) x = y"
proof -
  have "g  carrier G. (φ g) x = y"
    using assms(2) unfolding orbit_def by blast
  then obtain g where g: "g  carrier G  (φ g) x = y" by blast
  
  let ?R = "(stabilizer G φ x) #> (inv g)"
  have R: "?R  rcosets (stabilizer G φ x)"
    unfolding RCOSETS_def using g group_hom group_hom.axioms(1) by fastforce
  moreover have "𝟭  (inv g)  ?R"
    unfolding r_coset_def using assms(1) stabilizer_one_closed by auto
  ultimately have "φ (inv (SOME h. h  ?R)) x = φ (inv (𝟭  (inv g))) x"
    using orbit_stab_fun_is_well_defined1[OF assms(1)] by simp
  also have " ... = (φ g) x"
    using group_def g group_hom group_hom.axioms(1) monoid.l_one by fastforce
  finally have "φ (inv (SOME h. h  ?R)) x = y"
    using g by simp
  thus ?thesis using R by blast 
qed

proposition (in group_action) orbit_stab_fun_is_bij:
  assumes "x  E"
  shows "bij_betw (λR. (φ (inv (SOME h. h  R))) x) (rcosets (stabilizer G φ x)) (orbit G φ x)"
  unfolding bij_betw_def
proof
  show "inj_on (λR. φ (inv (SOME h. h  R)) x) (rcosets stabilizer G φ x)"
    using orbit_stab_fun_is_inj[OF assms(1)] by (simp add: inj_on_def)
next
  have "R. R  (rcosets stabilizer G φ x)  φ (inv (SOME h. h  R)) x  orbit G φ x "
  proof -
    fix R assume R: "R  (rcosets stabilizer G φ x)"
    then obtain g where g: "g  R"
      using assms stab_rcosets_not_empty by auto
    hence "φ (inv (SOME h. h  R)) x = φ (inv g) x"
      using R  assms orbit_stab_fun_is_well_defined1 by blast
    thus "φ (inv (SOME h. h  R)) x  orbit G φ x" unfolding orbit_def
      using subgroup.rcosets_carrier group_hom group_hom.axioms(1)
            g R assms stabilizer_subgroup by fastforce
  qed
  moreover have "orbit G φ x  (λR. φ (inv (SOME h. h  R)) x) ` (rcosets stabilizer G φ x)"
    using assms orbit_stab_fun_is_surj by fastforce
  ultimately show "(λR. φ (inv (SOME h. h  R)) x) ` (rcosets stabilizer G φ x) = orbit G φ x "
    using assms set_eq_subset by blast
qed


subsubsection ‹The Theorem›

theorem (in group_action) orbit_stabilizer_theorem:
  assumes "x  E"
  shows "card (orbit G φ x) * card (stabilizer G φ x) = order G"
proof -
  have "card (rcosets stabilizer G φ x) = card (orbit G φ x)"
    using orbit_stab_fun_is_bij[OF assms(1)] bij_betw_same_card by blast
  moreover have "card (rcosets stabilizer G φ x) * card (stabilizer G φ x) = order G"
    using stabilizer_subgroup assms group.lagrange group_hom group_hom.axioms(1) by blast
  ultimately show ?thesis by auto
qed



subsection ‹The Burnside's Lemma›

subsubsection ‹Sums and Cardinals›

lemma card_as_sums:
  assumes "A = {x  B. P x}" "finite B"
  shows "card A = (xB. (if P x then 1 else 0))"
proof -
  have "A  B" using assms(1) by blast
  have "card A = (xA. 1)" by simp
  also have " ... = (xA. (if P x then 1 else 0))"
    by (simp add: assms(1))
  also have " ... = (xA. (if P x then 1 else 0)) + (x(B - A). (if P x then 1 else 0))"
    using assms(1) by auto
  finally show "card A = (xB. (if P x then 1 else 0))"
    using A  B add.commute assms(2) sum.subset_diff by metis
qed

lemma sum_invertion:
  " finite A; finite B   (xA. yB. f x y) = (yB. xA. f x y)"
proof (induct set: finite)
  case empty thus ?case by simp
next
  case (insert x A')
  have "(xinsert x A'. yB. f x y) = (yB. f x y) + (xA'. yB. f x y)"
    by (simp add: insert.hyps)
  also have " ... = (yB. f x y) + (yB. xA'. f x y)"
    using insert.hyps by (simp add: insert.prems)
  also have " ... = (yB. (f x y) + (xA'. f x y))"
    by (simp add: sum.distrib)
  finally have "(xinsert x A'. yB. f x y) = (yB. xinsert x A'. f x y)"
    using sum.swap by blast
  thus ?case by simp
qed

lemma (in group_action) card_stablizer_sum:
  assumes "finite (carrier G)" "orb  (orbits G E φ)"
  shows "(x  orb. card (stabilizer G φ x)) = order G"
proof -
  obtain x where x:"x  E" and orb:"orb = orbit G φ x"
    using assms(2) unfolding orbits_def by blast
  have "y. y  orb  card (stabilizer G φ x) = card (stabilizer G φ y)"
  proof -
    fix y assume "y  orb"
    hence y: "y  E  y  orbit G φ x"
      using x orb assms(2) orbits_coverture by auto 
    hence same_orbit: "(orbit G φ x) = (orbit G φ y)"
      using disjoint_union[of "orbit G φ x" "orbit G φ y"] orbit_refl x
      unfolding orbits_def by auto
    have "card (orbit G φ x) * card (stabilizer G φ x) =
          card (orbit G φ y) * card (stabilizer G φ y)"
      using y assms(1) x orbit_stabilizer_theorem by simp
    hence "card (orbit G φ x) * card (stabilizer G φ x) =
           card (orbit G φ x) * card (stabilizer G φ y)" using same_orbit by simp
    moreover have "orbit G φ x  {}  finite (orbit G φ x)"
      using y orbit_def[of G φ x] assms(1) by auto
    hence "card (orbit G φ x) > 0"
      by (simp add: card_gt_0_iff)
    ultimately show "card (stabilizer G φ x) = card (stabilizer G φ y)" by auto
  qed
  hence "(x  orb. card (stabilizer G φ x)) = (y  orb. card (stabilizer G φ x))" by auto
  also have " ... = card (stabilizer G φ x) * (y  orb. 1)" by simp
  also have " ... = card (stabilizer G φ x) * card (orbit G φ x)"
    using orb by auto
  finally show "(x  orb. card (stabilizer G φ x)) = order G"
    by (metis mult.commute orbit_stabilizer_theorem x)
qed


subsubsection ‹The Lemma›

theorem (in group_action) burnside:
  assumes "finite (carrier G)" "finite E"
  shows "card (orbits G E φ) * order G = (g  carrier G. card(invariants E φ g))"
proof -
  have "(g  carrier G. card(invariants E φ g)) =
        (g  carrier G. x  E. (if (φ g) x = x then 1 else 0))"
    by (simp add: assms(2) card_as_sums invariants_def)
  also have " ... = (x  E. g  carrier G. (if (φ g) x = x then 1 else 0))"
    using sum_invertion[where ?f = "λ g x. (if (φ g) x = x then 1 else 0)"] assms by auto
  also have " ... = (x  E. card (stabilizer G φ x))"
    by (simp add: assms(1) card_as_sums stabilizer_def)
  also have " ... = (orbit  (orbits G E φ). x  orbit. card (stabilizer G φ x))"
    using disjoint_sum orbits_coverture assms(2) by metis
  also have " ... = (orbit  (orbits G E φ). order G)"
    by (simp add: assms(1) card_stablizer_sum)
  finally have "(g  carrier G. card(invariants E φ g)) = card (orbits G E φ) * order G" by simp
  thus ?thesis by simp
qed



subsection ‹Action by Conjugation›


subsubsection ‹Action Over Itself›

text ‹A Group Acts by Conjugation Over Itself›

lemma (in group) conjugation_is_inj:
  assumes "g  carrier G" "h1  carrier G" "h2  carrier G"
    and "g  h1  (inv g) = g  h2  (inv g)"
    shows "h1 = h2"
  using assms by auto

lemma (in group) conjugation_is_surj:
  assumes "g  carrier G" "h  carrier G"
  shows "g  ((inv g)  h  g)  (inv g) = h"
  using assms m_assoc inv_closed inv_inv m_closed monoid_axioms r_inv r_one
  by metis

lemma (in group) conjugation_is_bij:
  assumes "g  carrier G"
  shows "bij_betw (λh  carrier G. g  h  (inv g)) (carrier G) (carrier G)"
         (is "bij_betw  (carrier G) (carrier G)")
  unfolding bij_betw_def
proof
  show "inj_on  (carrier G)"
    using conjugation_is_inj by (simp add: assms inj_on_def) 
next
  have S: " h. h  carrier G  (inv g)  h  g  carrier G"
    using assms by blast
  have " h. h  carrier G   ((inv g)  h  g) = h"
    using assms by (simp add: conjugation_is_surj)
  hence "carrier G   ` carrier G"
    using S image_iff by fastforce
  moreover have " h. h  carrier G   h  carrier G"
    using assms by simp
  hence " ` carrier G  carrier G" by blast
  ultimately show " ` carrier G = carrier G" by blast
qed

lemma(in group) conjugation_is_hom:
  "(λg. λh  carrier G. g  h  inv g)  hom G (BijGroup (carrier G))"
  unfolding hom_def
proof -
  let  = "λg. λh. g  h  inv g"
  let  = "λg. restrict ( g) (carrier G)"

  (* First, we prove that ?φ: G → Bij(G) is well defined *)
  have Step0: " g. g  carrier G  ( g)  Bij (carrier G)"
    using Bij_def conjugation_is_bij by fastforce
  hence Step1: ": carrier G  carrier (BijGroup (carrier G))"
    unfolding BijGroup_def by simp

  (* Second, we prove that ?φ is a homomorphism *)
  have " g1 g2.  g1  carrier G; g2  carrier G  
                  ( h. h  carrier G   (g1  g2) h = ( g1) (( g2) h))"
  proof -
    fix g1 g2 h assume g1: "g1  carrier G" and g2: "g2  carrier G" and h: "h  carrier G"
    have "inv (g1  g2) = (inv g2)  (inv g1)"
      using g1 g2 by (simp add: inv_mult_group)
    thus " (g1  g2) h  = ( g1) (( g2) h)"
      by (simp add: g1 g2 h m_assoc)
  qed
  hence " g1 g2.  g1  carrier G; g2  carrier G  
         (λ h  carrier G.  (g1  g2) h) = (λ h  carrier G. ( g1) (( g2) h))" by auto
  hence Step2: " g1 g2.  g1  carrier G; g2  carrier G  
                 (g1  g2) = ( g1) BijGroup (carrier G)( g2)"
    unfolding BijGroup_def by (simp add: Step0 compose_def)

  (* Finally, we combine both results to prove the lemma *)
  thus "  {h: carrier G  carrier (BijGroup (carrier G)).
              (x  carrier G. y  carrier G. h (x  y) = h x BijGroup (carrier G)h y)}"
    using Step1 Step2 by auto
qed

theorem (in group) action_by_conjugation:
  "group_action G (carrier G) (λg. (λh  carrier G. g  h  (inv g)))"
  unfolding group_action_def group_hom_def using conjugation_is_hom
  by (simp add: group_BijGroup group_hom_axioms.intro is_group)


subsubsection ‹Action Over The Set of Subgroups›

text ‹A Group Acts by Conjugation Over The Set of Subgroups›

lemma (in group) subgroup_conjugation_is_inj_aux:
  assumes "g  carrier G" "H1  carrier G" "H2  carrier G"
    and "g <# H1 #> (inv g) = g <# H2 #> (inv g)"
    shows "H1  H2"
proof
  fix h1 assume h1: "h1  H1"
  hence "g  h1  (inv g)  g <# H1 #> (inv g)"
    unfolding l_coset_def r_coset_def using assms by blast
  hence "g  h1  (inv g)  g <# H2 #> (inv g)"
    using assms by auto
  hence "h2  H2. g  h1  (inv g) = g  h2  (inv g)"
      unfolding l_coset_def r_coset_def by blast
  then obtain h2 where "h2  H2  g  h1  (inv g) = g  h2  (inv g)" by blast
  thus "h1  H2"
    using assms conjugation_is_inj h1 by blast
qed

lemma (in group) subgroup_conjugation_is_inj:
  assumes "g  carrier G" "H1  carrier G" "H2  carrier G"
    and "g <# H1 #> (inv g) = g <# H2 #> (inv g)"
    shows "H1 = H2"
  using subgroup_conjugation_is_inj_aux assms set_eq_subset by metis

lemma (in group) subgroup_conjugation_is_surj0:
  assumes "g  carrier G" "H  carrier G"
  shows "g <# ((inv g) <# H #> g) #> (inv g) = H"
  using coset_assoc assms coset_mult_assoc l_coset_subset_G lcos_m_assoc
  by (simp add: lcos_mult_one)

lemma (in group) subgroup_conjugation_is_surj1:
  assumes "g  carrier G" "subgroup H G"
  shows "subgroup ((inv g) <# H #> g) G"
proof
  show "𝟭  inv g <# H #> g"
  proof -
    have "𝟭  H" by (simp add: assms(2) subgroup.one_closed)
    hence "inv g  𝟭  g  inv g <# H #> g"
      unfolding l_coset_def r_coset_def by blast
    thus "𝟭  inv g <# H #> g" using assms by simp
  qed
next
  show "inv g <# H #> g  carrier G"
  proof
    fix x assume "x  inv g <# H #> g"
    hence "h  H. x = (inv g)  h  g"
      unfolding r_coset_def l_coset_def by blast
    hence "h  (carrier G). x = (inv g)  h  g"
      by (meson assms subgroup.mem_carrier)
    thus "x  carrier G" using assms by blast
  qed
next
  show "  x y.  x  inv g <# H #> g; y  inv g <# H #> g   x  y  inv g <# H #> g"
  proof -
    fix x y assume "x  inv g <# H #> g"  "y  inv g <# H #> g"
    then obtain h1 h2 where h12: "h1  H" "h2  H" and "x = (inv g)  h1  g  y = (inv g)  h2  g"
      unfolding l_coset_def r_coset_def by blast
    hence "x  y = ((inv g)  h1  g)  ((inv g)  h2  g)" by blast
    also have " = ((inv g)  h1  (g  inv g)  h2  g)"
      using h12 assms inv_closed  m_assoc m_closed subgroup.mem_carrier [OF subgroup H G] by presburger 
    also have " = ((inv g)  (h1  h2)  g)"
      by (simp add: h12 assms m_assoc subgroup.mem_carrier [OF subgroup H G])
    finally have " h  H. x  y = (inv g)  h  g"
      by (meson assms(2) h12 subgroup_def)
    thus "x  y  inv g <# H #> g"
      unfolding l_coset_def r_coset_def by blast
  qed
next
  show "x. x  inv g <# H #> g  inv x  inv g <# H #> g"
  proof -
    fix x assume "x  inv g <# H #> g"
    hence "h  H. x = (inv g)  h  g"
      unfolding r_coset_def l_coset_def by blast
    then obtain h where h: "h  H  x = (inv g)  h  g" by blast
    hence "x  (inv g)  (inv h)  g = 𝟭"
      using assms m_assoc monoid_axioms by (simp add: subgroup.mem_carrier)
    hence "inv x = (inv g)  (inv h)  g"
      using assms h inv_mult_group m_assoc monoid_axioms by (simp add: subgroup.mem_carrier)
    moreover have "inv h  H"
      by (simp add: assms h subgroup.m_inv_closed)
    ultimately show "inv x  inv g <# H #> g" unfolding r_coset_def l_coset_def by blast
  qed
qed

lemma (in group) subgroup_conjugation_is_surj2:
  assumes "g  carrier G" "subgroup H G"
  shows "subgroup (g <# H #> (inv g)) G"
  using subgroup_conjugation_is_surj1 by (metis assms inv_closed inv_inv)

lemma (in group) subgroup_conjugation_is_bij:
  assumes "g  carrier G"
  shows "bij_betw (λH  {H. subgroup H G}. g <# H #> (inv g)) {H. subgroup H G} {H. subgroup H G}"
         (is "bij_betw  {H. subgroup H G} {H. subgroup H G}")
  unfolding bij_betw_def
proof
  show "inj_on  {H. subgroup H G}"
    using subgroup_conjugation_is_inj assms inj_on_def subgroup.subset
    by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq)
next
  have "H. H  {H. subgroup H G}   ((inv g) <# H #> g) = H"
    by (simp add: assms subgroup.subset subgroup_conjugation_is_surj0
                  subgroup_conjugation_is_surj1 is_group)
  hence "H. H  {H. subgroup H G}  H'  {H. subgroup H G}.  H' = H"
    using assms subgroup_conjugation_is_surj1 by fastforce
  thus " ` {H. subgroup H G} = {H. subgroup H G}"
    using subgroup_conjugation_is_surj2 assms by auto
qed

lemma (in group) subgroup_conjugation_is_hom:
  "(λg. λH  {H. subgroup H G}. g <# H #> (inv g))  hom G (BijGroup {H. subgroup H G})"
  unfolding hom_def
proof -
  (* We follow the exact same structure of conjugation_is_hom's proof *)
  let  = "λg. λH. g <# H #> (inv g)"
  let  = "λg. restrict ( g) {H. subgroup H G}"

  have Step0: " g. g  carrier G  ( g)  Bij {H. subgroup H G}"
    using Bij_def subgroup_conjugation_is_bij by fastforce
  hence Step1: ": carrier G  carrier (BijGroup {H. subgroup H G})"
    unfolding BijGroup_def by simp

  have " g1 g2.  g1  carrier G; g2  carrier G  
                  ( H. H  {H. subgroup H G}   (g1  g2) H = ( g1) (( g2) H))"
  proof -
    fix g1 g2 H assume g1: "g1  carrier G" and g2: "g2  carrier G" and H': "H  {H. subgroup H G}"
    hence H: "subgroup H G" by simp
    have "( g1) (( g2) H) = g1 <# (g2 <# H #> (inv g2)) #> (inv g1)"
      by (simp add: H g2 subgroup_conjugation_is_surj2)
    also have " ... = g1 <# (g2 <# H) #> ((inv g2)  (inv g1))"
      by (simp add: H coset_mult_assoc g1 g2 group.coset_assoc
                    is_group l_coset_subset_G subgroup.subset)
    also have " ... = g1 <# (g2 <# H) #> inv (g1  g2)"
      using g1 g2 by (simp add: inv_mult_group)
    finally have "( g1) (( g2) H) =  (g1  g2) H"
      by (simp add: H g1 g2 lcos_m_assoc subgroup.subset)
    thus " (g1  g2) H = ( g1) (( g2) H)" by auto
  qed
  hence " g1 g2.  g1  carrier G; g2  carrier G  
         (λH  {H. subgroup H G}.  (g1  g2) H) = (λH  {H. subgroup H G}. ( g1) (( g2) H))"
    by (meson restrict_ext)
  hence Step2: " g1 g2.  g1  carrier G; g2  carrier G  
                 (g1  g2) = ( g1) BijGroup {H. subgroup H G}( g2)"
    unfolding BijGroup_def by (simp add: Step0 compose_def)

  show "  {h: carrier G  carrier (BijGroup {H. subgroup H G}).
              xcarrier G. ycarrier G. h (x  y) = h x BijGroup {H. subgroup H G}h y}"
    using Step1 Step2 by auto
qed

theorem (in group) action_by_conjugation_on_subgroups_set:
  "group_action G {H. subgroup H G} (λg. λH  {H. subgroup H G}. g <# H #> (inv g))"
  unfolding group_action_def group_hom_def using subgroup_conjugation_is_hom
  by (simp add: group_BijGroup group_hom_axioms.intro is_group)


subsubsection ‹Action Over The Power Set›

text ‹A Group Acts by Conjugation Over The Power Set›

lemma (in group) subset_conjugation_is_bij:
  assumes "g  carrier G"
  shows "bij_betw (λH  {H. H  carrier G}. g <# H #> (inv g)) {H. H  carrier G} {H. H  carrier G}"
         (is "bij_betw  {H. H  carrier G} {H. H  carrier G}")
  unfolding bij_betw_def
proof
  show "inj_on  {H. H  carrier G}"
    using subgroup_conjugation_is_inj assms inj_on_def
    by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq)
next
  have "H. H  {H. H  carrier G}   ((inv g) <# H #> g) = H"
    by (simp add: assms l_coset_subset_G r_coset_subset_G subgroup_conjugation_is_surj0)
  hence "H. H  {H. H  carrier G}  H'  {H. H  carrier G}.  H' = H"
    by (metis assms l_coset_subset_G mem_Collect_eq r_coset_subset_G subgroup_def subgroup_self)
  hence "{H. H  carrier G}   ` {H. H  carrier G}" by blast
  moreover have " ` {H. H  carrier G}  {H. H  carrier G}"
    by clarsimp (meson assms contra_subsetD inv_closed l_coset_subset_G r_coset_subset_G)
  ultimately show " ` {H. H  carrier G} = {H. H  carrier G}" by simp
qed

lemma (in group) subset_conjugation_is_hom:
  "(λg. λH  {H. H  carrier G}. g <# H #> (inv g))  hom G (BijGroup {H. H  carrier G})"
  unfolding hom_def
proof -
  (* We follow the exact same structure of conjugation_is_hom's proof *)
  let  = "λg. λH. g <# H #> (inv g)"
  let  = "λg. restrict ( g) {H. H  carrier G}"

  have Step0: " g. g  carrier G  ( g)  Bij {H. H  carrier G}"
    using Bij_def subset_conjugation_is_bij by fastforce
  hence Step1: ": carrier G  carrier (BijGroup {H. H  carrier G})"
    unfolding BijGroup_def by simp

  have " g1 g2.  g1  carrier G; g2  carrier G  
                  ( H. H  {H. H  carrier G}   (g1  g2) H = ( g1) (( g2) H))"
  proof -
    fix g1 g2 H assume g1: "g1  carrier G" and g2: "g2  carrier G" and H: "H  {H. H  carrier G}"
    hence "( g1) (( g2) H) = g1 <# (g2 <# H #> (inv g2)) #> (inv g1)"
      using l_coset_subset_G r_coset_subset_G by auto
    also have " ... = g1 <# (g2 <# H) #> ((inv g2)  (inv g1))"
      using H coset_assoc coset_mult_assoc g1 g2 l_coset_subset_G by auto
    also have " ... = g1 <# (g2 <# H) #> inv (g1  g2)"
      using g1 g2 by (simp add: inv_mult_group)
    finally have "( g1) (( g2) H) =  (g1  g2) H"
      using H g1 g2 lcos_m_assoc by force
    thus " (g1  g2) H = ( g1) (( g2) H)" by auto
  qed
  hence " g1 g2.  g1  carrier G; g2  carrier G  
         (λH  {H. H  carrier G}.  (g1  g2) H) = (λH  {H. H  carrier G}. ( g1) (( g2) H))"
    by (meson restrict_ext)
  hence Step2: " g1 g2.  g1  carrier G; g2  carrier G  
                 (g1  g2) = ( g1) BijGroup {H. H  carrier G}( g2)"
    unfolding BijGroup_def by (simp add: Step0 compose_def)

  show "  {h: carrier G  carrier (BijGroup {H. H  carrier G}).
              xcarrier G. ycarrier G. h (x  y) = h x BijGroup {H. H  carrier G}h y}"
    using Step1 Step2 by auto
qed

theorem (in group) action_by_conjugation_on_power_set:
  "group_action G {H. H  carrier G} (λg. λH  {H. H  carrier G}. g <# H #> (inv g))"
  unfolding group_action_def group_hom_def using subset_conjugation_is_hom
  by (simp add: group_BijGroup group_hom_axioms.intro is_group)

corollary (in group) normalizer_imp_subgroup:
  assumes "H  carrier G"
  shows "subgroup (normalizer G H) G"
  unfolding normalizer_def
  using group_action.stabilizer_subgroup[OF action_by_conjugation_on_power_set] assms by auto


subsection ‹Subgroup of an Acting Group›

text ‹A Subgroup of an Acting Group Induces an Action›

lemma (in group_action) induced_homomorphism:
  assumes "subgroup H G"
  shows "φ  hom (G carrier := H) (BijGroup E)"
  unfolding hom_def apply simp
proof -
  have S0: "H  carrier G" by (meson assms subgroup_def)
  hence "φ: H  carrier (BijGroup E)"
    by (simp add: BijGroup_def bij_prop0 subset_eq)
  thus "φ: H  carrier (BijGroup E)  (x  H. y  H. φ (x  y) = φ x BijGroup Eφ y)"
    by (simp add: S0  group_hom group_hom.hom_mult rev_subsetD)
qed

theorem (in group_action) induced_action:
  assumes "subgroup H G"
  shows "group_action (G carrier := H) E φ"
  unfolding group_action_def group_hom_def
  using induced_homomorphism assms group.subgroup_imp_group group_BijGroup
        group_hom group_hom.axioms(1) group_hom_axioms_def by blast

end