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