Quelle Group_Action.thy Sprache: Isabelle

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

theory Group_Action
imports Bij Coset Congruence
begin

section \<open>Group Actions\<close>

locale group_action =
  fixes G (structure) and E and \<phi>
  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 (\<lambda>g. \<lambda>H \<in> {H. H \<subseteq> carrier G}. g <#\<^bsub>G\<^esub> H #>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> g)) 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 \<open>Prelimineries\<close>

text \<open>Some simple lemmas to make group action's properties more explicit\<close>

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 \<open>g \<in> carrier G\<close> 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) \\<^bsub>BijGroup E\<^esub> (\ 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 \<open>Orbits\<close>

text\<open>We prove here that orbits form an equivalence relation\<close>

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)) \\<^bsub>BijGroup E\<^esub> (\ g)) x"
    by (simp add: BijGroup_def assms(1) bij_prop0)
  also have " ... = (\ ((inv g) \ g)) x"
    by (metis \<open>inv g \<in> carrier G\<close> 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) \\<^bsub>BijGroup E\<^esub> (\ 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\<^bsub>\ carrier = E, eq = \x. \y. y \ orbit G \ x \\<^esub> = 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 \). \x\orb. f x) = (\x\E. f x)"
  using partition.disjoint_sum[OF orbit_partition] assms by auto

subsubsection \<open>Transitive Actions\<close>

text \<open>Transitive actions have only one orbit\<close>

lemma (in transitive_action) all_equivalent:
  "\ x \ E; y \ E \ \ x .=\<^bsub>\carrier = E, eq = \x y. y \ orbit G \ x\\<^esub> y"
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 .=\<^bsub>\carrier = E, eq = \x y. y \ orbit G \ x\\<^esub> y" 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 \<open>Stabilizers\<close>

text \<open>We show that stabilizers are subgroups from the acting group\<close>

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 \<open>The Orbit-Stabilizer Theorem\<close>

text \<open>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 \<open>Rcosets - Supporting Lemmas\<close>

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 \<open>Bijection Between Rcosets and an Orbit - Definition and Supporting Lemmas\<close>

(* 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 \<rightarrow> lcosets, s.t. f R = (\<lambda>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 = (\ (inv\<^bsub>G\<^esub> (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 \<open>The Theorem\<close>

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 \<open>The Burnside's Lemma\<close>

subsubsection \<open>Sums and Cardinals\<close>

lemma card_as_sums:
  assumes "A = {x \ B. P x}" "finite B"
  shows "card A = (\x\B. (if P x then 1 else 0))"
proof -
  have "A \ B" using assms(1) by blast
  have "card A = (\x\A. 1)" by simp
  also have " ... = (\x\A. (if P x then 1 else 0))"
    by (simp add: assms(1))
  also have " ... = (\x\A. (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 = (\x\B. (if P x then 1 else 0))"
    using \<open>A \<subseteq> B\<close> add.commute assms(2) sum.subset_diff by metis
qed

lemma sum_invertion:
  "\ finite A; finite B \ \ (\x\A. \y\B. f x y) = (\y\B. \x\A. f x y)"
proof (induct set: finite)
  case empty thus ?case by simp
next
  case (insert x A')
  have "(\x\insert x A'. \y\B. f x y) = (\y\B. f x y) + (\x\A'. \y\B. f x y)"
    by (simp add: insert.hyps)
  also have " ... = (\y\B. f x y) + (\y\B. \x\A'. f x y)"
    using insert.hyps by (simp add: insert.prems)
  also have " ... = (\y\B. (f x y) + (\x\A'. f x y))"
    by (simp add: sum.distrib)
  finally have "(\x\insert x A'. \y\B. f x y) = (\y\B. \x\insert 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 \<phi> y) * card (stabilizer G \<phi> y)"
      using y assms(1) x orbit_stabilizer_theorem by simp
    hence "card (orbit G \ x) * card (stabilizer G \ x) =
           card (orbit G \<phi> x) * card (stabilizer G \<phi> y)" using same_orbit by simp
    moreover have "orbit G \ x \ {} \ finite (orbit G \ x)"
      using y orbit_def[of G \<phi> 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 \<open>The Lemma\<close>

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)) =
        (\<Sum>g \<in> carrier G. \<Sum>x \<in> E. (if (\<phi> 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 \<open>Action by Conjugation\<close>

subsubsection \<open>Action Over Itself\<close>

text \<open>A Group Acts by Conjugation Over Itself\<close>

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 ?\<psi> = "\<lambda>g. \<lambda>h. g \<otimes> h \<otimes> inv g"
  let ?\<phi> = "\<lambda>g. restrict (?\<psi> g) (carrier G)"

  (* First, we prove that ?\<phi>: G \<rightarrow> 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 ?\<phi> is a homomorphism *)
  have "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \
                  (\<And> h. h \<in> carrier G \<Longrightarrow> ?\<psi> (g1 \<otimes> g2) h = (?\<phi> g1) ((?\<phi> 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 \ \
         (\<lambda> h \<in> carrier G. ?\<psi> (g1 \<otimes> g2) h) = (\<lambda> h \<in> carrier G. (?\<phi> g1) ((?\<phi> g2) h))" by auto
  hence Step2: "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \
                ?\<phi> (g1 \<otimes> g2) = (?\<phi> g1) \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> (?\<phi> 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)).
              (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> 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 \<open>Action Over The Set of Subgroups\<close>

text \<open>A Group Acts by Conjugation Over The Set of Subgroups\<close>

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 \<open>subgroup H G\<close>] by presburger
    also have "\ = ((inv g) \ (h1 \ h2) \ g)"
      by (simp add: h12 assms m_assoc subgroup.mem_carrier [OF \<open>subgroup H G\<close>])
    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 ?\<psi> = "\<lambda>g. \<lambda>H. g <# H #> (inv g)"
  let ?\<phi> = "\<lambda>g. restrict (?\<psi> 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 \ \
                  (\<And> H. H \<in> {H. subgroup H G} \<Longrightarrow> ?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> 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 \ \
         (\<lambda>H \<in> {H. subgroup H G}. ?\<psi> (g1 \<otimes> g2) H) = (\<lambda>H \<in> {H. subgroup H G}. (?\<phi> g1) ((?\<phi> g2) H))"
    by (meson restrict_ext)
  hence Step2: "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \
                ?\<phi> (g1 \<otimes> g2) = (?\<phi> g1) \<otimes>\<^bsub>BijGroup {H. subgroup H G}\<^esub> (?\<phi> g2)"
    unfolding BijGroup_def by (simp add: Step0 compose_def)

  show "?\ \ {h: carrier G \ carrier (BijGroup {H. subgroup H G}).
              \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h (x \<otimes> y) = h x \<otimes>\<^bsub>BijGroup {H. subgroup H G}\<^esub> 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 \<open>Action Over The Power Set\<close>

text \<open>A Group Acts by Conjugation Over The Power Set\<close>

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 ?\<psi> = "\<lambda>g. \<lambda>H. g <# H #> (inv g)"
  let ?\<phi> = "\<lambda>g. restrict (?\<psi> g) {H. H \<subseteq> 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 \ \
                  (\<And> H. H \<in> {H. H \<subseteq> carrier G} \<Longrightarrow> ?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> 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 \ \
         (\<lambda>H \<in> {H. H \<subseteq> carrier G}. ?\<psi> (g1 \<otimes> g2) H) = (\<lambda>H \<in> {H. H \<subseteq> carrier G}. (?\<phi> g1) ((?\<phi> g2) H))"
    by (meson restrict_ext)
  hence Step2: "\ g1 g2. \ g1 \ carrier G; g2 \ carrier G \ \
                ?\<phi> (g1 \<otimes> g2) = (?\<phi> g1) \<otimes>\<^bsub>BijGroup {H. H \<subseteq> carrier G}\<^esub> (?\<phi> g2)"
    unfolding BijGroup_def by (simp add: Step0 compose_def)

  show "?\ \ {h: carrier G \ carrier (BijGroup {H. H \ carrier G}).
              \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h (x \<otimes> y) = h x \<otimes>\<^bsub>BijGroup {H. H \<subseteq> carrier G}\<^esub> 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 \<open>Subgroup of an Acting Group\<close>

text \<open>A Subgroup of an Acting Group Induces an Action\<close>

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 \\<^bsub>BijGroup E\<^esub> \ 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

quality100%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.