author | paulson <lp15@cam.ac.uk> |
Tue, 02 Apr 2019 12:56:05 +0100 | |
changeset 70027 | 94494b92d8d0 |
parent 70019 | 095dce9892e8 |
child 70039 | 733e256ecdf3 |
permissions | -rw-r--r-- |
68582 | 1 |
(* Title: HOL/Algebra/Generated_Groups.thy |
2 |
Author: Paulo Emílio de Vilhena |
|
3 |
*) |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
4 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
5 |
theory Generated_Groups |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
imports Group Coset |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
7 |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
begin |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
10 |
section \<open>Generated Groups\<close> |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
11 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
12 |
inductive_set generate :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
13 |
for G and H where |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
one: "\<one>\<^bsub>G\<^esub> \<in> generate G H" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
15 |
| incl: "h \<in> H \<Longrightarrow> h \<in> generate G H" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
| inv: "h \<in> H \<Longrightarrow> inv\<^bsub>G\<^esub> h \<in> generate G H" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
| eng: "h1 \<in> generate G H \<Longrightarrow> h2 \<in> generate G H \<Longrightarrow> h1 \<otimes>\<^bsub>G\<^esub> h2 \<in> generate G H" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
20 |
subsection \<open>Basic Properties\<close> |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
22 |
lemma (in group) generate_consistent: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
23 |
assumes "K \<subseteq> H" "subgroup H G" shows "generate (G \<lparr> carrier := H \<rparr>) K = generate G K" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
24 |
proof |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
25 |
show "generate (G \<lparr> carrier := H \<rparr>) K \<subseteq> generate G K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
26 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
27 |
fix h assume "h \<in> generate (G \<lparr> carrier := H \<rparr>) K" thus "h \<in> generate G K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
28 |
proof (induction, simp add: one, simp_all add: incl[of _ K G] eng) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
29 |
case inv thus ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
30 |
using m_inv_consistent assms generate.inv[of _ K G] by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
31 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
32 |
qed |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
next |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
34 |
show "generate G K \<subseteq> generate (G \<lparr> carrier := H \<rparr>) K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
35 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
36 |
note gen_simps = one incl eng |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
37 |
fix h assume "h \<in> generate G K" thus "h \<in> generate (G \<lparr> carrier := H \<rparr>) K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
38 |
using gen_simps[where ?G = "G \<lparr> carrier := H \<rparr>"] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
39 |
proof (induction, auto) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
40 |
fix h assume "h \<in> K" thus "inv h \<in> generate (G \<lparr> carrier := H \<rparr>) K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
41 |
using m_inv_consistent assms generate.inv[of h K "G \<lparr> carrier := H \<rparr>"] by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
46 |
lemma (in group) generate_in_carrier: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
47 |
assumes "H \<subseteq> carrier G" and "h \<in> generate G H" shows "h \<in> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
48 |
using assms(2,1) by (induct h rule: generate.induct) (auto) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
49 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
50 |
lemma (in group) generate_incl: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
51 |
assumes "H \<subseteq> carrier G" shows "generate G H \<subseteq> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
52 |
using generate_in_carrier[OF assms(1)] by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
53 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
54 |
lemma (in group) generate_m_inv_closed: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
55 |
assumes "H \<subseteq> carrier G" and "h \<in> generate G H" shows "(inv h) \<in> generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
56 |
using assms(2,1) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
57 |
proof (induction rule: generate.induct, auto simp add: one inv incl) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
58 |
fix h1 h2 |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
59 |
assume h1: "h1 \<in> generate G H" "inv h1 \<in> generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
60 |
and h2: "h2 \<in> generate G H" "inv h2 \<in> generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
61 |
hence "inv (h1 \<otimes> h2) = (inv h2) \<otimes> (inv h1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
62 |
by (meson assms generate_in_carrier group.inv_mult_group is_group) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
63 |
thus "inv (h1 \<otimes> h2) \<in> generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
64 |
using generate.eng[OF h2(2) h1(2)] by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
65 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
66 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
67 |
lemma (in group) generate_is_subgroup: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
68 |
assumes "H \<subseteq> carrier G" shows "subgroup (generate G H) G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
69 |
using subgroup.intro[OF generate_incl eng one generate_m_inv_closed] assms by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
70 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
71 |
lemma (in group) mono_generate: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
72 |
assumes "K \<subseteq> H" shows "generate G K \<subseteq> generate G H" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
proof |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
74 |
fix h assume "h \<in> generate G K" thus "h \<in> generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
75 |
using assms by (induction) (auto simp add: one incl inv eng) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
76 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
77 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
78 |
lemma (in group) generate_subgroup_incl: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
79 |
assumes "K \<subseteq> H" "subgroup H G" shows "generate G K \<subseteq> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
80 |
using group.generate_incl[OF subgroup_imp_group[OF assms(2)], of K] assms(1) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
81 |
by (simp add: generate_consistent[OF assms]) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
82 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
83 |
lemma (in group) generate_minimal: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
84 |
assumes "H \<subseteq> carrier G" shows "generate G H = \<Inter> { H'. subgroup H' G \<and> H \<subseteq> H' }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
85 |
using generate_subgroup_incl generate_is_subgroup[OF assms] incl[of _ H] by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
86 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
87 |
lemma (in group) generateI: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
88 |
assumes "subgroup E G" "H \<subseteq> E" and "\<And>K. \<lbrakk> subgroup K G; H \<subseteq> K \<rbrakk> \<Longrightarrow> E \<subseteq> K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
89 |
shows "E = generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
90 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
91 |
have subset: "H \<subseteq> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
92 |
using subgroup.subset assms by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
93 |
show ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
94 |
using assms unfolding generate_minimal[OF subset] by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
95 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
96 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
97 |
lemma (in group) normal_generateI: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
98 |
assumes "H \<subseteq> carrier G" and "\<And>h g. \<lbrakk> h \<in> H; g \<in> carrier G \<rbrakk> \<Longrightarrow> g \<otimes> h \<otimes> (inv g) \<in> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
99 |
shows "generate G H \<lhd> G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
100 |
proof (rule normal_invI[OF generate_is_subgroup[OF assms(1)]]) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
101 |
fix g h assume g: "g \<in> carrier G" show "h \<in> generate G H \<Longrightarrow> g \<otimes> h \<otimes> (inv g) \<in> generate G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
102 |
proof (induct h rule: generate.induct) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
103 |
case one thus ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
104 |
using g generate.one by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
105 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
106 |
case incl show ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
107 |
using generate.incl[OF assms(2)[OF incl g]] . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
108 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
109 |
case (inv h) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
110 |
hence h: "h \<in> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
111 |
using assms(1) by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
112 |
hence "inv (g \<otimes> h \<otimes> (inv g)) = g \<otimes> (inv h) \<otimes> (inv g)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
113 |
using g by (simp add: inv_mult_group m_assoc) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
114 |
thus ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
115 |
using generate_m_inv_closed[OF assms(1) generate.incl[OF assms(2)[OF inv g]]] by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
116 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
117 |
case (eng h1 h2) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
118 |
note in_carrier = eng(1,3)[THEN generate_in_carrier[OF assms(1)]] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
119 |
have "g \<otimes> (h1 \<otimes> h2) \<otimes> inv g = (g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
120 |
using in_carrier g by (simp add: inv_solve_left m_assoc) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
121 |
thus ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
122 |
using generate.eng[OF eng(2,4)] by simp |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
126 |
lemma (in group) subgroup_int_pow_closed: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
127 |
assumes "subgroup H G" "h \<in> H" shows "h [^] (k :: int) \<in> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
128 |
using group.int_pow_closed[OF subgroup_imp_group[OF assms(1)]] assms(2) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
129 |
unfolding int_pow_consistent[OF assms] by simp |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
131 |
lemma (in group) generate_pow: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
132 |
assumes "a \<in> carrier G" shows "generate G { a } = { a [^] (k :: int) | k. k \<in> UNIV }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
133 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
134 |
show "{ a [^] (k :: int) | k. k \<in> UNIV } \<subseteq> generate G { a }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
135 |
using subgroup_int_pow_closed[OF generate_is_subgroup[of "{ a }"] incl[of a]] assms by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
136 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
137 |
show "generate G { a } \<subseteq> { a [^] (k :: int) | k. k \<in> UNIV }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
138 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
139 |
fix h assume "h \<in> generate G { a }" hence "\<exists>k :: int. h = a [^] k" |
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
140 |
proof (induction) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
141 |
case one |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
142 |
then show ?case |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
143 |
using int_pow_0 [of G] by metis |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
144 |
next |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
145 |
case (incl h) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
146 |
then show ?case |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
147 |
by (metis assms int_pow_1 singletonD) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
148 |
next |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
149 |
case (inv h) |
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
150 |
then show ?case |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
151 |
by (metis assms int_pow_1 int_pow_neg singletonD) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
next |
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
153 |
case (eng h1 h2) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
154 |
then show ?case |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
155 |
using assms by (metis int_pow_mult) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
156 |
qed |
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
157 |
then show "h \<in> { a [^] (k :: int) | k. k \<in> UNIV }" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
158 |
by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
159 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
160 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
161 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
162 |
corollary (in group) generate_one: "generate G { \<one> } = { \<one> }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
163 |
using generate_pow[of "\<one>", OF one_closed] by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
164 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
165 |
corollary (in group) generate_empty: "generate G {} = { \<one> }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
166 |
using mono_generate[of "{}" "{ \<one> }"] generate.one unfolding generate_one by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
168 |
lemma (in group_hom) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
169 |
"subgroup K G \<Longrightarrow> subgroup (h ` K) H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
170 |
using subgroup_img_is_subgroup by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
171 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
172 |
lemma (in group_hom) generate_img: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
173 |
assumes "K \<subseteq> carrier G" shows "generate H (h ` K) = h ` (generate G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
174 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
175 |
have "h ` K \<subseteq> h ` (generate G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
176 |
using incl[of _ K G] by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
177 |
thus "generate H (h ` K) \<subseteq> h ` (generate G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
178 |
using generate_subgroup_incl subgroup_img_is_subgroup[OF G.generate_is_subgroup[OF assms]] by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
179 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
180 |
show "h ` (generate G K) \<subseteq> generate H (h ` K)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
181 |
proof |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
182 |
fix a assume "a \<in> h ` (generate G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
183 |
then obtain k where "k \<in> generate G K" "a = h k" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
184 |
by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
185 |
show "a \<in> generate H (h ` K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
186 |
using \<open>k \<in> generate G K\<close> unfolding \<open>a = h k\<close> |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
187 |
proof (induct k, auto simp add: generate.one[of H] generate.incl[of _ "h ` K" H]) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
188 |
case (inv k) show ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
189 |
using assms generate.inv[of "h k" "h ` K" H] inv by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
190 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
191 |
case eng show ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
192 |
using generate.eng[OF eng(2,4)] eng(1,3)[THEN G.generate_in_carrier[OF assms]] by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
196 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
198 |
section \<open>Derived Subgroup\<close> |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
200 |
subsection \<open>Definitions\<close> |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
202 |
abbreviation derived_set :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
203 |
where "derived_set G H \<equiv> |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
204 |
\<Union>h1 \<in> H. (\<Union>h2 \<in> H. { h1 \<otimes>\<^bsub>G\<^esub> h2 \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> h1) \<otimes>\<^bsub>G\<^esub> (inv\<^bsub>G\<^esub> h2) })" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
definition derived :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
"derived G H = generate G (derived_set G H)" |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
209 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
210 |
subsection \<open>Basic Properties\<close> |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
211 |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
212 |
lemma (in group) derived_set_incl: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
213 |
assumes "K \<subseteq> H" "subgroup H G" shows "derived_set G K \<subseteq> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
214 |
using assms(1) subgroupE(3-4)[OF assms(2)] by (auto simp add: subset_iff) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
216 |
lemma (in group) derived_incl: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
217 |
assumes "K \<subseteq> H" "subgroup H G" shows "derived G K \<subseteq> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
218 |
using generate_subgroup_incl[OF derived_set_incl] assms unfolding derived_def by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
220 |
lemma (in group) derived_set_in_carrier: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
221 |
assumes "H \<subseteq> carrier G" shows "derived_set G H \<subseteq> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
222 |
using derived_set_incl[OF assms subgroup_self] . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
223 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
224 |
lemma (in group) derived_in_carrier: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
225 |
assumes "H \<subseteq> carrier G" shows "derived G H \<subseteq> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
226 |
using derived_incl[OF assms subgroup_self] . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
227 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
228 |
lemma (in group) exp_of_derived_in_carrier: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
229 |
assumes "H \<subseteq> carrier G" shows "(derived G ^^ n) H \<subseteq> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
230 |
using assms derived_in_carrier by (induct n) (auto) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
231 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
232 |
lemma (in group) derived_is_subgroup: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
233 |
assumes "H \<subseteq> carrier G" shows "subgroup (derived G H) G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
234 |
unfolding derived_def using generate_is_subgroup[OF derived_set_in_carrier[OF assms]] . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
235 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
236 |
lemma (in group) exp_of_derived_is_subgroup: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
237 |
assumes "subgroup H G" shows "subgroup ((derived G ^^ n) H) G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
238 |
using assms derived_is_subgroup subgroup.subset by (induct n) (auto) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
239 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
240 |
lemma (in group) exp_of_derived_is_subgroup': |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
241 |
assumes "H \<subseteq> carrier G" shows "subgroup ((derived G ^^ (Suc n)) H) G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
242 |
using assms derived_is_subgroup[OF subgroup.subset] derived_is_subgroup by (induct n) (auto) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
243 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
244 |
lemma (in group) mono_derived_set: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
245 |
assumes "K \<subseteq> H" shows "derived_set G K \<subseteq> derived_set G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
246 |
using assms by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
247 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
248 |
lemma (in group) mono_derived: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
249 |
assumes "K \<subseteq> H" shows "derived G K \<subseteq> derived G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
250 |
unfolding derived_def using mono_generate[OF mono_derived_set[OF assms]] . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
251 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
252 |
lemma (in group) mono_exp_of_derived: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
253 |
assumes "K \<subseteq> H" shows "(derived G ^^ n) K \<subseteq> (derived G ^^ n) H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
254 |
using assms mono_derived by (induct n) (auto) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
255 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
256 |
lemma (in group) derived_set_consistent: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
257 |
assumes "K \<subseteq> H" "subgroup H G" shows "derived_set (G \<lparr> carrier := H \<rparr>) K = derived_set G K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
258 |
using m_inv_consistent[OF assms(2)] assms(1) by (auto simp add: subset_iff) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
259 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
260 |
lemma (in group) derived_consistent: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
261 |
assumes "K \<subseteq> H" "subgroup H G" shows "derived (G \<lparr> carrier := H \<rparr>) K = derived G K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
262 |
using generate_consistent[OF derived_set_incl] derived_set_consistent assms by (simp add: derived_def) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
263 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
264 |
lemma (in comm_group) derived_eq_singleton: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
265 |
assumes "H \<subseteq> carrier G" shows "derived G H = { \<one> }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
266 |
proof (cases "derived_set G H = {}") |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
267 |
case True show ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
268 |
using generate_empty unfolding derived_def True by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
269 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
270 |
case False |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
271 |
have aux_lemma: "h \<in> derived_set G H \<Longrightarrow> h = \<one>" for h |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
272 |
using assms by (auto simp add: subset_iff) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
273 |
(metis (no_types, lifting) m_comm m_closed inv_closed inv_solve_right l_inv l_inv_ex) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
274 |
have "derived_set G H = { \<one> }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
275 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
276 |
show "derived_set G H \<subseteq> { \<one> }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
277 |
using aux_lemma by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
278 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
279 |
obtain h where h: "h \<in> derived_set G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
280 |
using False by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
281 |
thus "{ \<one> } \<subseteq> derived_set G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
282 |
using aux_lemma[OF h] by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
283 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
284 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
285 |
using generate_one unfolding derived_def by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
286 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
288 |
lemma (in group) derived_is_normal: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
289 |
assumes "H \<lhd> G" shows "derived G H \<lhd> G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
290 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
291 |
interpret H: normal H G |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
292 |
using assms . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
293 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
294 |
show ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
295 |
unfolding derived_def |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
296 |
proof (rule normal_generateI[OF derived_set_in_carrier[OF H.subset]]) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
297 |
fix h g assume "h \<in> derived_set G H" and g: "g \<in> carrier G" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
298 |
then obtain h1 h2 where h: "h1 \<in> H" "h2 \<in> H" "h = h1 \<otimes> h2 \<otimes> inv h1 \<otimes> inv h2" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
299 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
300 |
hence in_carrier: "h1 \<in> carrier G" "h2 \<in> carrier G" "g \<in> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
301 |
using H.subset g by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
302 |
have "g \<otimes> h \<otimes> inv g = |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
303 |
g \<otimes> h1 \<otimes> (inv g \<otimes> g) \<otimes> h2 \<otimes> (inv g \<otimes> g) \<otimes> inv h1 \<otimes> (inv g \<otimes> g) \<otimes> inv h2 \<otimes> inv g" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
304 |
unfolding h(3) by (simp add: in_carrier m_assoc) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
305 |
also have " ... = |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
306 |
(g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> (g \<otimes> inv h1 \<otimes> inv g) \<otimes> (g \<otimes> inv h2 \<otimes> inv g)" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
307 |
using in_carrier m_assoc inv_closed m_closed by presburger |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
308 |
finally have "g \<otimes> h \<otimes> inv g = |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
309 |
(g \<otimes> h1 \<otimes> inv g) \<otimes> (g \<otimes> h2 \<otimes> inv g) \<otimes> inv (g \<otimes> h1 \<otimes> inv g) \<otimes> inv (g \<otimes> h2 \<otimes> inv g)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
310 |
by (simp add: in_carrier inv_mult_group m_assoc) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
311 |
thus "g \<otimes> h \<otimes> inv g \<in> derived_set G H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
312 |
using h(1-2)[THEN H.inv_op_closed2[OF g]] by auto |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
316 |
lemma (in group) normal_self: "carrier G \<lhd> G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
317 |
by (rule normal_invI[OF subgroup_self], simp) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
318 |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
319 |
corollary (in group) derived_self_is_normal: "derived G (carrier G) \<lhd> G" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
320 |
using derived_is_normal[OF normal_self] . |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
322 |
corollary (in group) derived_subgroup_is_normal: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
323 |
assumes "subgroup H G" shows "derived G H \<lhd> G \<lparr> carrier := H \<rparr>" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
324 |
using group.derived_self_is_normal[OF subgroup_imp_group[OF assms]] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
325 |
derived_consistent[OF _ assms] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
326 |
by simp |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
328 |
corollary (in group) derived_quot_is_group: "group (G Mod (derived G (carrier G)))" |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
329 |
using normal.factorgroup_is_group[OF derived_self_is_normal] by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
330 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
331 |
lemma (in group) derived_quot_is_comm_group: "comm_group (G Mod (derived G (carrier G)))" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
332 |
proof (rule group.group_comm_groupI[OF derived_quot_is_group], simp add: FactGroup_def) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
333 |
interpret DG: normal "derived G (carrier G)" G |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
334 |
using derived_self_is_normal . |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
335 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
336 |
fix H K assume "H \<in> rcosets derived G (carrier G)" and "K \<in> rcosets derived G (carrier G)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
337 |
then obtain g1 g2 |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
338 |
where g1: "g1 \<in> carrier G" "H = derived G (carrier G) #> g1" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
339 |
and g2: "g2 \<in> carrier G" "K = derived G (carrier G) #> g2" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
340 |
unfolding RCOSETS_def by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
341 |
hence "H <#> K = derived G (carrier G) #> (g1 \<otimes> g2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
342 |
by (simp add: DG.rcos_sum) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
343 |
also have " ... = derived G (carrier G) #> (g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
344 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
345 |
{ fix g1 g2 assume g1: "g1 \<in> carrier G" and g2: "g2 \<in> carrier G" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
346 |
have "derived G (carrier G) #> (g1 \<otimes> g2) \<subseteq> derived G (carrier G) #> (g2 \<otimes> g1)" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
347 |
proof |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
348 |
fix h assume "h \<in> derived G (carrier G) #> (g1 \<otimes> g2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
349 |
then obtain g' where h: "g' \<in> carrier G" "g' \<in> derived G (carrier G)" "h = g' \<otimes> (g1 \<otimes> g2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
350 |
using DG.subset unfolding r_coset_def by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
351 |
hence "h = g' \<otimes> (g1 \<otimes> g2) \<otimes> (inv g1 \<otimes> inv g2 \<otimes> g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
352 |
using g1 g2 by (simp add: m_assoc) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
353 |
hence "h = (g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2)) \<otimes> (g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
354 |
using h(1) g1 g2 inv_closed m_assoc m_closed by presburger |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
355 |
moreover have "g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2 \<in> derived G (carrier G)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
356 |
using incl[of _ "derived_set G (carrier G)"] g1 g2 unfolding derived_def by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
357 |
hence "g' \<otimes> (g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2) \<in> derived G (carrier G)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
358 |
using DG.m_closed[OF h(2)] by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
359 |
ultimately show "h \<in> derived G (carrier G) #> (g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
360 |
unfolding r_coset_def by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
361 |
qed } |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
362 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
363 |
using g1(1) g2(1) by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
364 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
365 |
also have " ... = K <#> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
366 |
by (simp add: g1 g2 DG.rcos_sum) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
367 |
finally show "H <#> K = K <#> H" . |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
368 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
369 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
370 |
corollary (in group) derived_quot_of_subgroup_is_comm_group: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
371 |
assumes "subgroup H G" shows "comm_group ((G \<lparr> carrier := H \<rparr>) Mod (derived G H))" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
372 |
using group.derived_quot_is_comm_group[OF subgroup_imp_group[OF assms]] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
373 |
derived_consistent[OF _ assms] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
374 |
by simp |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
375 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
376 |
proposition (in group) derived_minimal: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
377 |
assumes "H \<lhd> G" and "comm_group (G Mod H)" shows "derived G (carrier G) \<subseteq> H" |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
378 |
proof - |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
379 |
interpret H: normal H G |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
380 |
using assms(1) . |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
381 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
382 |
show ?thesis |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
383 |
unfolding derived_def |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
384 |
proof (rule generate_subgroup_incl[OF _ H.subgroup_axioms]) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
385 |
show "derived_set G (carrier G) \<subseteq> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
386 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
387 |
fix h assume "h \<in> derived_set G (carrier G)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
388 |
then obtain g1 g2 where h: "g1 \<in> carrier G" "g2 \<in> carrier G" "h = g1 \<otimes> g2 \<otimes> inv g1 \<otimes> inv g2" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
389 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
390 |
have "H #> (g1 \<otimes> g2) = (H #> g1) <#> (H #> g2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
391 |
by (simp add: h(1-2) H.rcos_sum) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
392 |
also have " ... = (H #> g2) <#> (H #> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
393 |
using comm_groupE(4)[OF assms(2)] h(1-2) unfolding FactGroup_def RCOSETS_def by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
394 |
also have " ... = H #> (g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
395 |
by (simp add: h(1-2) H.rcos_sum) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
396 |
finally have "H #> (g1 \<otimes> g2) = H #> (g2 \<otimes> g1)" . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
397 |
then obtain h' where "h' \<in> H" "\<one> \<otimes> (g1 \<otimes> g2) = h' \<otimes> (g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
398 |
using H.one_closed unfolding r_coset_def by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
399 |
thus "h \<in> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
400 |
using h m_assoc by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
401 |
qed |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
402 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
403 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
404 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
405 |
proposition (in group) derived_of_subgroup_minimal: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
406 |
assumes "K \<lhd> G \<lparr> carrier := H \<rparr>" "subgroup H G" and "comm_group ((G \<lparr> carrier := H \<rparr>) Mod K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
407 |
shows "derived G H \<subseteq> K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
408 |
using group.derived_minimal[OF subgroup_imp_group[OF assms(2)] assms(1,3)] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
409 |
derived_consistent[OF _ assms(2)] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
410 |
by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
411 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
412 |
lemma (in group_hom) derived_img: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
413 |
assumes "K \<subseteq> carrier G" shows "derived H (h ` K) = h ` (derived G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
414 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
415 |
have "derived_set H (h ` K) = h ` (derived_set G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
416 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
417 |
show "derived_set H (h ` K) \<subseteq> h ` derived_set G K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
418 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
419 |
fix a assume "a \<in> derived_set H (h ` K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
420 |
then obtain k1 k2 |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
421 |
where "k1 \<in> K" "k2 \<in> K" "a = (h k1) \<otimes>\<^bsub>H\<^esub> (h k2) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
422 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
423 |
hence "a = h (k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
424 |
using assms by (simp add: subset_iff) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
425 |
from this \<open>k1 \<in> K\<close> and \<open>k2 \<in> K\<close> show "a \<in> h ` derived_set G K" by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
426 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
427 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
428 |
show "h ` (derived_set G K) \<subseteq> derived_set H (h ` K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
429 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
430 |
fix a assume "a \<in> h ` (derived_set G K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
431 |
then obtain k1 k2 where "k1 \<in> K" "k2 \<in> K" "a = h (k1 \<otimes> k2 \<otimes> inv k1 \<otimes> inv k2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
432 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
433 |
hence "a = (h k1) \<otimes>\<^bsub>H\<^esub> (h k2) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k1) \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h k2)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
434 |
using assms by (simp add: subset_iff) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
435 |
from this \<open>k1 \<in> K\<close> and \<open>k2 \<in> K\<close> show "a \<in> derived_set H (h ` K)" by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
436 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
437 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
438 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
439 |
unfolding derived_def using generate_img[OF G.derived_set_in_carrier[OF assms]] by simp |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
440 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
441 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
442 |
lemma (in group_hom) exp_of_derived_img: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
443 |
assumes "K \<subseteq> carrier G" shows "(derived H ^^ n) (h ` K) = h ` ((derived G ^^ n) K)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
444 |
using derived_img[OF G.exp_of_derived_in_carrier[OF assms]] by (induct n) (auto) |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
445 |
|
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
446 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
447 |
subsection \<open>Generated subgroup of a group\<close> |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
448 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
449 |
definition subgroup_generated :: "('a, 'b) monoid_scheme \<Rightarrow> 'a set \<Rightarrow> ('a, 'b) monoid_scheme" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
450 |
where "subgroup_generated G S = G\<lparr>carrier := generate G (carrier G \<inter> S)\<rparr>" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
451 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
452 |
lemma carrier_subgroup_generated: "carrier (subgroup_generated G S) = generate G (carrier G \<inter> S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
453 |
by (auto simp: subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
454 |
|
70027
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
455 |
lemma (in group) subgroup_generated_subset_carrier_subset: |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
456 |
"S \<subseteq> carrier G \<Longrightarrow> S \<subseteq> carrier(subgroup_generated G S)" |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
457 |
by (simp add: Int_absorb1 carrier_subgroup_generated generate.incl subsetI) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
458 |
|
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
459 |
lemma (in group) subgroup_generated_minimal: |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
460 |
"\<lbrakk>subgroup H G; S \<subseteq> H\<rbrakk> \<Longrightarrow> carrier(subgroup_generated G S) \<subseteq> H" |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
461 |
by (simp add: carrier_subgroup_generated generate_subgroup_incl le_infI2) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
462 |
|
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
463 |
lemma (in group) carrier_subgroup_generated_subset: |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
464 |
"carrier (subgroup_generated G A) \<subseteq> carrier G" |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
465 |
apply (clarsimp simp: carrier_subgroup_generated) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
466 |
by (meson Int_lower1 generate_in_carrier) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
467 |
|
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
468 |
lemma (in group) group_subgroup_generated [simp]: "group (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
469 |
unfolding subgroup_generated_def |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
470 |
by (simp add: generate_is_subgroup subgroup_imp_group) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
471 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
472 |
lemma (in group) abelian_subgroup_generated: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
473 |
assumes "comm_group G" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
474 |
shows "comm_group (subgroup_generated G S)" (is "comm_group ?GS") |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
475 |
proof (rule group.group_comm_groupI) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
476 |
show "Group.group ?GS" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
477 |
by simp |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
478 |
next |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
479 |
fix x y |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
480 |
assume "x \<in> carrier ?GS" "y \<in> carrier ?GS" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
481 |
with assms show "x \<otimes>\<^bsub>?GS\<^esub> y = y \<otimes>\<^bsub>?GS\<^esub> x" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
482 |
apply (simp add: subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
483 |
by (meson Int_lower1 comm_groupE(4) generate_in_carrier) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
484 |
qed |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
485 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
486 |
lemma (in group) subgroup_of_subgroup_generated: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
487 |
assumes "H \<subseteq> B" "subgroup H G" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
488 |
shows "subgroup H (subgroup_generated G B)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
489 |
proof unfold_locales |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
490 |
fix x |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
491 |
assume "x \<in> H" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
492 |
with assms show "inv\<^bsub>subgroup_generated G B\<^esub> x \<in> H" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
493 |
unfolding subgroup_generated_def |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
494 |
by (metis IntI Int_commute Int_lower2 generate.incl generate_is_subgroup m_inv_consistent subgroup_def subsetCE) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
495 |
next |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
496 |
show "H \<subseteq> carrier (subgroup_generated G B)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
497 |
using assms apply (auto simp: carrier_subgroup_generated) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
498 |
by (metis Int_iff generate.incl inf.orderE subgroup.mem_carrier) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
499 |
qed (use assms in \<open>auto simp: subgroup_generated_def subgroup_def\<close>) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
500 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
501 |
lemma carrier_subgroup_generated_alt: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
502 |
assumes "Group.group G" "S \<subseteq> carrier G" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
503 |
shows "carrier (subgroup_generated G S) = \<Inter>{H. subgroup H G \<and> carrier G \<inter> S \<subseteq> H}" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
504 |
using assms by (auto simp: group.generate_minimal subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
505 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
506 |
lemma one_subgroup_generated [simp]: "\<one>\<^bsub>subgroup_generated G S\<^esub> = \<one>\<^bsub>G\<^esub>" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
507 |
by (auto simp: subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
508 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
509 |
lemma mult_subgroup_generated [simp]: "mult (subgroup_generated G S) = mult G" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
510 |
by (auto simp: subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
511 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
512 |
lemma (in group) inv_subgroup_generated [simp]: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
513 |
assumes "f \<in> carrier (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
514 |
shows "inv\<^bsub>subgroup_generated G S\<^esub> f = inv f" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
515 |
proof (rule group.inv_equality) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
516 |
show "Group.group (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
517 |
by simp |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
518 |
have [simp]: "f \<in> carrier G" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
519 |
by (metis Int_lower1 assms carrier_subgroup_generated generate_in_carrier) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
520 |
show "inv f \<otimes>\<^bsub>subgroup_generated G S\<^esub> f = \<one>\<^bsub>subgroup_generated G S\<^esub>" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
521 |
by (simp add: assms) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
522 |
show "f \<in> carrier (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
523 |
using assms by (simp add: generate.incl subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
524 |
show "inv f \<in> carrier (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
525 |
using assms by (simp add: subgroup_generated_def generate_m_inv_closed) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
526 |
qed |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
527 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
528 |
lemma subgroup_generated_restrict [simp]: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
529 |
"subgroup_generated G (carrier G \<inter> S) = subgroup_generated G S" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
530 |
by (simp add: subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
531 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
532 |
lemma (in subgroup) carrier_subgroup_generated_subgroup [simp]: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
533 |
"carrier (subgroup_generated G H) = H" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
534 |
by (auto simp: generate.incl carrier_subgroup_generated elim: generate.induct) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
535 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
536 |
lemma (in group) subgroup_subgroup_generated_iff: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
537 |
"subgroup H (subgroup_generated G B) \<longleftrightarrow> subgroup H G \<and> H \<subseteq> carrier(subgroup_generated G B)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
538 |
(is "?lhs = ?rhs") |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
539 |
proof |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
540 |
assume L: ?lhs |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
541 |
then have Hsub: "H \<subseteq> generate G (carrier G \<inter> B)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
542 |
by (simp add: subgroup_def subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
543 |
then have H: "H \<subseteq> carrier G" "H \<subseteq> carrier(subgroup_generated G B)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
544 |
unfolding carrier_subgroup_generated |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
545 |
using generate_incl by blast+ |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
546 |
with Hsub have "subgroup H G" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
547 |
by (metis Int_commute Int_lower2 L carrier_subgroup_generated generate_consistent |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
548 |
generate_is_subgroup inf.orderE subgroup.carrier_subgroup_generated_subgroup subgroup_generated_def) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
549 |
with H show ?rhs |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
550 |
by blast |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
551 |
next |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
552 |
assume ?rhs |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
553 |
then show ?lhs |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
554 |
by (simp add: generate_is_subgroup subgroup_generated_def subgroup_incl) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
555 |
qed |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
556 |
|
70027
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
557 |
lemma (in group) subgroup_subgroup_generated: |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
558 |
"subgroup (carrier(subgroup_generated G S)) G" |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
559 |
using group.subgroup_self group_subgroup_generated subgroup_subgroup_generated_iff by blast |
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
560 |
|
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
561 |
lemma pow_subgroup_generated: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
562 |
"pow (subgroup_generated G S) = (pow G :: 'a \<Rightarrow> nat \<Rightarrow> 'a)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
563 |
proof - |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
564 |
have "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n" for x and n::nat |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
565 |
by (induction n) auto |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
566 |
then show ?thesis |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
567 |
by force |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
568 |
qed |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
569 |
|
70027
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
570 |
lemma (in group) subgroup_generated2 [simp]: "subgroup_generated (subgroup_generated G S) S = subgroup_generated G S" |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
571 |
proof - |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
572 |
have *: "\<And>A. carrier G \<inter> A \<subseteq> carrier (subgroup_generated (subgroup_generated G A) A)" |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
573 |
by (metis (no_types, hide_lams) Int_assoc carrier_subgroup_generated generate.incl inf.order_iff subset_iff) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
574 |
show ?thesis |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
575 |
apply (auto intro!: monoid.equality) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
576 |
using group.carrier_subgroup_generated_subset group_subgroup_generated apply blast |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
577 |
apply (metis (no_types, hide_lams) "*" group.subgroup_subgroup_generated group_subgroup_generated subgroup_generated_minimal |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
578 |
subgroup_generated_restrict subgroup_subgroup_generated_iff subset_eq) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
579 |
apply (simp add: subgroup_generated_def) |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
580 |
done |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
581 |
qed |
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
582 |
|
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
583 |
lemma (in group) int_pow_subgroup_generated: |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
584 |
fixes n::int |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
585 |
assumes "x \<in> carrier (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
586 |
shows "x [^]\<^bsub>subgroup_generated G S\<^esub> n = x [^]\<^bsub>G\<^esub> n" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
587 |
proof - |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
588 |
have "x [^] nat (- n) \<in> carrier (subgroup_generated G S)" |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
589 |
by (metis assms group.is_monoid group_subgroup_generated monoid.nat_pow_closed pow_subgroup_generated) |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
590 |
then show ?thesis |
70027
94494b92d8d0
some new group theory results: integer group, trivial group, etc.
paulson <lp15@cam.ac.uk>
parents:
70019
diff
changeset
|
591 |
by (metis group.inv_subgroup_generated int_pow_def2 is_group pow_subgroup_generated) |
69749
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
592 |
qed |
10e48c47a549
some new results in group theory
paulson <lp15@cam.ac.uk>
parents:
69122
diff
changeset
|
593 |
|
70019
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
594 |
lemma kernel_from_subgroup_generated [simp]: |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
595 |
"subgroup S G \<Longrightarrow> kernel (subgroup_generated G S) H f = kernel G H f \<inter> S" |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
596 |
using subgroup.carrier_subgroup_generated_subgroup subgroup.subset |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
597 |
by (fastforce simp add: kernel_def set_eq_iff) |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
598 |
|
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
599 |
lemma kernel_to_subgroup_generated [simp]: |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
600 |
"kernel G (subgroup_generated H S) f = kernel G H f" |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
601 |
by (simp add: kernel_def) |
095dce9892e8
A few results in Algebra, and bits for Analysis
paulson <lp15@cam.ac.uk>
parents:
69749
diff
changeset
|
602 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
603 |
end |