src/HOL/Algebra/Group_Action.thy
 author wenzelm Tue Jul 03 11:00:37 2018 +0200 (13 months ago) changeset 68582 b9b9e2985878 parent 68517 6b5f15387353 child 68606 96a49db47c97 permissions -rw-r--r--
more standard headers;
tuned whitespace;
```     1 (*  Title:      HOL/Algebra/Group_Action.thy
```
```     2     Author:     Paulo Emílio de Vilhena
```
```     3 *)
```
```     4
```
```     5 theory Group_Action
```
```     6 imports Bij Coset Congruence
```
```     7 begin
```
```     8
```
```     9 section \<open>Group Actions\<close>
```
```    10
```
```    11 locale group_action =
```
```    12   fixes G (structure) and E and \<phi>
```
```    13   assumes group_hom: "group_hom G (BijGroup E) \<phi>"
```
```    14
```
```    15 definition
```
```    16   orbit :: "[_, 'a \<Rightarrow> 'b \<Rightarrow> 'b, 'b] \<Rightarrow> 'b set"
```
```    17   where "orbit G \<phi> x = {(\<phi> g) x | g. g \<in> carrier G}"
```
```    18
```
```    19 definition
```
```    20   orbits :: "[_, 'b set, 'a \<Rightarrow> 'b \<Rightarrow> 'b] \<Rightarrow> ('b set) set"
```
```    21   where "orbits G E \<phi> = {orbit G \<phi> x | x. x \<in> E}"
```
```    22
```
```    23 definition
```
```    24   stabilizer :: "[_, 'a \<Rightarrow> 'b \<Rightarrow> 'b, 'b] \<Rightarrow> 'a set"
```
```    25   where "stabilizer G \<phi> x = {g \<in> carrier G. (\<phi> g) x = x}"
```
```    26
```
```    27 definition
```
```    28   invariants :: "['b set, 'a \<Rightarrow> 'b \<Rightarrow> 'b, 'a] \<Rightarrow> 'b set"
```
```    29   where "invariants E \<phi> g = {x \<in> E. (\<phi> g) x = x}"
```
```    30
```
```    31 definition
```
```    32   normalizer :: "[_, 'a set] \<Rightarrow> 'a set"
```
```    33   where "normalizer G H =
```
```    34          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"
```
```    35
```
```    36 locale faithful_action = group_action +
```
```    37   assumes faithful: "inj_on \<phi> (carrier G)"
```
```    38
```
```    39 locale transitive_action = group_action +
```
```    40   assumes unique_orbit: "\<lbrakk> x \<in> E; y \<in> E \<rbrakk> \<Longrightarrow> \<exists>g \<in> carrier G. (\<phi> g) x = y"
```
```    41
```
```    42
```
```    43
```
```    44 subsection \<open>Prelimineries\<close>
```
```    45
```
```    46 text \<open>Some simple lemmas to make group action's properties more explicit\<close>
```
```    47
```
```    48 lemma (in group_action) id_eq_one: "(\<lambda>x \<in> E. x) = \<phi> \<one>"
```
```    49   by (metis BijGroup_def group_hom group_hom.hom_one select_convs(2))
```
```    50
```
```    51 lemma (in group_action) bij_prop0:
```
```    52   "\<And> g. g \<in> carrier G \<Longrightarrow> (\<phi> g) \<in> Bij E"
```
```    53   by (metis BijGroup_def group_hom group_hom.hom_closed partial_object.select_convs(1))
```
```    54
```
```    55 lemma (in group_action) surj_prop:
```
```    56   "\<And> g. g \<in> carrier G \<Longrightarrow> (\<phi> g) ` E = E"
```
```    57   using bij_prop0 by (simp add: Bij_def bij_betw_def)
```
```    58
```
```    59 lemma (in group_action) inj_prop:
```
```    60   "\<And> g. g \<in> carrier G \<Longrightarrow> inj_on (\<phi> g) E"
```
```    61   using bij_prop0 by (simp add: Bij_def bij_betw_def)
```
```    62
```
```    63 lemma (in group_action) bij_prop1:
```
```    64   "\<And> g y. \<lbrakk> g \<in> carrier G; y \<in> E \<rbrakk> \<Longrightarrow>  \<exists>!x \<in> E. (\<phi> g) x = y"
```
```    65 proof -
```
```    66   fix g y assume "g \<in> carrier G" "y \<in> E"
```
```    67   hence "\<exists>x \<in> E. (\<phi> g) x = y"
```
```    68     using surj_prop by force
```
```    69   moreover have "\<And> x1 x2. \<lbrakk> x1 \<in> E; x2 \<in> E \<rbrakk> \<Longrightarrow> (\<phi> g) x1 = (\<phi> g) x2 \<Longrightarrow> x1 = x2"
```
```    70     using inj_prop by (meson \<open>g \<in> carrier G\<close> inj_on_eq_iff)
```
```    71   ultimately show "\<exists>!x \<in> E. (\<phi> g) x = y"
```
```    72     by blast
```
```    73 qed
```
```    74
```
```    75 lemma (in group_action) composition_rule:
```
```    76   assumes "x \<in> E" "g1 \<in> carrier G" "g2 \<in> carrier G"
```
```    77   shows "\<phi> (g1 \<otimes> g2) x = (\<phi> g1) (\<phi> g2 x)"
```
```    78 proof -
```
```    79   have "\<phi> (g1 \<otimes> g2) x = ((\<phi> g1) \<otimes>\<^bsub>BijGroup E\<^esub> (\<phi> g2)) x"
```
```    80     using assms(2) assms(3) group_hom group_hom.hom_mult by fastforce
```
```    81   also have " ... = (compose E (\<phi> g1) (\<phi> g2)) x"
```
```    82     unfolding BijGroup_def by (simp add: assms bij_prop0)
```
```    83   finally show "\<phi> (g1 \<otimes> g2) x = (\<phi> g1) (\<phi> g2 x)"
```
```    84     by (simp add: assms(1) compose_eq)
```
```    85 qed
```
```    86
```
```    87 lemma (in group_action) element_image:
```
```    88   assumes "g \<in> carrier G" and "x \<in> E" and "(\<phi> g) x = y"
```
```    89   shows "y \<in> E"
```
```    90   using surj_prop assms by blast
```
```    91
```
```    92
```
```    93
```
```    94 subsection \<open>Orbits\<close>
```
```    95
```
```    96 text\<open>We prove here that orbits form an equivalence relation\<close>
```
```    97
```
```    98 lemma (in group_action) orbit_sym_aux:
```
```    99   assumes "g \<in> carrier G"
```
```   100     and "x \<in> E"
```
```   101     and "(\<phi> g) x = y"
```
```   102   shows "(\<phi> (inv g)) y = x"
```
```   103 proof -
```
```   104   interpret group G
```
```   105     using group_hom group_hom.axioms(1) by auto
```
```   106   have "y \<in> E"
```
```   107     using element_image assms by simp
```
```   108   have "inv g \<in> carrier G"
```
```   109     by (simp add: assms(1))
```
```   110
```
```   111   have "(\<phi> (inv g)) y = (\<phi> (inv g)) ((\<phi> g) x)"
```
```   112     using assms(3) by simp
```
```   113   also have " ... = compose E (\<phi> (inv g)) (\<phi> g) x"
```
```   114     by (simp add: assms(2) compose_eq)
```
```   115   also have " ... = ((\<phi> (inv g)) \<otimes>\<^bsub>BijGroup E\<^esub> (\<phi> g)) x"
```
```   116     by (simp add: BijGroup_def assms(1) bij_prop0)
```
```   117   also have " ... = (\<phi> ((inv g) \<otimes> g)) x"
```
```   118     by (metis \<open>inv g \<in> carrier G\<close> assms(1) group_hom group_hom.hom_mult)
```
```   119   finally show "(\<phi> (inv g)) y = x"
```
```   120     by (metis assms(1) assms(2) id_eq_one l_inv restrict_apply)
```
```   121 qed
```
```   122
```
```   123 lemma (in group_action) orbit_refl:
```
```   124   "x \<in> E \<Longrightarrow> x \<in> orbit G \<phi> x"
```
```   125 proof -
```
```   126   assume "x \<in> E" hence "(\<phi> \<one>) x = x"
```
```   127     using id_eq_one by (metis restrict_apply')
```
```   128   thus "x \<in> orbit G \<phi> x" unfolding orbit_def
```
```   129     using group.is_monoid group_hom group_hom.axioms(1) by force
```
```   130 qed
```
```   131
```
```   132 lemma (in group_action) orbit_sym:
```
```   133   assumes "x \<in> E" and "y \<in> E" and "y \<in> orbit G \<phi> x"
```
```   134   shows "x \<in> orbit G \<phi> y"
```
```   135 proof -
```
```   136   have "\<exists> g \<in> carrier G. (\<phi> g) x = y"
```
```   137     by (smt assms(3) mem_Collect_eq orbit_def)
```
```   138   then obtain g where g: "g \<in> carrier G \<and> (\<phi> g) x = y" by blast
```
```   139   hence "(\<phi> (inv g)) y = x"
```
```   140     using orbit_sym_aux by (simp add: assms(1))
```
```   141   thus ?thesis
```
```   142     using g group_hom group_hom.axioms(1) orbit_def by fastforce
```
```   143 qed
```
```   144
```
```   145 lemma (in group_action) orbit_trans:
```
```   146   assumes "x \<in> E" "y \<in> E" "z \<in> E"
```
```   147     and "y \<in> orbit G \<phi> x" "z \<in> orbit G \<phi> y"
```
```   148   shows "z \<in> orbit G \<phi> x"
```
```   149 proof -
```
```   150   interpret group G
```
```   151     using group_hom group_hom.axioms(1) by auto
```
```   152
```
```   153   have "\<exists> g1 \<in> carrier G. (\<phi> g1) x = y"
```
```   154     by (smt assms mem_Collect_eq orbit_def)
```
```   155   then obtain g1 where g1: "g1 \<in> carrier G \<and> (\<phi> g1) x = y" by blast
```
```   156
```
```   157   have "\<exists> g2 \<in> carrier G. (\<phi> g2) y = z"
```
```   158     by (smt assms mem_Collect_eq orbit_def)
```
```   159   then obtain g2 where g2: "g2 \<in> carrier G \<and> (\<phi> g2) y = z" by blast
```
```   160
```
```   161   have "(\<phi> (g2 \<otimes> g1)) x = ((\<phi> g2) \<otimes>\<^bsub>BijGroup E\<^esub> (\<phi> g1)) x"
```
```   162     using g1 g2 group_hom group_hom.hom_mult by fastforce
```
```   163   also have " ... = (\<phi> g2) ((\<phi> g1) x)"
```
```   164     using composition_rule assms(1) calculation g1 g2 by auto
```
```   165   finally have "(\<phi> (g2 \<otimes> g1)) x = z"
```
```   166     by (simp add: g1 g2)
```
```   167   thus ?thesis
```
```   168     using g1 g2 orbit_def by force
```
```   169 qed
```
```   170
```
```   171 lemma (in group_action) orbits_as_classes:
```
```   172   "classes\<^bsub>\<lparr> carrier = E, eq = \<lambda>x. \<lambda>y. y \<in> orbit G \<phi> x \<rparr>\<^esub> = orbits G E \<phi>"
```
```   173   unfolding eq_classes_def eq_class_of_def orbits_def apply simp
```
```   174 proof -
```
```   175   have "\<And>x. x \<in> E \<Longrightarrow> {y \<in> E. y \<in> orbit G \<phi> x} = orbit G \<phi> x"
```
```   176     by (smt Collect_cong element_image mem_Collect_eq orbit_def)
```
```   177   thus "{{y \<in> E. y \<in> orbit G \<phi> x} |x. x \<in> E} = {orbit G \<phi> x |x. x \<in> E}" by blast
```
```   178 qed
```
```   179
```
```   180 theorem (in group_action) orbit_partition:
```
```   181   "partition E (orbits G E \<phi>)"
```
```   182 proof -
```
```   183   have "equivalence \<lparr> carrier = E, eq = \<lambda>x. \<lambda>y. y \<in> orbit G \<phi> x \<rparr>"
```
```   184   unfolding equivalence_def apply simp
```
```   185   using orbit_refl orbit_sym orbit_trans by blast
```
```   186   thus ?thesis using equivalence.partition_from_equivalence orbits_as_classes by fastforce
```
```   187 qed
```
```   188
```
```   189 corollary (in group_action) orbits_coverture:
```
```   190   "\<Union> (orbits G E \<phi>) = E"
```
```   191   using partition.partition_coverture[OF orbit_partition] by simp
```
```   192
```
```   193 corollary (in group_action) disjoint_union:
```
```   194   assumes "orb1 \<in> (orbits G E \<phi>)" "orb2 \<in> (orbits G E \<phi>)"
```
```   195   shows "(orb1 = orb2) \<or> (orb1 \<inter> orb2) = {}"
```
```   196   using partition.disjoint_union[OF orbit_partition] assms by auto
```
```   197
```
```   198 corollary (in group_action) disjoint_sum:
```
```   199   assumes "finite E"
```
```   200   shows "(\<Sum>orb\<in>(orbits G E \<phi>). \<Sum>x\<in>orb. f x) = (\<Sum>x\<in>E. f x)"
```
```   201   using partition.disjoint_sum[OF orbit_partition] assms by auto
```
```   202
```
```   203
```
```   204 subsubsection \<open>Transitive Actions\<close>
```
```   205
```
```   206 text \<open>Transitive actions have only one orbit\<close>
```
```   207
```
```   208 lemma (in transitive_action) all_equivalent:
```
```   209   "\<lbrakk> x \<in> E; y \<in> E \<rbrakk> \<Longrightarrow> x .=\<^bsub>\<lparr>carrier = E, eq = \<lambda>x y. y \<in> orbit G \<phi> x\<rparr>\<^esub> y"
```
```   210 proof -
```
```   211   assume "x \<in> E" "y \<in> E"
```
```   212   hence "\<exists> g \<in> carrier G. (\<phi> g) x = y"
```
```   213     using unique_orbit  by blast
```
```   214   hence "y \<in> orbit G \<phi> x"
```
```   215     using orbit_def by fastforce
```
```   216   thus "x .=\<^bsub>\<lparr>carrier = E, eq = \<lambda>x y. y \<in> orbit G \<phi> x\<rparr>\<^esub> y" by simp
```
```   217 qed
```
```   218
```
```   219 proposition (in transitive_action) one_orbit:
```
```   220   assumes "E \<noteq> {}"
```
```   221   shows "card (orbits G E \<phi>) = 1"
```
```   222 proof -
```
```   223   have "orbits G E \<phi> \<noteq> {}"
```
```   224     using assms orbits_coverture by auto
```
```   225   moreover have "\<And> orb1 orb2. \<lbrakk> orb1 \<in> (orbits G E \<phi>); orb2 \<in> (orbits G E \<phi>) \<rbrakk> \<Longrightarrow> orb1 = orb2"
```
```   226   proof -
```
```   227     fix orb1 orb2 assume orb1: "orb1 \<in> (orbits G E \<phi>)"
```
```   228                      and orb2: "orb2 \<in> (orbits G E \<phi>)"
```
```   229     then obtain x y where x: "orb1 = orbit G \<phi> x" and x_E: "x \<in> E"
```
```   230                       and y: "orb2 = orbit G \<phi> y" and y_E: "y \<in> E"
```
```   231       unfolding orbits_def by blast
```
```   232     hence "x \<in> orbit G \<phi> y" using all_equivalent by auto
```
```   233     hence "orb1 \<inter> orb2 \<noteq> {}" using x y x_E orbit_refl by auto
```
```   234     thus "orb1 = orb2" using disjoint_union[of orb1 orb2] orb1 orb2 by auto
```
```   235   qed
```
```   236   ultimately show "card (orbits G E \<phi>) = 1"
```
```   237     by (meson is_singletonI' is_singleton_altdef)
```
```   238 qed
```
```   239
```
```   240
```
```   241
```
```   242 subsection \<open>Stabilizers\<close>
```
```   243
```
```   244 text \<open>We show that stabilizers are subgroups from the acting group\<close>
```
```   245
```
```   246 lemma (in group_action) stabilizer_subset:
```
```   247   "stabilizer G \<phi> x \<subseteq> carrier G"
```
```   248   by (metis (no_types, lifting) mem_Collect_eq stabilizer_def subsetI)
```
```   249
```
```   250 lemma (in group_action) stabilizer_m_closed:
```
```   251   assumes "x \<in> E" "g1 \<in> (stabilizer G \<phi> x)" "g2 \<in> (stabilizer G \<phi> x)"
```
```   252   shows "(g1 \<otimes> g2) \<in> (stabilizer G \<phi> x)"
```
```   253 proof -
```
```   254   interpret group G
```
```   255     using group_hom group_hom.axioms(1) by auto
```
```   256
```
```   257   have "\<phi> g1 x = x"
```
```   258     using assms stabilizer_def by fastforce
```
```   259   moreover have "\<phi> g2 x = x"
```
```   260     using assms stabilizer_def by fastforce
```
```   261   moreover have g1: "g1 \<in> carrier G"
```
```   262     by (meson assms contra_subsetD stabilizer_subset)
```
```   263   moreover have g2: "g2 \<in> carrier G"
```
```   264     by (meson assms contra_subsetD stabilizer_subset)
```
```   265   ultimately have "\<phi> (g1 \<otimes> g2) x = x"
```
```   266     using composition_rule assms by simp
```
```   267
```
```   268   thus ?thesis
```
```   269     by (simp add: g1 g2 stabilizer_def)
```
```   270 qed
```
```   271
```
```   272 lemma (in group_action) stabilizer_one_closed:
```
```   273   assumes "x \<in> E"
```
```   274   shows "\<one> \<in> (stabilizer G \<phi> x)"
```
```   275 proof -
```
```   276   have "\<phi> \<one> x = x"
```
```   277     by (metis assms id_eq_one restrict_apply')
```
```   278   thus ?thesis
```
```   279     using group_def group_hom group_hom.axioms(1) stabilizer_def by fastforce
```
```   280 qed
```
```   281
```
```   282 lemma (in group_action) stabilizer_m_inv_closed:
```
```   283   assumes "x \<in> E" "g \<in> (stabilizer G \<phi> x)"
```
```   284   shows "(inv g) \<in> (stabilizer G \<phi> x)"
```
```   285 proof -
```
```   286   interpret group G
```
```   287     using group_hom group_hom.axioms(1) by auto
```
```   288
```
```   289   have "\<phi> g x = x"
```
```   290     using assms(2) stabilizer_def by fastforce
```
```   291   moreover have g: "g \<in> carrier G"
```
```   292     using assms(2) stabilizer_subset by blast
```
```   293   moreover have inv_g: "inv g \<in> carrier G"
```
```   294     by (simp add: g)
```
```   295   ultimately have "\<phi> (inv g) x = x"
```
```   296     using assms(1) orbit_sym_aux by blast
```
```   297
```
```   298   thus ?thesis by (simp add: inv_g stabilizer_def)
```
```   299 qed
```
```   300
```
```   301 theorem (in group_action) stabilizer_subgroup:
```
```   302   assumes "x \<in> E"
```
```   303   shows "subgroup (stabilizer G \<phi> x) G"
```
```   304   unfolding subgroup_def
```
```   305   using stabilizer_subset stabilizer_m_closed stabilizer_one_closed
```
```   306         stabilizer_m_inv_closed assms by simp
```
```   307
```
```   308
```
```   309
```
```   310 subsection \<open>The Orbit-Stabilizer Theorem\<close>
```
```   311
```
```   312 text \<open>In this subsection, we prove the Orbit-Stabilizer theorem.
```
```   313       Our approach is to show the existence of a bijection between
```
```   314       "rcosets (stabilizer G phi x)" and "orbit G phi x". Then we use
```
```   315       Lagrange's theorem to find the cardinal of the first set.\<close>
```
```   316
```
```   317 subsubsection \<open>Rcosets - Supporting Lemmas\<close>
```
```   318
```
```   319 corollary (in group_action) stab_rcosets_not_empty:
```
```   320   assumes "x \<in> E" "R \<in> rcosets (stabilizer G \<phi> x)"
```
```   321   shows "R \<noteq> {}"
```
```   322   using subgroup.rcosets_non_empty[OF stabilizer_subgroup[OF assms(1)] assms(2)] by simp
```
```   323
```
```   324 corollary (in group_action) diff_stabilizes:
```
```   325   assumes "x \<in> E" "R \<in> rcosets (stabilizer G \<phi> x)"
```
```   326   shows "\<And>g1 g2. \<lbrakk> g1 \<in> R; g2 \<in> R \<rbrakk> \<Longrightarrow> g1 \<otimes> (inv g2) \<in> stabilizer G \<phi> x"
```
```   327   using group.diff_neutralizes[of G "stabilizer G \<phi> x" R] stabilizer_subgroup[OF assms(1)]
```
```   328         assms(2) group_hom group_hom.axioms(1) by blast
```
```   329
```
```   330
```
```   331 subsubsection \<open>Bijection Between Rcosets and an Orbit - Definition and Supporting Lemmas\<close>
```
```   332
```
```   333 (* This definition could be easier if lcosets were available, and it's indeed a considerable
```
```   334    modification at Coset theory, since we could derive it easily from the definition of rcosets
```
```   335    following the same idea we use here: f: rcosets \<rightarrow> lcosets, s.t. f R = (\<lambda>g. inv g) ` R
```
```   336    is a bijection. *)
```
```   337
```
```   338 definition
```
```   339   orb_stab_fun :: "[_, ('a \<Rightarrow> 'b \<Rightarrow> 'b), 'a set, 'b] \<Rightarrow> 'b"
```
```   340   where "orb_stab_fun G \<phi> R x = (\<phi> (inv\<^bsub>G\<^esub> (SOME h. h \<in> R))) x"
```
```   341
```
```   342 lemma (in group_action) orbit_stab_fun_is_well_defined0:
```
```   343   assumes "x \<in> E" "R \<in> rcosets (stabilizer G \<phi> x)"
```
```   344   shows "\<And>g1 g2. \<lbrakk> g1 \<in> R; g2 \<in> R \<rbrakk> \<Longrightarrow> (\<phi> (inv g1)) x = (\<phi> (inv g2)) x"
```
```   345 proof -
```
```   346   fix g1 g2 assume g1: "g1 \<in> R" and g2: "g2 \<in> R"
```
```   347   have R_carr: "R \<subseteq> carrier G"
```
```   348     using subgroup.rcosets_carrier[OF stabilizer_subgroup[OF assms(1)]]
```
```   349           assms(2) group_hom group_hom.axioms(1) by auto
```
```   350   from R_carr have g1_carr: "g1 \<in> carrier G" using g1 by blast
```
```   351   from R_carr have g2_carr: "g2 \<in> carrier G" using g2 by blast
```
```   352
```
```   353   have "g1 \<otimes> (inv g2) \<in> stabilizer G \<phi> x"
```
```   354     using diff_stabilizes[of x R g1 g2] assms g1 g2 by blast
```
```   355   hence "\<phi> (g1 \<otimes> (inv g2)) x = x"
```
```   356     by (simp add: stabilizer_def)
```
```   357   hence "(\<phi> (inv g1)) x = (\<phi> (inv g1)) (\<phi> (g1 \<otimes> (inv g2)) x)" by simp
```
```   358   also have " ... = \<phi> ((inv g1) \<otimes> (g1 \<otimes> (inv g2))) x"
```
```   359     using group_def assms(1) composition_rule g1_carr g2_carr
```
```   360           group_hom group_hom.axioms(1) monoid.m_closed by fastforce
```
```   361   also have " ... = \<phi> (((inv g1) \<otimes> g1) \<otimes> (inv g2)) x"
```
```   362     using group_def g1_carr g2_carr group_hom group_hom.axioms(1) monoid.m_assoc by fastforce
```
```   363   finally show "(\<phi> (inv g1)) x = (\<phi> (inv g2)) x"
```
```   364     using group_def g1_carr g2_carr group.l_inv group_hom group_hom.axioms(1) by fastforce
```
```   365 qed
```
```   366
```
```   367 lemma (in group_action) orbit_stab_fun_is_well_defined1:
```
```   368   assumes "x \<in> E" "R \<in> rcosets (stabilizer G \<phi> x)"
```
```   369   shows "\<And>g. g \<in> R \<Longrightarrow> (\<phi> (inv (SOME h. h \<in> R))) x = (\<phi> (inv g)) x"
```
```   370   by (meson assms orbit_stab_fun_is_well_defined0 someI_ex)
```
```   371
```
```   372 lemma (in group_action) orbit_stab_fun_is_inj:
```
```   373   assumes "x \<in> E"
```
```   374     and "R1 \<in> rcosets (stabilizer G \<phi> x)"
```
```   375     and "R2 \<in> rcosets (stabilizer G \<phi> x)"
```
```   376     and "\<phi> (inv (SOME h. h \<in> R1)) x = \<phi> (inv (SOME h. h \<in> R2)) x"
```
```   377   shows "R1 = R2"
```
```   378 proof -
```
```   379   have "(\<exists>g1. g1 \<in> R1) \<and> (\<exists>g2. g2 \<in> R2)"
```
```   380     using assms(1-3) stab_rcosets_not_empty by auto
```
```   381   then obtain g1 g2 where g1: "g1 \<in> R1" and g2: "g2 \<in> R2" by blast
```
```   382   hence g12_carr: "g1 \<in> carrier G \<and> g2 \<in> carrier G"
```
```   383     using subgroup.rcosets_carrier assms(1-3) group_hom
```
```   384           group_hom.axioms(1) stabilizer_subgroup by blast
```
```   385
```
```   386   then obtain r1 r2 where r1: "r1 \<in> carrier G" "R1 = (stabilizer G \<phi> x) #> r1"
```
```   387                       and r2: "r2 \<in> carrier G" "R2 = (stabilizer G \<phi> x) #> r2"
```
```   388     using assms(1-3) unfolding RCOSETS_def by blast
```
```   389   then obtain s1 s2 where s1: "s1 \<in> (stabilizer G \<phi> x)" "g1 = s1 \<otimes> r1"
```
```   390                       and s2: "s2 \<in> (stabilizer G \<phi> x)" "g2 = s2 \<otimes> r2"
```
```   391     using g1 g2 unfolding r_coset_def by blast
```
```   392
```
```   393   have "\<phi> (inv g1) x = \<phi> (inv (SOME h. h \<in> R1)) x"
```
```   394     using orbit_stab_fun_is_well_defined1[OF assms(1) assms(2) g1] by simp
```
```   395   also have " ... = \<phi> (inv (SOME h. h \<in> R2)) x"
```
```   396     using assms(4) by simp
```
```   397   finally have "\<phi> (inv g1) x = \<phi> (inv g2) x"
```
```   398     using orbit_stab_fun_is_well_defined1[OF assms(1) assms(3) g2] by simp
```
```   399
```
```   400   hence "\<phi> g2 (\<phi> (inv g1) x) = \<phi> g2 (\<phi> (inv g2) x)" by simp
```
```   401   also have " ... = \<phi> (g2 \<otimes> (inv g2)) x"
```
```   402     using assms(1) composition_rule g12_carr group_hom group_hom.axioms(1) by fastforce
```
```   403   finally have "\<phi> g2 (\<phi> (inv g1) x) = x"
```
```   404     using g12_carr assms(1) group.r_inv group_hom group_hom.axioms(1)
```
```   405           id_eq_one restrict_apply by metis
```
```   406   hence "\<phi> (g2 \<otimes> (inv g1)) x = x"
```
```   407     using assms(1) composition_rule g12_carr group_hom group_hom.axioms(1) by fastforce
```
```   408   hence "g2 \<otimes> (inv g1) \<in> (stabilizer G \<phi> x)"
```
```   409     using g12_carr group.subgroup_self group_hom group_hom.axioms(1)
```
```   410           mem_Collect_eq stabilizer_def subgroup_def by (metis (mono_tags, lifting))
```
```   411   then obtain s where s: "s \<in> (stabilizer G \<phi> x)" "s = g2 \<otimes> (inv g1)" by blast
```
```   412
```
```   413   let ?h = "s \<otimes> g1"
```
```   414   have "?h = s \<otimes> (s1 \<otimes> r1)" by (simp add: s1)
```
```   415   hence "?h = (s \<otimes> s1) \<otimes> r1"
```
```   416     using stabilizer_subgroup[OF assms(1)] group_def group_hom
```
```   417           group_hom.axioms(1) monoid.m_assoc r1 s s1 subgroup.mem_carrier by fastforce
```
```   418   hence inR1: "?h \<in> (stabilizer G \<phi> x) #> r1" unfolding r_coset_def
```
```   419     using stabilizer_subgroup[OF assms(1)] assms(1) s s1 stabilizer_m_closed by auto
```
```   420
```
```   421   have "?h = g2" using s stabilizer_subgroup[OF assms(1)] g12_carr group.inv_solve_right
```
```   422                        group_hom group_hom.axioms(1) subgroup.mem_carrier by metis
```
```   423   hence inR2: "?h \<in> (stabilizer G \<phi> x) #> r2"
```
```   424     using g2 r2 by blast
```
```   425
```
```   426   have "R1 \<inter> R2 \<noteq> {}" using inR1 inR2 r1 r2 by blast
```
```   427   thus ?thesis using stabilizer_subgroup group.rcos_disjoint[of G "stabilizer G \<phi> x" R1 R2]
```
```   428                      assms group_hom group_hom.axioms(1) by blast
```
```   429 qed
```
```   430
```
```   431 lemma (in group_action) orbit_stab_fun_is_surj:
```
```   432   assumes "x \<in> E" "y \<in> orbit G \<phi> x"
```
```   433   shows "\<exists>R \<in> rcosets (stabilizer G \<phi> x). \<phi> (inv (SOME h. h \<in> R)) x = y"
```
```   434 proof -
```
```   435   have "\<exists>g \<in> carrier G. (\<phi> g) x = y"
```
```   436     using assms(2) unfolding orbit_def by blast
```
```   437   then obtain g where g: "g \<in> carrier G \<and> (\<phi> g) x = y" by blast
```
```   438
```
```   439   let ?R = "(stabilizer G \<phi> x) #> (inv g)"
```
```   440   have R: "?R \<in> rcosets (stabilizer G \<phi> x)"
```
```   441     unfolding RCOSETS_def using g group_hom group_hom.axioms(1) by fastforce
```
```   442   moreover have "\<one> \<otimes> (inv g) \<in> ?R"
```
```   443     unfolding r_coset_def using assms(1) stabilizer_one_closed by auto
```
```   444   ultimately have "\<phi> (inv (SOME h. h \<in> ?R)) x = \<phi> (inv (\<one> \<otimes> (inv g))) x"
```
```   445     using orbit_stab_fun_is_well_defined1[OF assms(1)] by simp
```
```   446   also have " ... = (\<phi> g) x"
```
```   447     using group_def g group_hom group_hom.axioms(1) monoid.l_one by fastforce
```
```   448   finally have "\<phi> (inv (SOME h. h \<in> ?R)) x = y"
```
```   449     using g by simp
```
```   450   thus ?thesis using R by blast
```
```   451 qed
```
```   452
```
```   453 proposition (in group_action) orbit_stab_fun_is_bij:
```
```   454   assumes "x \<in> E"
```
```   455   shows "bij_betw (\<lambda>R. (\<phi> (inv (SOME h. h \<in> R))) x) (rcosets (stabilizer G \<phi> x)) (orbit G \<phi> x)"
```
```   456   unfolding bij_betw_def
```
```   457 proof
```
```   458   show "inj_on (\<lambda>R. \<phi> (inv (SOME h. h \<in> R)) x) (rcosets stabilizer G \<phi> x)"
```
```   459     using orbit_stab_fun_is_inj[OF assms(1)] by (simp add: inj_on_def)
```
```   460 next
```
```   461   have "\<And>R. R \<in> (rcosets stabilizer G \<phi> x) \<Longrightarrow> \<phi> (inv (SOME h. h \<in> R)) x \<in> orbit G \<phi> x "
```
```   462   proof -
```
```   463     fix R assume R: "R \<in> (rcosets stabilizer G \<phi> x)"
```
```   464     then obtain g where g: "g \<in> R"
```
```   465       using assms stab_rcosets_not_empty by auto
```
```   466     hence "\<phi> (inv (SOME h. h \<in> R)) x = \<phi> (inv g) x"
```
```   467       using R  assms orbit_stab_fun_is_well_defined1 by blast
```
```   468     thus "\<phi> (inv (SOME h. h \<in> R)) x \<in> orbit G \<phi> x" unfolding orbit_def
```
```   469       using subgroup.rcosets_carrier group_hom group_hom.axioms(1)
```
```   470             g R assms stabilizer_subgroup by fastforce
```
```   471   qed
```
```   472   moreover have "orbit G \<phi> x \<subseteq> (\<lambda>R. \<phi> (inv (SOME h. h \<in> R)) x) ` (rcosets stabilizer G \<phi> x)"
```
```   473     using assms orbit_stab_fun_is_surj by fastforce
```
```   474   ultimately show "(\<lambda>R. \<phi> (inv (SOME h. h \<in> R)) x) ` (rcosets stabilizer G \<phi> x) = orbit G \<phi> x "
```
```   475     using assms set_eq_subset by blast
```
```   476 qed
```
```   477
```
```   478
```
```   479 subsubsection \<open>The Theorem\<close>
```
```   480
```
```   481 theorem (in group_action) orbit_stabilizer_theorem:
```
```   482   assumes "x \<in> E"
```
```   483   shows "card (orbit G \<phi> x) * card (stabilizer G \<phi> x) = order G"
```
```   484 proof -
```
```   485   have "card (rcosets stabilizer G \<phi> x) = card (orbit G \<phi> x)"
```
```   486     using orbit_stab_fun_is_bij[OF assms(1)] bij_betw_same_card by blast
```
```   487   moreover have "card (rcosets stabilizer G \<phi> x) * card (stabilizer G \<phi> x) = order G"
```
```   488     using stabilizer_subgroup assms group.lagrange group_hom group_hom.axioms(1) by blast
```
```   489   ultimately show ?thesis by auto
```
```   490 qed
```
```   491
```
```   492
```
```   493
```
```   494 subsection \<open>The Burnside's Lemma\<close>
```
```   495
```
```   496 subsubsection \<open>Sums and Cardinals\<close>
```
```   497
```
```   498 lemma card_as_sums:
```
```   499   assumes "A = {x \<in> B. P x}" "finite B"
```
```   500   shows "card A = (\<Sum>x\<in>B. (if P x then 1 else 0))"
```
```   501 proof -
```
```   502   have "A \<subseteq> B" using assms(1) by blast
```
```   503   have "card A = (\<Sum>x\<in>A. 1)" by simp
```
```   504   also have " ... = (\<Sum>x\<in>A. (if P x then 1 else 0))"
```
```   505     by (simp add: assms(1))
```
```   506   also have " ... = (\<Sum>x\<in>A. (if P x then 1 else 0)) + (\<Sum>x\<in>(B - A). (if P x then 1 else 0))"
```
```   507     using assms(1) by auto
```
```   508   finally show "card A = (\<Sum>x\<in>B. (if P x then 1 else 0))"
```
```   509     using \<open>A \<subseteq> B\<close> add.commute assms(2) sum.subset_diff by metis
```
```   510 qed
```
```   511
```
```   512 lemma sum_invertion:
```
```   513   "\<lbrakk> finite A; finite B \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>A. \<Sum>y\<in>B. f x y) = (\<Sum>y\<in>B. \<Sum>x\<in>A. f x y)"
```
```   514 proof (induct set: finite)
```
```   515   case empty thus ?case by simp
```
```   516 next
```
```   517   case (insert x A')
```
```   518   have "(\<Sum>x\<in>insert x A'. \<Sum>y\<in>B. f x y) = (\<Sum>y\<in>B. f x y) + (\<Sum>x\<in>A'. \<Sum>y\<in>B. f x y)"
```
```   519     by (simp add: insert.hyps)
```
```   520   also have " ... = (\<Sum>y\<in>B. f x y) + (\<Sum>y\<in>B. \<Sum>x\<in>A'. f x y)"
```
```   521     using insert.hyps by (simp add: insert.prems)
```
```   522   also have " ... = (\<Sum>y\<in>B. (f x y) + (\<Sum>x\<in>A'. f x y))"
```
```   523     by (simp add: sum.distrib)
```
```   524   finally have "(\<Sum>x\<in>insert x A'. \<Sum>y\<in>B. f x y) = (\<Sum>y\<in>B. \<Sum>x\<in>insert x A'. f x y)"
```
```   525     using sum.swap by blast
```
```   526   thus ?case by simp
```
```   527 qed
```
```   528
```
```   529 lemma (in group_action) card_stablizer_sum:
```
```   530   assumes "finite (carrier G)" "orb \<in> (orbits G E \<phi>)"
```
```   531   shows "(\<Sum>x \<in> orb. card (stabilizer G \<phi> x)) = order G"
```
```   532 proof -
```
```   533   obtain x where x:"x \<in> E" and orb:"orb = orbit G \<phi> x"
```
```   534     using assms(2) unfolding orbits_def by blast
```
```   535   have "\<And>y. y \<in> orb \<Longrightarrow> card (stabilizer G \<phi> x) = card (stabilizer G \<phi> y)"
```
```   536   proof -
```
```   537     fix y assume "y \<in> orb"
```
```   538     hence y: "y \<in> E \<and> y \<in> orbit G \<phi> x"
```
```   539       using x orb assms(2) orbits_coverture by auto
```
```   540     hence same_orbit: "(orbit G \<phi> x) = (orbit G \<phi> y)"
```
```   541       using disjoint_union[of "orbit G \<phi> x" "orbit G \<phi> y"] orbit_refl x
```
```   542       unfolding orbits_def by auto
```
```   543     have "card (orbit G \<phi> x) * card (stabilizer G \<phi> x) =
```
```   544           card (orbit G \<phi> y) * card (stabilizer G \<phi> y)"
```
```   545       using y assms(1) x orbit_stabilizer_theorem by simp
```
```   546     hence "card (orbit G \<phi> x) * card (stabilizer G \<phi> x) =
```
```   547            card (orbit G \<phi> x) * card (stabilizer G \<phi> y)" using same_orbit by simp
```
```   548     moreover have "orbit G \<phi> x \<noteq> {} \<and> finite (orbit G \<phi> x)"
```
```   549       using y orbit_def[of G \<phi> x] assms(1) by auto
```
```   550     hence "card (orbit G \<phi> x) > 0"
```
```   551       by (simp add: card_gt_0_iff)
```
```   552     ultimately show "card (stabilizer G \<phi> x) = card (stabilizer G \<phi> y)" by auto
```
```   553   qed
```
```   554   hence "(\<Sum>x \<in> orb. card (stabilizer G \<phi> x)) = (\<Sum>y \<in> orb. card (stabilizer G \<phi> x))" by auto
```
```   555   also have " ... = card (stabilizer G \<phi> x) * (\<Sum>y \<in> orb. 1)" by simp
```
```   556   also have " ... = card (stabilizer G \<phi> x) * card (orbit G \<phi> x)"
```
```   557     using orb by auto
```
```   558   finally show "(\<Sum>x \<in> orb. card (stabilizer G \<phi> x)) = order G"
```
```   559     by (metis mult.commute orbit_stabilizer_theorem x)
```
```   560 qed
```
```   561
```
```   562
```
```   563 subsubsection \<open>The Lemma\<close>
```
```   564
```
```   565 theorem (in group_action) burnside:
```
```   566   assumes "finite (carrier G)" "finite E"
```
```   567   shows "card (orbits G E \<phi>) * order G = (\<Sum>g \<in> carrier G. card(invariants E \<phi> g))"
```
```   568 proof -
```
```   569   have "(\<Sum>g \<in> carrier G. card(invariants E \<phi> g)) =
```
```   570         (\<Sum>g \<in> carrier G. \<Sum>x \<in> E. (if (\<phi> g) x = x then 1 else 0))"
```
```   571     by (simp add: assms(2) card_as_sums invariants_def)
```
```   572   also have " ... = (\<Sum>x \<in> E. \<Sum>g \<in> carrier G. (if (\<phi> g) x = x then 1 else 0))"
```
```   573     using sum_invertion[where ?f = "\<lambda> g x. (if (\<phi> g) x = x then 1 else 0)"] assms by auto
```
```   574   also have " ... = (\<Sum>x \<in> E. card (stabilizer G \<phi> x))"
```
```   575     by (simp add: assms(1) card_as_sums stabilizer_def)
```
```   576   also have " ... = (\<Sum>orbit \<in> (orbits G E \<phi>). \<Sum>x \<in> orbit. card (stabilizer G \<phi> x))"
```
```   577     using disjoint_sum orbits_coverture assms(2) by metis
```
```   578   also have " ... = (\<Sum>orbit \<in> (orbits G E \<phi>). order G)"
```
```   579     by (simp add: assms(1) card_stablizer_sum)
```
```   580   finally have "(\<Sum>g \<in> carrier G. card(invariants E \<phi> g)) = card (orbits G E \<phi>) * order G" by simp
```
```   581   thus ?thesis by simp
```
```   582 qed
```
```   583
```
```   584
```
```   585
```
```   586 subsection \<open>Action by Conjugation\<close>
```
```   587
```
```   588
```
```   589 subsubsection \<open>Action Over Itself\<close>
```
```   590
```
```   591 text \<open>A Group Acts by Conjugation Over Itself\<close>
```
```   592
```
```   593 lemma (in group) conjugation_is_inj:
```
```   594   assumes "g \<in> carrier G" "h1 \<in> carrier G" "h2 \<in> carrier G"
```
```   595     and "g \<otimes> h1 \<otimes> (inv g) = g \<otimes> h2 \<otimes> (inv g)"
```
```   596     shows "h1 = h2"
```
```   597   using assms by auto
```
```   598
```
```   599 lemma (in group) conjugation_is_surj:
```
```   600   assumes "g \<in> carrier G" "h \<in> carrier G"
```
```   601   shows "g \<otimes> ((inv g) \<otimes> h \<otimes> g) \<otimes> (inv g) = h"
```
```   602   using assms m_assoc inv_closed inv_inv m_closed monoid_axioms r_inv r_one
```
```   603   by metis
```
```   604
```
```   605 lemma (in group) conjugation_is_bij:
```
```   606   assumes "g \<in> carrier G"
```
```   607   shows "bij_betw (\<lambda>h \<in> carrier G. g \<otimes> h \<otimes> (inv g)) (carrier G) (carrier G)"
```
```   608          (is "bij_betw ?\<phi> (carrier G) (carrier G)")
```
```   609   unfolding bij_betw_def
```
```   610 proof
```
```   611   show "inj_on ?\<phi> (carrier G)"
```
```   612     using conjugation_is_inj by (simp add: assms inj_on_def)
```
```   613 next
```
```   614   have S: "\<And> h. h \<in> carrier G \<Longrightarrow> (inv g) \<otimes> h \<otimes> g \<in> carrier G"
```
```   615     using assms by blast
```
```   616   have "\<And> h. h \<in> carrier G \<Longrightarrow> ?\<phi> ((inv g) \<otimes> h \<otimes> g) = h"
```
```   617     using assms by (simp add: conjugation_is_surj)
```
```   618   hence "carrier G \<subseteq> ?\<phi> ` carrier G"
```
```   619     using S image_iff by fastforce
```
```   620   moreover have "\<And> h. h \<in> carrier G \<Longrightarrow> ?\<phi> h \<in> carrier G"
```
```   621     using assms by simp
```
```   622   hence "?\<phi> ` carrier G \<subseteq> carrier G" by blast
```
```   623   ultimately show "?\<phi> ` carrier G = carrier G" by blast
```
```   624 qed
```
```   625
```
```   626 lemma(in group) conjugation_is_hom:
```
```   627   "(\<lambda>g. \<lambda>h \<in> carrier G. g \<otimes> h \<otimes> inv g) \<in> hom G (BijGroup (carrier G))"
```
```   628   unfolding hom_def
```
```   629 proof -
```
```   630   let ?\<psi> = "\<lambda>g. \<lambda>h. g \<otimes> h \<otimes> inv g"
```
```   631   let ?\<phi> = "\<lambda>g. restrict (?\<psi> g) (carrier G)"
```
```   632
```
```   633   (* First, we prove that ?\<phi>: G \<rightarrow> Bij(G) is well defined *)
```
```   634   have Step0: "\<And> g. g \<in> carrier G \<Longrightarrow> (?\<phi> g) \<in> Bij (carrier G)"
```
```   635     using Bij_def conjugation_is_bij by fastforce
```
```   636   hence Step1: "?\<phi>: carrier G \<rightarrow> carrier (BijGroup (carrier G))"
```
```   637     unfolding BijGroup_def by simp
```
```   638
```
```   639   (* Second, we prove that ?\<phi> is a homomorphism *)
```
```   640   have "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   641                   (\<And> h. h \<in> carrier G \<Longrightarrow> ?\<psi> (g1 \<otimes> g2) h = (?\<phi> g1) ((?\<phi> g2) h))"
```
```   642   proof -
```
```   643     fix g1 g2 h assume g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G" and h: "h \<in> carrier G"
```
```   644     have "inv (g1 \<otimes> g2) = (inv g2) \<otimes> (inv g1)"
```
```   645       using g1 g2 by (simp add: inv_mult_group)
```
```   646     thus "?\<psi> (g1 \<otimes> g2) h  = (?\<phi> g1) ((?\<phi> g2) h)"
```
```   647       by (simp add: g1 g2 h m_assoc)
```
```   648   qed
```
```   649   hence "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   650          (\<lambda> h \<in> carrier G. ?\<psi> (g1 \<otimes> g2) h) = (\<lambda> h \<in> carrier G. (?\<phi> g1) ((?\<phi> g2) h))" by auto
```
```   651   hence Step2: "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   652                 ?\<phi> (g1 \<otimes> g2) = (?\<phi> g1) \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> (?\<phi> g2)"
```
```   653     unfolding BijGroup_def by (simp add: Step0 compose_def)
```
```   654
```
```   655   (* Finally, we combine both results to prove the lemma *)
```
```   656   thus "?\<phi> \<in> {h: carrier G \<rightarrow> carrier (BijGroup (carrier G)).
```
```   657               (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^bsub>BijGroup (carrier G)\<^esub> h y)}"
```
```   658     using Step1 Step2 by auto
```
```   659 qed
```
```   660
```
```   661 theorem (in group) action_by_conjugation:
```
```   662   "group_action G (carrier G) (\<lambda>g. (\<lambda>h \<in> carrier G. g \<otimes> h \<otimes> (inv g)))"
```
```   663   unfolding group_action_def group_hom_def using conjugation_is_hom
```
```   664   by (simp add: group_BijGroup group_hom_axioms.intro is_group)
```
```   665
```
```   666
```
```   667 subsubsection \<open>Action Over The Set of Subgroups\<close>
```
```   668
```
```   669 text \<open>A Group Acts by Conjugation Over The Set of Subgroups\<close>
```
```   670
```
```   671 lemma (in group) subgroup_conjugation_is_inj_aux:
```
```   672   assumes "g \<in> carrier G" "H1 \<subseteq> carrier G" "H2 \<subseteq> carrier G"
```
```   673     and "g <# H1 #> (inv g) = g <# H2 #> (inv g)"
```
```   674     shows "H1 \<subseteq> H2"
```
```   675 proof
```
```   676   fix h1 assume h1: "h1 \<in> H1"
```
```   677   hence "g \<otimes> h1 \<otimes> (inv g) \<in> g <# H1 #> (inv g)"
```
```   678     unfolding l_coset_def r_coset_def using assms by blast
```
```   679   hence "g \<otimes> h1 \<otimes> (inv g) \<in> g <# H2 #> (inv g)"
```
```   680     using assms by auto
```
```   681   hence "\<exists>h2 \<in> H2. g \<otimes> h1 \<otimes> (inv g) = g \<otimes> h2 \<otimes> (inv g)"
```
```   682       unfolding l_coset_def r_coset_def by blast
```
```   683   then obtain h2 where "h2 \<in> H2 \<and> g \<otimes> h1 \<otimes> (inv g) = g \<otimes> h2 \<otimes> (inv g)" by blast
```
```   684   thus "h1 \<in> H2"
```
```   685     using assms conjugation_is_inj h1 by blast
```
```   686 qed
```
```   687
```
```   688 lemma (in group) subgroup_conjugation_is_inj:
```
```   689   assumes "g \<in> carrier G" "H1 \<subseteq> carrier G" "H2 \<subseteq> carrier G"
```
```   690     and "g <# H1 #> (inv g) = g <# H2 #> (inv g)"
```
```   691     shows "H1 = H2"
```
```   692   using subgroup_conjugation_is_inj_aux assms set_eq_subset by metis
```
```   693
```
```   694 lemma (in group) subgroup_conjugation_is_surj0:
```
```   695   assumes "g \<in> carrier G" "H \<subseteq> carrier G"
```
```   696   shows "g <# ((inv g) <# H #> g) #> (inv g) = H"
```
```   697   using coset_assoc assms coset_mult_assoc l_coset_subset_G lcos_m_assoc
```
```   698   by (simp add: lcos_mult_one)
```
```   699
```
```   700 lemma (in group) subgroup_conjugation_is_surj1:
```
```   701   assumes "g \<in> carrier G" "subgroup H G"
```
```   702   shows "subgroup ((inv g) <# H #> g) G"
```
```   703 proof
```
```   704   show "\<one> \<in> inv g <# H #> g"
```
```   705   proof -
```
```   706     have "\<one> \<in> H" by (simp add: assms(2) subgroup.one_closed)
```
```   707     hence "inv g \<otimes> \<one> \<otimes> g \<in> inv g <# H #> g"
```
```   708       unfolding l_coset_def r_coset_def by blast
```
```   709     thus "\<one> \<in> inv g <# H #> g" using assms by simp
```
```   710   qed
```
```   711 next
```
```   712   show "inv g <# H #> g \<subseteq> carrier G"
```
```   713   proof
```
```   714     fix x assume "x \<in> inv g <# H #> g"
```
```   715     hence "\<exists>h \<in> H. x = (inv g) \<otimes> h \<otimes> g"
```
```   716       unfolding r_coset_def l_coset_def by blast
```
```   717     hence "\<exists>h \<in> (carrier G). x = (inv g) \<otimes> h \<otimes> g"
```
```   718       by (meson assms subgroup.mem_carrier)
```
```   719     thus "x \<in> carrier G" using assms by blast
```
```   720   qed
```
```   721 next
```
```   722   show " \<And> x y. \<lbrakk> x \<in> inv g <# H #> g; y \<in> inv g <# H #> g \<rbrakk> \<Longrightarrow> x \<otimes> y \<in> inv g <# H #> g"
```
```   723   proof -
```
```   724     fix x y assume "x \<in> inv g <# H #> g"  "y \<in> inv g <# H #> g"
```
```   725     hence "\<exists> h1 \<in> H. \<exists> h2 \<in> H. x = (inv g) \<otimes> h1 \<otimes> g \<and> y = (inv g) \<otimes> h2 \<otimes> g"
```
```   726       unfolding l_coset_def r_coset_def by blast
```
```   727     hence "\<exists> h1 \<in> H. \<exists> h2 \<in> H. x \<otimes> y = ((inv g) \<otimes> h1 \<otimes> g) \<otimes> ((inv g) \<otimes> h2 \<otimes> g)" by blast
```
```   728     hence "\<exists> h1 \<in> H. \<exists> h2 \<in> H. x \<otimes> y = ((inv g) \<otimes> (h1 \<otimes> h2) \<otimes> g)"
```
```   729       using assms is_group inv_closed l_one m_assoc m_closed
```
```   730             monoid_axioms r_inv subgroup.mem_carrier by smt
```
```   731     hence "\<exists> h \<in> H. x \<otimes> y = (inv g) \<otimes> h \<otimes> g"
```
```   732       by (meson assms(2) subgroup_def)
```
```   733     thus "x \<otimes> y \<in> inv g <# H #> g"
```
```   734       unfolding l_coset_def r_coset_def by blast
```
```   735   qed
```
```   736 next
```
```   737   show "\<And>x. x \<in> inv g <# H #> g \<Longrightarrow> inv x \<in> inv g <# H #> g"
```
```   738   proof -
```
```   739     fix x assume "x \<in> inv g <# H #> g"
```
```   740     hence "\<exists>h \<in> H. x = (inv g) \<otimes> h \<otimes> g"
```
```   741       unfolding r_coset_def l_coset_def by blast
```
```   742     then obtain h where h: "h \<in> H \<and> x = (inv g) \<otimes> h \<otimes> g" by blast
```
```   743     hence "x \<otimes> (inv g) \<otimes> (inv h) \<otimes> g = \<one>"
```
```   744       using assms inv_closed m_assoc m_closed monoid_axioms
```
```   745             r_inv r_one subgroup.mem_carrier by smt
```
```   746     hence "inv x = (inv g) \<otimes> (inv h) \<otimes> g"
```
```   747       using assms h inv_closed inv_inv inv_mult_group m_assoc
```
```   748             m_closed monoid_axioms subgroup.mem_carrier by smt
```
```   749     moreover have "inv h \<in> H"
```
```   750       by (simp add: assms h subgroup.m_inv_closed)
```
```   751     ultimately show "inv x \<in> inv g <# H #> g" unfolding r_coset_def l_coset_def by blast
```
```   752   qed
```
```   753 qed
```
```   754
```
```   755 lemma (in group) subgroup_conjugation_is_surj2:
```
```   756   assumes "g \<in> carrier G" "subgroup H G"
```
```   757   shows "subgroup (g <# H #> (inv g)) G"
```
```   758   using subgroup_conjugation_is_surj1 by (metis assms inv_closed inv_inv)
```
```   759
```
```   760 lemma (in group) subgroup_conjugation_is_bij:
```
```   761   assumes "g \<in> carrier G"
```
```   762   shows "bij_betw (\<lambda>H \<in> {H. subgroup H G}. g <# H #> (inv g)) {H. subgroup H G} {H. subgroup H G}"
```
```   763          (is "bij_betw ?\<phi> {H. subgroup H G} {H. subgroup H G}")
```
```   764   unfolding bij_betw_def
```
```   765 proof
```
```   766   show "inj_on ?\<phi> {H. subgroup H G}"
```
```   767     using subgroup_conjugation_is_inj assms inj_on_def subgroup.subset
```
```   768     by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq)
```
```   769 next
```
```   770   have "\<And>H. H \<in> {H. subgroup H G} \<Longrightarrow> ?\<phi> ((inv g) <# H #> g) = H"
```
```   771     by (simp add: assms subgroup.subset subgroup_conjugation_is_surj0
```
```   772                   subgroup_conjugation_is_surj1 is_group)
```
```   773   hence "\<And>H. H \<in> {H. subgroup H G} \<Longrightarrow> \<exists>H' \<in> {H. subgroup H G}. ?\<phi> H' = H"
```
```   774     using assms subgroup_conjugation_is_surj1 by fastforce
```
```   775   thus "?\<phi> ` {H. subgroup H G} = {H. subgroup H G}"
```
```   776     using subgroup_conjugation_is_surj2 assms by auto
```
```   777 qed
```
```   778
```
```   779 lemma (in group) subgroup_conjugation_is_hom:
```
```   780   "(\<lambda>g. \<lambda>H \<in> {H. subgroup H G}. g <# H #> (inv g)) \<in> hom G (BijGroup {H. subgroup H G})"
```
```   781   unfolding hom_def
```
```   782 proof -
```
```   783   (* We follow the exact same structure of conjugation_is_hom's proof *)
```
```   784   let ?\<psi> = "\<lambda>g. \<lambda>H. g <# H #> (inv g)"
```
```   785   let ?\<phi> = "\<lambda>g. restrict (?\<psi> g) {H. subgroup H G}"
```
```   786
```
```   787   have Step0: "\<And> g. g \<in> carrier G \<Longrightarrow> (?\<phi> g) \<in> Bij {H. subgroup H G}"
```
```   788     using Bij_def subgroup_conjugation_is_bij by fastforce
```
```   789   hence Step1: "?\<phi>: carrier G \<rightarrow> carrier (BijGroup {H. subgroup H G})"
```
```   790     unfolding BijGroup_def by simp
```
```   791
```
```   792   have "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   793                   (\<And> H. H \<in> {H. subgroup H G} \<Longrightarrow> ?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> g2) H))"
```
```   794   proof -
```
```   795     fix g1 g2 H assume g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G" and H': "H \<in> {H. subgroup H G}"
```
```   796     hence H: "subgroup H G" by simp
```
```   797     have "(?\<phi> g1) ((?\<phi> g2) H) = g1 <# (g2 <# H #> (inv g2)) #> (inv g1)"
```
```   798       by (simp add: H g2 subgroup_conjugation_is_surj2)
```
```   799     also have " ... = g1 <# (g2 <# H) #> ((inv g2) \<otimes> (inv g1))"
```
```   800       by (simp add: H coset_mult_assoc g1 g2 group.coset_assoc
```
```   801                     is_group l_coset_subset_G subgroup.subset)
```
```   802     also have " ... = g1 <# (g2 <# H) #> inv (g1 \<otimes> g2)"
```
```   803       using g1 g2 by (simp add: inv_mult_group)
```
```   804     finally have "(?\<phi> g1) ((?\<phi> g2) H) = ?\<psi> (g1 \<otimes> g2) H"
```
```   805       by (simp add: H g1 g2 lcos_m_assoc subgroup.subset)
```
```   806     thus "?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> g2) H)" by auto
```
```   807   qed
```
```   808   hence "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   809          (\<lambda>H \<in> {H. subgroup H G}. ?\<psi> (g1 \<otimes> g2) H) = (\<lambda>H \<in> {H. subgroup H G}. (?\<phi> g1) ((?\<phi> g2) H))"
```
```   810     by (meson restrict_ext)
```
```   811   hence Step2: "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   812                 ?\<phi> (g1 \<otimes> g2) = (?\<phi> g1) \<otimes>\<^bsub>BijGroup {H. subgroup H G}\<^esub> (?\<phi> g2)"
```
```   813     unfolding BijGroup_def by (simp add: Step0 compose_def)
```
```   814
```
```   815   show "?\<phi> \<in> {h: carrier G \<rightarrow> carrier (BijGroup {H. subgroup H G}).
```
```   816               \<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}"
```
```   817     using Step1 Step2 by auto
```
```   818 qed
```
```   819
```
```   820 theorem (in group) action_by_conjugation_on_subgroups_set:
```
```   821   "group_action G {H. subgroup H G} (\<lambda>g. \<lambda>H \<in> {H. subgroup H G}. g <# H #> (inv g))"
```
```   822   unfolding group_action_def group_hom_def using subgroup_conjugation_is_hom
```
```   823   by (simp add: group_BijGroup group_hom_axioms.intro is_group)
```
```   824
```
```   825
```
```   826 subsubsection \<open>Action Over The Power Set\<close>
```
```   827
```
```   828 text \<open>A Group Acts by Conjugation Over The Power Set\<close>
```
```   829
```
```   830 lemma (in group) subset_conjugation_is_bij:
```
```   831   assumes "g \<in> carrier G"
```
```   832   shows "bij_betw (\<lambda>H \<in> {H. H \<subseteq> carrier G}. g <# H #> (inv g)) {H. H \<subseteq> carrier G} {H. H \<subseteq> carrier G}"
```
```   833          (is "bij_betw ?\<phi> {H. H \<subseteq> carrier G} {H. H \<subseteq> carrier G}")
```
```   834   unfolding bij_betw_def
```
```   835 proof
```
```   836   show "inj_on ?\<phi> {H. H \<subseteq> carrier G}"
```
```   837     using subgroup_conjugation_is_inj assms inj_on_def
```
```   838     by (metis (mono_tags, lifting) inj_on_restrict_eq mem_Collect_eq)
```
```   839 next
```
```   840   have "\<And>H. H \<in> {H. H \<subseteq> carrier G} \<Longrightarrow> ?\<phi> ((inv g) <# H #> g) = H"
```
```   841     by (simp add: assms l_coset_subset_G r_coset_subset_G subgroup_conjugation_is_surj0)
```
```   842   hence "\<And>H. H \<in> {H. H \<subseteq> carrier G} \<Longrightarrow> \<exists>H' \<in> {H. H \<subseteq> carrier G}. ?\<phi> H' = H"
```
```   843     by (metis assms l_coset_subset_G mem_Collect_eq r_coset_subset_G subgroup_def subgroup_self)
```
```   844   hence "{H. H \<subseteq> carrier G} \<subseteq> ?\<phi> ` {H. H \<subseteq> carrier G}" by blast
```
```   845   moreover have "?\<phi> ` {H. H \<subseteq> carrier G} \<subseteq> {H. H \<subseteq> carrier G}"
```
```   846     by (smt assms image_subsetI inv_closed l_coset_subset_G
```
```   847             mem_Collect_eq r_coset_subset_G restrict_apply')
```
```   848   ultimately show "?\<phi> ` {H. H \<subseteq> carrier G} = {H. H \<subseteq> carrier G}" by simp
```
```   849 qed
```
```   850
```
```   851 lemma (in group) subset_conjugation_is_hom:
```
```   852   "(\<lambda>g. \<lambda>H \<in> {H. H \<subseteq> carrier G}. g <# H #> (inv g)) \<in> hom G (BijGroup {H. H \<subseteq> carrier G})"
```
```   853   unfolding hom_def
```
```   854 proof -
```
```   855   (* We follow the exact same structure of conjugation_is_hom's proof *)
```
```   856   let ?\<psi> = "\<lambda>g. \<lambda>H. g <# H #> (inv g)"
```
```   857   let ?\<phi> = "\<lambda>g. restrict (?\<psi> g) {H. H \<subseteq> carrier G}"
```
```   858
```
```   859   have Step0: "\<And> g. g \<in> carrier G \<Longrightarrow> (?\<phi> g) \<in> Bij {H. H \<subseteq> carrier G}"
```
```   860     using Bij_def subset_conjugation_is_bij by fastforce
```
```   861   hence Step1: "?\<phi>: carrier G \<rightarrow> carrier (BijGroup {H. H \<subseteq> carrier G})"
```
```   862     unfolding BijGroup_def by simp
```
```   863
```
```   864   have "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   865                   (\<And> H. H \<in> {H. H \<subseteq> carrier G} \<Longrightarrow> ?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> g2) H))"
```
```   866   proof -
```
```   867     fix g1 g2 H assume g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G" and H: "H \<in> {H. H \<subseteq> carrier G}"
```
```   868     hence "(?\<phi> g1) ((?\<phi> g2) H) = g1 <# (g2 <# H #> (inv g2)) #> (inv g1)"
```
```   869       using l_coset_subset_G r_coset_subset_G by auto
```
```   870     also have " ... = g1 <# (g2 <# H) #> ((inv g2) \<otimes> (inv g1))"
```
```   871       using H coset_assoc coset_mult_assoc g1 g2 l_coset_subset_G by auto
```
```   872     also have " ... = g1 <# (g2 <# H) #> inv (g1 \<otimes> g2)"
```
```   873       using g1 g2 by (simp add: inv_mult_group)
```
```   874     finally have "(?\<phi> g1) ((?\<phi> g2) H) = ?\<psi> (g1 \<otimes> g2) H"
```
```   875       using H g1 g2 lcos_m_assoc by force
```
```   876     thus "?\<psi> (g1 \<otimes> g2) H = (?\<phi> g1) ((?\<phi> g2) H)" by auto
```
```   877   qed
```
```   878   hence "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   879          (\<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))"
```
```   880     by (meson restrict_ext)
```
```   881   hence Step2: "\<And> g1 g2. \<lbrakk> g1 \<in> carrier G; g2 \<in> carrier G \<rbrakk> \<Longrightarrow>
```
```   882                 ?\<phi> (g1 \<otimes> g2) = (?\<phi> g1) \<otimes>\<^bsub>BijGroup {H. H \<subseteq> carrier G}\<^esub> (?\<phi> g2)"
```
```   883     unfolding BijGroup_def by (simp add: Step0 compose_def)
```
```   884
```
```   885   show "?\<phi> \<in> {h: carrier G \<rightarrow> carrier (BijGroup {H. H \<subseteq> carrier G}).
```
```   886               \<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}"
```
```   887     using Step1 Step2 by auto
```
```   888 qed
```
```   889
```
```   890 theorem (in group) action_by_conjugation_on_power_set:
```
```   891   "group_action G {H. H \<subseteq> carrier G} (\<lambda>g. \<lambda>H \<in> {H. H \<subseteq> carrier G}. g <# H #> (inv g))"
```
```   892   unfolding group_action_def group_hom_def using subset_conjugation_is_hom
```
```   893   by (simp add: group_BijGroup group_hom_axioms.intro is_group)
```
```   894
```
```   895 corollary (in group) normalizer_imp_subgroup:
```
```   896   assumes "H \<subseteq> carrier G"
```
```   897   shows "subgroup (normalizer G H) G"
```
```   898   unfolding normalizer_def
```
```   899   using group_action.stabilizer_subgroup[OF action_by_conjugation_on_power_set] assms by auto
```
```   900
```
```   901
```
```   902 subsection \<open>Subgroup of an Acting Group\<close>
```
```   903
```
```   904 text \<open>A Subgroup of an Acting Group Induces an Action\<close>
```
```   905
```
```   906 lemma (in group_action) induced_homomorphism:
```
```   907   assumes "subgroup H G"
```
```   908   shows "\<phi> \<in> hom (G \<lparr>carrier := H\<rparr>) (BijGroup E)"
```
```   909   unfolding hom_def apply simp
```
```   910 proof -
```
```   911   have S0: "H \<subseteq> carrier G" by (meson assms subgroup_def)
```
```   912   hence "\<phi>: H \<rightarrow> carrier (BijGroup E)"
```
```   913     by (simp add: BijGroup_def bij_prop0 subset_eq)
```
```   914   thus "\<phi>: H \<rightarrow> carrier (BijGroup E) \<and> (\<forall>x \<in> H. \<forall>y \<in> H. \<phi> (x \<otimes> y) = \<phi> x \<otimes>\<^bsub>BijGroup E\<^esub> \<phi> y)"
```
```   915     by (simp add: S0  group_hom group_hom.hom_mult set_rev_mp)
```
```   916 qed
```
```   917
```
```   918 theorem (in group_action) induced_action:
```
```   919   assumes "subgroup H G"
```
```   920   shows "group_action (G \<lparr>carrier := H\<rparr>) E \<phi>"
```
```   921   unfolding group_action_def group_hom_def
```
```   922   using induced_homomorphism assms group.subgroup_imp_group group_BijGroup
```
```   923         group_hom group_hom.axioms(1) group_hom_axioms_def by blast
```
```   924
```
```   925 end
```