(* 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 <#⇘G⇙ H #>⇘G⇙ (inv⇘G⇙ 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 ‹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 φ). ∑x∈orb. f x) = (∑x∈E. 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 φ x⦈⇙ 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 .=⇘⦇carrier = E, eq = λx y. y ∈ orbit G φ x⦈⇙ 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 ‹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 = (φ (inv⇘G⇙ (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 = (∑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 ‹A ⊆ B› 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 φ 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}). ∀x∈carrier G. ∀y∈carrier 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}). ∀x∈carrier G. ∀y∈carrier 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