|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
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
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
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.
|
|
|
|
|
|
