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