author | wenzelm |
Sat, 03 Nov 2018 20:09:39 +0100 | |
changeset 69227 | 71b48b749836 |
parent 69122 | 1b5178abaf97 |
child 69749 | 10e48c47a549 |
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" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
140 |
proof (induction, metis int_pow_0[of a], metis singletonD int_pow_1[OF assms]) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
141 |
case (inv h) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
142 |
hence "inv h = a [^] ((- 1) :: int)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
143 |
using assms unfolding int_pow_def2 by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
144 |
thus ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
145 |
by blast |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
next |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
147 |
case eng thus ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
148 |
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
|
149 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
150 |
thus "h \<in> { 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
|
151 |
by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
152 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
153 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
154 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
155 |
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
|
156 |
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
|
157 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
158 |
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
|
159 |
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
|
160 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
161 |
lemma (in group_hom) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
162 |
"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
|
163 |
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
|
164 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
165 |
lemma (in group_hom) generate_img: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
166 |
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
|
167 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
168 |
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
|
169 |
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
|
170 |
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
|
171 |
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
|
172 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
173 |
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
|
174 |
proof |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
175 |
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
|
176 |
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
|
177 |
by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
case (inv k) show ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
182 |
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
|
183 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
184 |
case eng show ?case |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
185 |
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
|
186 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
191 |
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
|
192 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
193 |
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
|
194 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
195 |
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
|
196 |
where "derived_set G H \<equiv> |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
197 |
\<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
|
198 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
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
|
200 |
"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
|
201 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
202 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
203 |
subsection \<open>Basic Properties\<close> |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
204 |
|
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 |
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
|
206 |
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
|
207 |
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
|
208 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
lemma (in group) derived_incl: |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
210 |
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
|
211 |
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
|
212 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
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
|
216 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
217 |
lemma (in group) derived_in_carrier: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
218 |
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
|
219 |
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
|
220 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
221 |
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
|
222 |
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
|
223 |
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
|
224 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
225 |
lemma (in group) derived_is_subgroup: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
226 |
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
|
227 |
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
|
228 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
233 |
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
|
234 |
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
|
235 |
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
|
236 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
237 |
lemma (in group) mono_derived_set: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
238 |
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
|
239 |
using assms by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
240 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
241 |
lemma (in group) mono_derived: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
242 |
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
|
243 |
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
|
244 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
245 |
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
|
246 |
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
|
247 |
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
|
248 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
249 |
lemma (in group) derived_set_consistent: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
250 |
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
|
251 |
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
|
252 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
253 |
lemma (in group) derived_consistent: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
254 |
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
|
255 |
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
|
256 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
257 |
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
|
258 |
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
|
259 |
proof (cases "derived_set G H = {}") |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
260 |
case True show ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
261 |
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
|
262 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
263 |
case False |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
264 |
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
|
265 |
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
|
266 |
(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
|
267 |
have "derived_set G H = { \<one> }" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
268 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
269 |
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
|
270 |
using aux_lemma by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
271 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
272 |
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
|
273 |
using False by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
274 |
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
|
275 |
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
|
276 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
277 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
278 |
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
|
279 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
280 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
281 |
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
|
282 |
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
|
283 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
284 |
interpret H: normal H G |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
285 |
using assms . |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
286 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
287 |
show ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
288 |
unfolding derived_def |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
293 |
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
|
294 |
using H.subset g by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
295 |
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
|
296 |
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
|
297 |
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
|
298 |
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
|
299 |
(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
|
300 |
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
|
301 |
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
|
302 |
(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
|
303 |
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
|
304 |
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
|
305 |
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
|
306 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
307 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
308 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
309 |
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
|
310 |
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
|
311 |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
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
|
313 |
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
|
314 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
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
|
316 |
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
|
317 |
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
|
318 |
derived_consistent[OF _ assms] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
319 |
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
|
320 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
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
|
322 |
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
|
323 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
324 |
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
|
325 |
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
|
326 |
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
|
327 |
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
|
328 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
329 |
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
|
330 |
then obtain g1 g2 |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
331 |
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
|
332 |
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
|
333 |
unfolding RCOSETS_def by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
334 |
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
|
335 |
by (simp add: DG.rcos_sum) |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
336 |
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
|
337 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
338 |
{ 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
|
339 |
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
|
340 |
proof |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
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
|
347 |
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
|
348 |
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
|
349 |
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
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
unfolding r_coset_def by blast |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
354 |
qed } |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
355 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
356 |
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
|
357 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
358 |
also have " ... = K <#> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
359 |
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
|
360 |
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
|
361 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
362 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
363 |
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
|
364 |
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
|
365 |
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
|
366 |
derived_consistent[OF _ assms] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
367 |
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
|
368 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
369 |
proposition (in group) derived_minimal: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
370 |
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
|
371 |
proof - |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
372 |
interpret H: normal H G |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
373 |
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
|
374 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
375 |
show ?thesis |
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
376 |
unfolding derived_def |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
377 |
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
|
378 |
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
|
379 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
380 |
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
|
381 |
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
|
382 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
383 |
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
|
384 |
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
|
385 |
also have " ... = (H #> g2) <#> (H #> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
386 |
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
|
387 |
also have " ... = H #> (g2 \<otimes> g1)" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
388 |
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
|
389 |
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
|
390 |
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
|
391 |
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
|
392 |
thus "h \<in> H" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
393 |
using h m_assoc by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
394 |
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
|
395 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
396 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
397 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
398 |
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
|
399 |
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
|
400 |
shows "derived G H \<subseteq> K" |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
401 |
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
|
402 |
derived_consistent[OF _ assms(2)] |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
403 |
by simp |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
404 |
|
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
405 |
lemma (in group_hom) derived_img: |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
406 |
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
|
407 |
proof - |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
408 |
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
|
409 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
410 |
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
|
411 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
412 |
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
|
413 |
then obtain k1 k2 |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
414 |
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
|
415 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
416 |
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
|
417 |
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
|
418 |
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
|
419 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
420 |
next |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
421 |
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
|
422 |
proof |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
423 |
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
|
424 |
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
|
425 |
by auto |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
426 |
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
|
427 |
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
|
428 |
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
|
429 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
430 |
qed |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
431 |
thus ?thesis |
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
432 |
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
|
433 |
qed |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
434 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
435 |
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
|
436 |
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
|
437 |
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
|
438 |
|
69122
1b5178abaf97
updates to Algebra from Baillon and de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68687
diff
changeset
|
439 |
end |