author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 32960  69916a850301 
child 35416  d8d7d1b785af 
permissions  rwrr 
14706  1 
(* Title: HOL/Algebra/Coset.thy 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

2 
Author: Florian Kammueller, with new proofs by L C Paulson, and 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

3 
Stephan Hohe 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

4 
*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

5 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27698
diff
changeset

6 
theory Coset imports Group begin 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

7 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

8 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

9 
section {*Cosets and Quotient Groups*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

10 

14651  11 
constdefs (structure G) 
14963  12 
r_coset :: "[_, 'a set, 'a] \<Rightarrow> 'a set" (infixl "#>\<index>" 60) 
13 
"H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

14 

14963  15 
l_coset :: "[_, 'a, 'a set] \<Rightarrow> 'a set" (infixl "<#\<index>" 60) 
16 
"a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

17 

14963  18 
RCOSETS :: "[_, 'a set] \<Rightarrow> ('a set)set" ("rcosets\<index> _" [81] 80) 
19 
"rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}" 

20 

21 
set_mult :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60) 

22 
"H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

23 

14963  24 
SET_INV :: "[_,'a set] \<Rightarrow> 'a set" ("set'_inv\<index> _" [81] 80) 
25 
"set_inv H \<equiv> \<Union>h\<in>H. {inv h}" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

26 

14963  27 

28 
locale normal = subgroup + group + 

29 
assumes coset_eq: "(\<forall>x \<in> carrier G. H #> x = x <# H)" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

30 

19380  31 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20318
diff
changeset

32 
normal_rel :: "['a set, ('a, 'b) monoid_scheme] \<Rightarrow> bool" (infixl "\<lhd>" 60) where 
19380  33 
"H \<lhd> G \<equiv> normal H G" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

34 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

35 

14803  36 
subsection {*Basic Properties of Cosets*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

37 

14747  38 
lemma (in group) coset_mult_assoc: 
39 
"[ M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G ] 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

40 
==> (M #> g) #> h = M #> (g \<otimes> h)" 
14747  41 
by (force simp add: r_coset_def m_assoc) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

42 

14747  43 
lemma (in group) coset_mult_one [simp]: "M \<subseteq> carrier G ==> M #> \<one> = M" 
44 
by (force simp add: r_coset_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

45 

14747  46 
lemma (in group) coset_mult_inv1: 
14666  47 
"[ M #> (x \<otimes> (inv y)) = M; x \<in> carrier G ; y \<in> carrier G; 
14747  48 
M \<subseteq> carrier G ] ==> M #> x = M #> y" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

49 
apply (erule subst [of concl: "%z. M #> x = z #> y"]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

50 
apply (simp add: coset_mult_assoc m_assoc) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

51 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

52 

14747  53 
lemma (in group) coset_mult_inv2: 
54 
"[ M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M \<subseteq> carrier G ] 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

55 
==> M #> (x \<otimes> (inv y)) = M " 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

56 
apply (simp add: coset_mult_assoc [symmetric]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

57 
apply (simp add: coset_mult_assoc) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

58 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

59 

14747  60 
lemma (in group) coset_join1: 
61 
"[ H #> x = H; x \<in> carrier G; subgroup H G ] ==> x \<in> H" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

62 
apply (erule subst) 
14963  63 
apply (simp add: r_coset_def) 
64 
apply (blast intro: l_one subgroup.one_closed sym) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

65 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

66 

14747  67 
lemma (in group) solve_equation: 
14963  68 
"\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. y = h \<otimes> x" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

69 
apply (rule bexI [of _ "y \<otimes> (inv x)"]) 
14666  70 
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

71 
subgroup.subset [THEN subsetD]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

72 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

73 

14963  74 
lemma (in group) repr_independence: 
75 
"\<lbrakk>y \<in> H #> x; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> H #> x = H #> y" 

76 
by (auto simp add: r_coset_def m_assoc [symmetric] 

77 
subgroup.subset [THEN subsetD] 

78 
subgroup.m_closed solve_equation) 

79 

14747  80 
lemma (in group) coset_join2: 
14963  81 
"\<lbrakk>x \<in> carrier G; subgroup H G; x\<in>H\<rbrakk> \<Longrightarrow> H #> x = H" 
82 
{*Alternative proof is to put @{term "x=\<one>"} in @{text repr_independence}.*} 

83 
by (force simp add: subgroup.m_closed r_coset_def solve_equation) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

84 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

85 
lemma (in monoid) r_coset_subset_G: 
14747  86 
"[ H \<subseteq> carrier G; x \<in> carrier G ] ==> H #> x \<subseteq> carrier G" 
87 
by (auto simp add: r_coset_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

88 

14747  89 
lemma (in group) rcosI: 
90 
"[ h \<in> H; H \<subseteq> carrier G; x \<in> carrier G] ==> h \<otimes> x \<in> H #> x" 

91 
by (auto simp add: r_coset_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

92 

14963  93 
lemma (in group) rcosetsI: 
94 
"\<lbrakk>H \<subseteq> carrier G; x \<in> carrier G\<rbrakk> \<Longrightarrow> H #> x \<in> rcosets H" 

95 
by (auto simp add: RCOSETS_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

96 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

97 
text{*Really needed?*} 
14747  98 
lemma (in group) transpose_inv: 
14666  99 
"[ x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

100 
==> (inv x) \<otimes> z = y" 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

101 
by (force simp add: m_assoc [symmetric]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

102 

14747  103 
lemma (in group) rcos_self: "[ x \<in> carrier G; subgroup H G ] ==> x \<in> H #> x" 
14963  104 
apply (simp add: r_coset_def) 
105 
apply (blast intro: sym l_one subgroup.subset [THEN subsetD] 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

106 
subgroup.one_closed) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

107 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

108 

23350  109 
text (in group) {* Opposite of @{thm [source] "repr_independence"} *} 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

110 
lemma (in group) repr_independenceD: 
27611  111 
assumes "subgroup H G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

112 
assumes ycarr: "y \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

113 
and repr: "H #> x = H #> y" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

114 
shows "y \<in> H #> x" 
27611  115 
proof  
29237  116 
interpret subgroup H G by fact 
27611  117 
show ?thesis apply (subst repr) 
23350  118 
apply (intro rcos_self) 
119 
apply (rule ycarr) 

120 
apply (rule is_subgroup) 

121 
done 

27611  122 
qed 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

123 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

124 
text {* Elements of a right coset are in the carrier *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

125 
lemma (in subgroup) elemrcos_carrier: 
27611  126 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

127 
assumes acarr: "a \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

128 
and a': "a' \<in> H #> a" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

129 
shows "a' \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

130 
proof  
29237  131 
interpret group G by fact 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

132 
from subset and acarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

133 
have "H #> a \<subseteq> carrier G" by (rule r_coset_subset_G) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

134 
from this and a' 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

135 
show "a' \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

136 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

137 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

138 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

139 
lemma (in subgroup) rcos_const: 
27611  140 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

141 
assumes hH: "h \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

142 
shows "H #> h = H" 
27611  143 
proof  
29237  144 
interpret group G by fact 
27611  145 
show ?thesis apply (unfold r_coset_def) 
146 
apply rule 

147 
apply rule 

148 
apply clarsimp 

149 
apply (intro subgroup.m_closed) 

150 
apply (rule is_subgroup) 

23463  151 
apply assumption 
27611  152 
apply (rule hH) 
153 
apply rule 

154 
apply simp 

155 
proof  

156 
fix h' 

157 
assume h'H: "h' \<in> H" 

158 
note carr = hH[THEN mem_carrier] h'H[THEN mem_carrier] 

159 
from carr 

160 
have a: "h' = (h' \<otimes> inv h) \<otimes> h" by (simp add: m_assoc) 

161 
from h'H hH 

162 
have "h' \<otimes> inv h \<in> H" by simp 

163 
from this and a 

164 
show "\<exists>x\<in>H. h' = x \<otimes> h" by fast 

165 
qed 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

166 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

167 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

168 
text {* Step one for lemma @{text "rcos_module"} *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

169 
lemma (in subgroup) rcos_module_imp: 
27611  170 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

171 
assumes xcarr: "x \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

172 
and x'cos: "x' \<in> H #> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

173 
shows "(x' \<otimes> inv x) \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

174 
proof  
29237  175 
interpret group G by fact 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

176 
from xcarr x'cos 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

177 
have x'carr: "x' \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

178 
by (rule elemrcos_carrier[OF is_group]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

179 
from xcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

180 
have ixcarr: "inv x \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

181 
by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

182 
from x'cos 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

183 
have "\<exists>h\<in>H. x' = h \<otimes> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

184 
unfolding r_coset_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

185 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

186 
from this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

187 
obtain h 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

188 
where hH: "h \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

189 
and x': "x' = h \<otimes> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

190 
by auto 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

191 
from hH and subset 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

192 
have hcarr: "h \<in> carrier G" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

193 
note carr = xcarr x'carr hcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

194 
from x' and carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

195 
have "x' \<otimes> (inv x) = (h \<otimes> x) \<otimes> (inv x)" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

196 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

197 
have "\<dots> = h \<otimes> (x \<otimes> inv x)" by (simp add: m_assoc) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

198 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

199 
have "\<dots> = h \<otimes> \<one>" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

200 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

201 
have "\<dots> = h" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

202 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

203 
have "x' \<otimes> (inv x) = h" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

204 
from hH this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

205 
show "x' \<otimes> (inv x) \<in> H" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

206 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

207 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

208 
text {* Step two for lemma @{text "rcos_module"} *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

209 
lemma (in subgroup) rcos_module_rev: 
27611  210 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

211 
assumes carr: "x \<in> carrier G" "x' \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

212 
and xixH: "(x' \<otimes> inv x) \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

213 
shows "x' \<in> H #> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

214 
proof  
29237  215 
interpret group G by fact 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

216 
from xixH 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

217 
have "\<exists>h\<in>H. x' \<otimes> (inv x) = h" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

218 
from this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

219 
obtain h 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

220 
where hH: "h \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

221 
and hsym: "x' \<otimes> (inv x) = h" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

222 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

223 
from hH subset have hcarr: "h \<in> carrier G" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

224 
note carr = carr hcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

225 
from hsym[symmetric] have "h \<otimes> x = x' \<otimes> (inv x) \<otimes> x" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

226 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

227 
have "\<dots> = x' \<otimes> ((inv x) \<otimes> x)" by (simp add: m_assoc) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

228 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

229 
have "\<dots> = x' \<otimes> \<one>" by (simp add: l_inv) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

230 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

231 
have "\<dots> = x'" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

232 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

233 
have "h \<otimes> x = x'" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

234 
from this[symmetric] and hH 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

235 
show "x' \<in> H #> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

236 
unfolding r_coset_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

237 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

238 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

239 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

240 
text {* Module property of right cosets *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

241 
lemma (in subgroup) rcos_module: 
27611  242 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

243 
assumes carr: "x \<in> carrier G" "x' \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

244 
shows "(x' \<in> H #> x) = (x' \<otimes> inv x \<in> H)" 
27611  245 
proof  
29237  246 
interpret group G by fact 
27611  247 
show ?thesis proof assume "x' \<in> H #> x" 
248 
from this and carr 

249 
show "x' \<otimes> inv x \<in> H" 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

250 
by (intro rcos_module_imp[OF is_group]) 
27611  251 
next 
252 
assume "x' \<otimes> inv x \<in> H" 

253 
from this and carr 

254 
show "x' \<in> H #> x" 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

255 
by (intro rcos_module_rev[OF is_group]) 
27611  256 
qed 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

257 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

258 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

259 
text {* Right cosets are subsets of the carrier. *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

260 
lemma (in subgroup) rcosets_carrier: 
27611  261 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

262 
assumes XH: "X \<in> rcosets H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

263 
shows "X \<subseteq> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

264 
proof  
29237  265 
interpret group G by fact 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

266 
from XH have "\<exists>x\<in> carrier G. X = H #> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

267 
unfolding RCOSETS_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

268 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

269 
from this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

270 
obtain x 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

271 
where xcarr: "x\<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

272 
and X: "X = H #> x" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

273 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

274 
from subset and xcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

275 
show "X \<subseteq> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

276 
unfolding X 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

277 
by (rule r_coset_subset_G) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

278 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

279 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

280 
text {* Multiplication of general subsets *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

281 
lemma (in monoid) set_mult_closed: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

282 
assumes Acarr: "A \<subseteq> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

283 
and Bcarr: "B \<subseteq> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

284 
shows "A <#> B \<subseteq> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

285 
apply rule apply (simp add: set_mult_def, clarsimp) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

286 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

287 
fix a b 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

288 
assume "a \<in> A" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

289 
from this and Acarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

290 
have acarr: "a \<in> carrier G" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

291 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

292 
assume "b \<in> B" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

293 
from this and Bcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

294 
have bcarr: "b \<in> carrier G" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

295 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

296 
from acarr bcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

297 
show "a \<otimes> b \<in> carrier G" by (rule m_closed) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

298 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

299 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

300 
lemma (in comm_group) mult_subgroups: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

301 
assumes subH: "subgroup H G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

302 
and subK: "subgroup K G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

303 
shows "subgroup (H <#> K) G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

304 
apply (rule subgroup.intro) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

305 
apply (intro set_mult_closed subgroup.subset[OF subH] subgroup.subset[OF subK]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

306 
apply (simp add: set_mult_def) apply clarsimp defer 1 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

307 
apply (simp add: set_mult_def) defer 1 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

308 
apply (simp add: set_mult_def, clarsimp) defer 1 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

309 
proof  
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

310 
fix ha hb ka kb 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

311 
assume haH: "ha \<in> H" and hbH: "hb \<in> H" and kaK: "ka \<in> K" and kbK: "kb \<in> K" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

312 
note carr = haH[THEN subgroup.mem_carrier[OF subH]] hbH[THEN subgroup.mem_carrier[OF subH]] 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

313 
kaK[THEN subgroup.mem_carrier[OF subK]] kbK[THEN subgroup.mem_carrier[OF subK]] 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

314 
from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

315 
have "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = ha \<otimes> (ka \<otimes> hb) \<otimes> kb" by (simp add: m_assoc) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

316 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

317 
have "\<dots> = ha \<otimes> (hb \<otimes> ka) \<otimes> kb" by (simp add: m_comm) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

318 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

319 
have "\<dots> = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" by (simp add: m_assoc) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

320 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

321 
have eq: "(ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = (ha \<otimes> hb) \<otimes> (ka \<otimes> kb)" . 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

322 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

323 
from haH hbH have hH: "ha \<otimes> hb \<in> H" by (simp add: subgroup.m_closed[OF subH]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

324 
from kaK kbK have kK: "ka \<otimes> kb \<in> K" by (simp add: subgroup.m_closed[OF subK]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

325 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

326 
from hH and kK and eq 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

327 
show "\<exists>h'\<in>H. \<exists>k'\<in>K. (ha \<otimes> ka) \<otimes> (hb \<otimes> kb) = h' \<otimes> k'" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

328 
next 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

329 
have "\<one> = \<one> \<otimes> \<one>" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

330 
from subgroup.one_closed[OF subH] subgroup.one_closed[OF subK] this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

331 
show "\<exists>h\<in>H. \<exists>k\<in>K. \<one> = h \<otimes> k" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

332 
next 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

333 
fix h k 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

334 
assume hH: "h \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

335 
and kK: "k \<in> K" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

336 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

337 
from hH[THEN subgroup.mem_carrier[OF subH]] kK[THEN subgroup.mem_carrier[OF subK]] 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

338 
have "inv (h \<otimes> k) = inv h \<otimes> inv k" by (simp add: inv_mult_group m_comm) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

339 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

340 
from subgroup.m_inv_closed[OF subH hH] and subgroup.m_inv_closed[OF subK kK] and this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

341 
show "\<exists>ha\<in>H. \<exists>ka\<in>K. inv (h \<otimes> k) = ha \<otimes> ka" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

342 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

343 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

344 
lemma (in subgroup) lcos_module_rev: 
27611  345 
assumes "group G" 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

346 
assumes carr: "x \<in> carrier G" "x' \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

347 
and xixH: "(inv x \<otimes> x') \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

348 
shows "x' \<in> x <# H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

349 
proof  
29237  350 
interpret group G by fact 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

351 
from xixH 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

352 
have "\<exists>h\<in>H. (inv x) \<otimes> x' = h" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

353 
from this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

354 
obtain h 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

355 
where hH: "h \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

356 
and hsym: "(inv x) \<otimes> x' = h" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

357 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

358 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

359 
from hH subset have hcarr: "h \<in> carrier G" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

360 
note carr = carr hcarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

361 
from hsym[symmetric] have "x \<otimes> h = x \<otimes> ((inv x) \<otimes> x')" by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

362 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

363 
have "\<dots> = (x \<otimes> (inv x)) \<otimes> x'" by (simp add: m_assoc[symmetric]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

364 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

365 
have "\<dots> = \<one> \<otimes> x'" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

366 
also from carr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

367 
have "\<dots> = x'" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

368 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

369 
have "x \<otimes> h = x'" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

370 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

371 
from this[symmetric] and hH 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

372 
show "x' \<in> x <# H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

373 
unfolding l_coset_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

374 
by fast 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

375 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

376 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

377 

14666  378 
subsection {* Normal subgroups *} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

379 

14963  380 
lemma normal_imp_subgroup: "H \<lhd> G \<Longrightarrow> subgroup H G" 
381 
by (simp add: normal_def subgroup_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

382 

14963  383 
lemma (in group) normalI: 
26310  384 
"subgroup H G \<Longrightarrow> (\<forall>x \<in> carrier G. H #> x = x <# H) \<Longrightarrow> H \<lhd> G" 
14963  385 
by (simp add: normal_def normal_axioms_def prems) 
386 

387 
lemma (in normal) inv_op_closed1: 

388 
"\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H" 

389 
apply (insert coset_eq) 

390 
apply (auto simp add: l_coset_def r_coset_def) 

14666  391 
apply (drule bspec, assumption) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

392 
apply (drule equalityD1 [THEN subsetD], blast, clarify) 
14963  393 
apply (simp add: m_assoc) 
394 
apply (simp add: m_assoc [symmetric]) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

395 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

396 

14963  397 
lemma (in normal) inv_op_closed2: 
398 
"\<lbrakk>x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H" 

399 
apply (subgoal_tac "inv (inv x) \<otimes> h \<otimes> (inv x) \<in> H") 

26310  400 
apply (simp add: ) 
14963  401 
apply (blast intro: inv_op_closed1) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

402 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

403 

14747  404 
text{*Alternative characterization of normal subgroups*} 
405 
lemma (in group) normal_inv_iff: 

406 
"(N \<lhd> G) = 

407 
(subgroup N G & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<otimes> h \<otimes> (inv x) \<in> N))" 

408 
(is "_ = ?rhs") 

409 
proof 

410 
assume N: "N \<lhd> G" 

411 
show ?rhs 

14963  412 
by (blast intro: N normal.inv_op_closed2 normal_imp_subgroup) 
14747  413 
next 
414 
assume ?rhs 

415 
hence sg: "subgroup N G" 

14963  416 
and closed: "\<And>x. x\<in>carrier G \<Longrightarrow> \<forall>h\<in>N. x \<otimes> h \<otimes> inv x \<in> N" by auto 
14747  417 
hence sb: "N \<subseteq> carrier G" by (simp add: subgroup.subset) 
418 
show "N \<lhd> G" 

14963  419 
proof (intro normalI [OF sg], simp add: l_coset_def r_coset_def, clarify) 
14747  420 
fix x 
421 
assume x: "x \<in> carrier G" 

15120  422 
show "(\<Union>h\<in>N. {h \<otimes> x}) = (\<Union>h\<in>N. {x \<otimes> h})" 
14747  423 
proof 
15120  424 
show "(\<Union>h\<in>N. {h \<otimes> x}) \<subseteq> (\<Union>h\<in>N. {x \<otimes> h})" 
14747  425 
proof clarify 
426 
fix n 

427 
assume n: "n \<in> N" 

15120  428 
show "n \<otimes> x \<in> (\<Union>h\<in>N. {x \<otimes> h})" 
14747  429 
proof 
14963  430 
from closed [of "inv x"] 
431 
show "inv x \<otimes> n \<otimes> x \<in> N" by (simp add: x n) 

432 
show "n \<otimes> x \<in> {x \<otimes> (inv x \<otimes> n \<otimes> x)}" 

14747  433 
by (simp add: x n m_assoc [symmetric] sb [THEN subsetD]) 
434 
qed 

435 
qed 

436 
next 

15120  437 
show "(\<Union>h\<in>N. {x \<otimes> h}) \<subseteq> (\<Union>h\<in>N. {h \<otimes> x})" 
14747  438 
proof clarify 
439 
fix n 

440 
assume n: "n \<in> N" 

15120  441 
show "x \<otimes> n \<in> (\<Union>h\<in>N. {h \<otimes> x})" 
14747  442 
proof 
14963  443 
show "x \<otimes> n \<otimes> inv x \<in> N" by (simp add: x n closed) 
444 
show "x \<otimes> n \<in> {x \<otimes> n \<otimes> inv x \<otimes> x}" 

14747  445 
by (simp add: x n m_assoc sb [THEN subsetD]) 
446 
qed 

447 
qed 

448 
qed 

449 
qed 

450 
qed 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

451 

14963  452 

14803  453 
subsection{*More Properties of Cosets*} 
454 

14747  455 
lemma (in group) lcos_m_assoc: 
456 
"[ M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G ] 

457 
==> g <# (h <# M) = (g \<otimes> h) <# M" 

458 
by (force simp add: l_coset_def m_assoc) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

459 

14747  460 
lemma (in group) lcos_mult_one: "M \<subseteq> carrier G ==> \<one> <# M = M" 
461 
by (force simp add: l_coset_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

462 

14747  463 
lemma (in group) l_coset_subset_G: 
464 
"[ H \<subseteq> carrier G; x \<in> carrier G ] ==> x <# H \<subseteq> carrier G" 

465 
by (auto simp add: l_coset_def subsetD) 

466 

467 
lemma (in group) l_coset_swap: 

14963  468 
"\<lbrakk>y \<in> x <# H; x \<in> carrier G; subgroup H G\<rbrakk> \<Longrightarrow> x \<in> y <# H" 
469 
proof (simp add: l_coset_def) 

470 
assume "\<exists>h\<in>H. y = x \<otimes> h" 

14666  471 
and x: "x \<in> carrier G" 
14530  472 
and sb: "subgroup H G" 
473 
then obtain h' where h': "h' \<in> H & x \<otimes> h' = y" by blast 

14963  474 
show "\<exists>h\<in>H. x = y \<otimes> h" 
14530  475 
proof 
14963  476 
show "x = y \<otimes> inv h'" using h' x sb 
14530  477 
by (auto simp add: m_assoc subgroup.subset [THEN subsetD]) 
478 
show "inv h' \<in> H" using h' sb 

479 
by (auto simp add: subgroup.subset [THEN subsetD] subgroup.m_inv_closed) 

480 
qed 

481 
qed 

482 

14747  483 
lemma (in group) l_coset_carrier: 
14530  484 
"[ y \<in> x <# H; x \<in> carrier G; subgroup H G ] ==> y \<in> carrier G" 
14747  485 
by (auto simp add: l_coset_def m_assoc 
14530  486 
subgroup.subset [THEN subsetD] subgroup.m_closed) 
487 

14747  488 
lemma (in group) l_repr_imp_subset: 
14666  489 
assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G" 
14530  490 
shows "y <# H \<subseteq> x <# H" 
491 
proof  

492 
from y 

14747  493 
obtain h' where "h' \<in> H" "x \<otimes> h' = y" by (auto simp add: l_coset_def) 
14530  494 
thus ?thesis using x sb 
14747  495 
by (auto simp add: l_coset_def m_assoc 
14530  496 
subgroup.subset [THEN subsetD] subgroup.m_closed) 
497 
qed 

498 

14747  499 
lemma (in group) l_repr_independence: 
14666  500 
assumes y: "y \<in> x <# H" and x: "x \<in> carrier G" and sb: "subgroup H G" 
14530  501 
shows "x <# H = y <# H" 
14666  502 
proof 
14530  503 
show "x <# H \<subseteq> y <# H" 
14666  504 
by (rule l_repr_imp_subset, 
14530  505 
(blast intro: l_coset_swap l_coset_carrier y x sb)+) 
14666  506 
show "y <# H \<subseteq> x <# H" by (rule l_repr_imp_subset [OF y x sb]) 
14530  507 
qed 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

508 

14747  509 
lemma (in group) setmult_subset_G: 
14963  510 
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G\<rbrakk> \<Longrightarrow> H <#> K \<subseteq> carrier G" 
511 
by (auto simp add: set_mult_def subsetD) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

512 

14963  513 
lemma (in group) subgroup_mult_id: "subgroup H G \<Longrightarrow> H <#> H = H" 
514 
apply (auto simp add: subgroup.m_closed set_mult_def Sigma_def image_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

515 
apply (rule_tac x = x in bexI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

516 
apply (rule bexI [of _ "\<one>"]) 
14666  517 
apply (auto simp add: subgroup.m_closed subgroup.one_closed 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

518 
r_one subgroup.subset [THEN subsetD]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

519 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

520 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

521 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

522 
subsubsection {* Set of Inverses of an @{text r_coset}. *} 
14666  523 

14963  524 
lemma (in normal) rcos_inv: 
525 
assumes x: "x \<in> carrier G" 

526 
shows "set_inv (H #> x) = H #> (inv x)" 

527 
proof (simp add: r_coset_def SET_INV_def x inv_mult_group, safe) 

528 
fix h 

529 
assume "h \<in> H" 

15120  530 
show "inv x \<otimes> inv h \<in> (\<Union>j\<in>H. {j \<otimes> inv x})" 
14963  531 
proof 
532 
show "inv x \<otimes> inv h \<otimes> x \<in> H" 

533 
by (simp add: inv_op_closed1 prems) 

534 
show "inv x \<otimes> inv h \<in> {inv x \<otimes> inv h \<otimes> x \<otimes> inv x}" 

535 
by (simp add: prems m_assoc) 

536 
qed 

537 
next 

538 
fix h 

539 
assume "h \<in> H" 

15120  540 
show "h \<otimes> inv x \<in> (\<Union>j\<in>H. {inv x \<otimes> inv j})" 
14963  541 
proof 
542 
show "x \<otimes> inv h \<otimes> inv x \<in> H" 

543 
by (simp add: inv_op_closed2 prems) 

544 
show "h \<otimes> inv x \<in> {inv x \<otimes> inv (x \<otimes> inv h \<otimes> inv x)}" 

545 
by (simp add: prems m_assoc [symmetric] inv_mult_group) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

546 
qed 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

547 
qed 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

548 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

549 

14803  550 
subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*} 
14666  551 

14747  552 
lemma (in group) setmult_rcos_assoc: 
14963  553 
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> 
554 
\<Longrightarrow> H <#> (K #> x) = (H <#> K) #> x" 

555 
by (force simp add: r_coset_def set_mult_def m_assoc) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

556 

14747  557 
lemma (in group) rcos_assoc_lcos: 
14963  558 
"\<lbrakk>H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G\<rbrakk> 
559 
\<Longrightarrow> (H #> x) <#> K = H <#> (x <# K)" 

560 
by (force simp add: r_coset_def l_coset_def set_mult_def m_assoc) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

561 

14963  562 
lemma (in normal) rcos_mult_step1: 
563 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> 

564 
\<Longrightarrow> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y" 

565 
by (simp add: setmult_rcos_assoc subset 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

566 
r_coset_subset_G l_coset_subset_G rcos_assoc_lcos) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

567 

14963  568 
lemma (in normal) rcos_mult_step2: 
569 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> 

570 
\<Longrightarrow> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y" 

571 
by (insert coset_eq, simp add: normal_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

572 

14963  573 
lemma (in normal) rcos_mult_step3: 
574 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> 

575 
\<Longrightarrow> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)" 

576 
by (simp add: setmult_rcos_assoc coset_mult_assoc 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19380
diff
changeset

577 
subgroup_mult_id normal.axioms subset prems) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

578 

14963  579 
lemma (in normal) rcos_sum: 
580 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> 

581 
\<Longrightarrow> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

582 
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

583 

14963  584 
lemma (in normal) rcosets_mult_eq: "M \<in> rcosets H \<Longrightarrow> H <#> M = M" 
14666  585 
 {* generalizes @{text subgroup_mult_id} *} 
14963  586 
by (auto simp add: RCOSETS_def subset 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19380
diff
changeset

587 
setmult_rcos_assoc subgroup_mult_id normal.axioms prems) 
14963  588 

589 

590 
subsubsection{*An Equivalence Relation*} 

591 

592 
constdefs (structure G) 

593 
r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set" 

594 
("rcong\<index> _") 

595 
"rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}" 

596 

597 

598 
lemma (in subgroup) equiv_rcong: 

27611  599 
assumes "group G" 
14963  600 
shows "equiv (carrier G) (rcong H)" 
27611  601 
proof  
29237  602 
interpret group G by fact 
27611  603 
show ?thesis 
604 
proof (intro equiv.intro) 

30198  605 
show "refl_on (carrier G) (rcong H)" 
606 
by (auto simp add: r_congruent_def refl_on_def) 

27611  607 
next 
608 
show "sym (rcong H)" 

609 
proof (simp add: r_congruent_def sym_def, clarify) 

610 
fix x y 

611 
assume [simp]: "x \<in> carrier G" "y \<in> carrier G" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31727
diff
changeset

612 
and "inv x \<otimes> y \<in> H" 
27611  613 
hence "inv (inv x \<otimes> y) \<in> H" by (simp add: m_inv_closed) 
614 
thus "inv y \<otimes> x \<in> H" by (simp add: inv_mult_group) 

615 
qed 

616 
next 

617 
show "trans (rcong H)" 

618 
proof (simp add: r_congruent_def trans_def, clarify) 

619 
fix x y z 

620 
assume [simp]: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31727
diff
changeset

621 
and "inv x \<otimes> y \<in> H" and "inv y \<otimes> z \<in> H" 
27611  622 
hence "(inv x \<otimes> y) \<otimes> (inv y \<otimes> z) \<in> H" by simp 
27698  623 
hence "inv x \<otimes> (y \<otimes> inv y) \<otimes> z \<in> H" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31727
diff
changeset

624 
by (simp add: m_assoc del: r_inv Units_r_inv) 
27611  625 
thus "inv x \<otimes> z \<in> H" by simp 
626 
qed 

14963  627 
qed 
628 
qed 

629 

630 
text{*Equivalence classes of @{text rcong} correspond to left cosets. 

631 
Was there a mistake in the definitions? I'd have expected them to 

632 
correspond to right cosets.*} 

633 

634 
(* CB: This is correct, but subtle. 

635 
We call H #> a the right coset of a relative to H. According to 

636 
Jacobson, this is what the majority of group theory literature does. 

637 
He then defines the notion of congruence relation ~ over monoids as 

638 
equivalence relation with a ~ a' & b ~ b' \<Longrightarrow> a*b ~ a'*b'. 

639 
Our notion of right congruence induced by K: rcong K appears only in 

640 
the context where K is a normal subgroup. Jacobson doesn't name it. 

641 
But in this context left and right cosets are identical. 

642 
*) 

643 

644 
lemma (in subgroup) l_coset_eq_rcong: 

27611  645 
assumes "group G" 
14963  646 
assumes a: "a \<in> carrier G" 
647 
shows "a <# H = rcong H `` {a}" 

27611  648 
proof  
29237  649 
interpret group G by fact 
27611  650 
show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
651 
qed 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

652 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

653 
subsubsection{*Two Distinct Right Cosets are Disjoint*} 
14803  654 

655 
lemma (in group) rcos_equation: 

27611  656 
assumes "subgroup H G" 
657 
assumes p: "ha \<otimes> a = h \<otimes> b" "a \<in> carrier G" "b \<in> carrier G" "h \<in> H" "ha \<in> H" "hb \<in> H" 

658 
shows "hb \<otimes> a \<in> (\<Union>h\<in>H. {h \<otimes> b})" 

659 
proof  

29237  660 
interpret subgroup H G by fact 
27611  661 
from p show ?thesis apply (rule_tac UN_I [of "hb \<otimes> ((inv ha) \<otimes> h)"]) 
662 
apply (simp add: ) 

663 
apply (simp add: m_assoc transpose_inv) 

664 
done 

665 
qed 

14803  666 

667 
lemma (in group) rcos_disjoint: 

27611  668 
assumes "subgroup H G" 
669 
assumes p: "a \<in> rcosets H" "b \<in> rcosets H" "a\<noteq>b" 

670 
shows "a \<inter> b = {}" 

671 
proof  

29237  672 
interpret subgroup H G by fact 
27611  673 
from p show ?thesis apply (simp add: RCOSETS_def r_coset_def) 
674 
apply (blast intro: rcos_equation prems sym) 

675 
done 

676 
qed 

14803  677 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

678 
subsection {* Further lemmas for @{text "r_congruent"} *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

679 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

680 
text {* The relation is a congruence *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

681 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

682 
lemma (in normal) congruent_rcong: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

683 
shows "congruent2 (rcong H) (rcong H) (\<lambda>a b. a \<otimes> b <# H)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

684 
proof (intro congruent2I[of "carrier G" _ "carrier G" _] equiv_rcong is_group) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

685 
fix a b c 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

686 
assume abrcong: "(a, b) \<in> rcong H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

687 
and ccarr: "c \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

688 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

689 
from abrcong 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

690 
have acarr: "a \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

691 
and bcarr: "b \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

692 
and abH: "inv a \<otimes> b \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

693 
unfolding r_congruent_def 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

694 
by fast+ 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

695 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

696 
note carr = acarr bcarr ccarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

697 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

698 
from ccarr and abH 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

699 
have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c \<in> H" by (rule inv_op_closed1) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

700 
moreover 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

701 
from carr and inv_closed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

702 
have "inv c \<otimes> (inv a \<otimes> b) \<otimes> c = (inv c \<otimes> inv a) \<otimes> (b \<otimes> c)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

703 
by (force cong: m_assoc) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

704 
moreover 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

705 
from carr and inv_closed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

706 
have "\<dots> = (inv (a \<otimes> c)) \<otimes> (b \<otimes> c)" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

707 
by (simp add: inv_mult_group) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

708 
ultimately 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

709 
have "(inv (a \<otimes> c)) \<otimes> (b \<otimes> c) \<in> H" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

710 
from carr and this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

711 
have "(b \<otimes> c) \<in> (a \<otimes> c) <# H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

712 
by (simp add: lcos_module_rev[OF is_group]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

713 
from carr and this and is_subgroup 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

714 
show "(a \<otimes> c) <# H = (b \<otimes> c) <# H" by (intro l_repr_independence, simp+) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

715 
next 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

716 
fix a b c 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

717 
assume abrcong: "(a, b) \<in> rcong H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

718 
and ccarr: "c \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

719 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

720 
from ccarr have "c \<in> Units G" by (simp add: Units_eq) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

721 
hence cinvc_one: "inv c \<otimes> c = \<one>" by (rule Units_l_inv) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

722 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

723 
from abrcong 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

724 
have acarr: "a \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

725 
and bcarr: "b \<in> carrier G" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

726 
and abH: "inv a \<otimes> b \<in> H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

727 
by (unfold r_congruent_def, fast+) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

728 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

729 
note carr = acarr bcarr ccarr 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

730 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

731 
from carr and inv_closed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

732 
have "inv a \<otimes> b = inv a \<otimes> (\<one> \<otimes> b)" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

733 
also from carr and inv_closed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

734 
have "\<dots> = inv a \<otimes> (inv c \<otimes> c) \<otimes> b" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

735 
also from carr and inv_closed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

736 
have "\<dots> = (inv a \<otimes> inv c) \<otimes> (c \<otimes> b)" by (force cong: m_assoc) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

737 
also from carr and inv_closed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

738 
have "\<dots> = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" by (simp add: inv_mult_group) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

739 
finally 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

740 
have "inv a \<otimes> b = inv (c \<otimes> a) \<otimes> (c \<otimes> b)" . 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

741 
from abH and this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

742 
have "inv (c \<otimes> a) \<otimes> (c \<otimes> b) \<in> H" by simp 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

743 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

744 
from carr and this 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

745 
have "(c \<otimes> b) \<in> (c \<otimes> a) <# H" 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

746 
by (simp add: lcos_module_rev[OF is_group]) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

747 
from carr and this and is_subgroup 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

748 
show "(c \<otimes> a) <# H = (c \<otimes> b) <# H" by (intro l_repr_independence, simp+) 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

749 
qed 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19931
diff
changeset

750 

14803  751 

752 
subsection {*Order of a Group and Lagrange's Theorem*} 

753 

754 
constdefs 

14963  755 
order :: "('a, 'b) monoid_scheme \<Rightarrow> nat" 
756 
"order S \<equiv> card (carrier S)" 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

757 

14963  758 
lemma (in group) rcosets_part_G: 
27611  759 
assumes "subgroup H G" 
14963  760 
shows "\<Union>(rcosets H) = carrier G" 
27611  761 
proof  
29237  762 
interpret subgroup H G by fact 
27611  763 
show ?thesis 
764 
apply (rule equalityI) 

765 
apply (force simp add: RCOSETS_def r_coset_def) 

766 
apply (auto simp add: RCOSETS_def intro: rcos_self prems) 

767 
done 

768 
qed 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

769 

14747  770 
lemma (in group) cosets_finite: 
14963  771 
"\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier G; finite (carrier G)\<rbrakk> \<Longrightarrow> finite c" 
772 
apply (auto simp add: RCOSETS_def) 

773 
apply (simp add: r_coset_subset_G [THEN finite_subset]) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

774 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

775 

14747  776 
text{*The next two lemmas support the proof of @{text card_cosets_equal}.*} 
777 
lemma (in group) inj_on_f: 

14963  778 
"\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

779 
apply (rule inj_onI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

780 
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

781 
prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

782 
apply (simp add: subsetD) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

783 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

784 

14747  785 
lemma (in group) inj_on_g: 
14963  786 
"\<lbrakk>H \<subseteq> carrier G; a \<in> carrier G\<rbrakk> \<Longrightarrow> inj_on (\<lambda>y. y \<otimes> a) H" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

787 
by (force simp add: inj_on_def subsetD) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

788 

14747  789 
lemma (in group) card_cosets_equal: 
14963  790 
"\<lbrakk>c \<in> rcosets H; H \<subseteq> carrier G; finite(carrier G)\<rbrakk> 
791 
\<Longrightarrow> card c = card H" 

792 
apply (auto simp add: RCOSETS_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

793 
apply (rule card_bij_eq) 
14666  794 
apply (rule inj_on_f, assumption+) 
14747  795 
apply (force simp add: m_assoc subsetD r_coset_def) 
14666  796 
apply (rule inj_on_g, assumption+) 
14747  797 
apply (force simp add: m_assoc subsetD r_coset_def) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

798 
txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

799 
apply (simp add: r_coset_subset_G [THEN finite_subset]) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

800 
apply (blast intro: finite_subset) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

801 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

802 

14963  803 
lemma (in group) rcosets_subset_PowG: 
804 
"subgroup H G \<Longrightarrow> rcosets H \<subseteq> Pow(carrier G)" 

805 
apply (simp add: RCOSETS_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

806 
apply (blast dest: r_coset_subset_G subgroup.subset) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

807 
done 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

808 

14803  809 

810 
theorem (in group) lagrange: 

14963  811 
"\<lbrakk>finite(carrier G); subgroup H G\<rbrakk> 
812 
\<Longrightarrow> card(rcosets H) * card(H) = order(G)" 

813 
apply (simp (no_asm_simp) add: order_def rcosets_part_G [symmetric]) 

14803  814 
apply (subst mult_commute) 
815 
apply (rule card_partition) 

14963  816 
apply (simp add: rcosets_subset_PowG [THEN finite_subset]) 
817 
apply (simp add: rcosets_part_G) 

14803  818 
apply (simp add: card_cosets_equal subgroup.subset) 
819 
apply (simp add: rcos_disjoint) 

820 
done 

821 

822 

14747  823 
subsection {*Quotient Groups: Factorization of a Group*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

824 

cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

825 
constdefs 
14963  826 
FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" 
14803  827 
(infixl "Mod" 65) 
14747  828 
{*Actually defined for groups rather than monoids*} 
14963  829 
"FactGroup G H \<equiv> 
830 
\<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>" 

14747  831 

14963  832 
lemma (in normal) setmult_closed: 
833 
"\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H" 

834 
by (auto simp add: rcos_sum RCOSETS_def) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

835 

14963  836 
lemma (in normal) setinv_closed: 
837 
"K \<in> rcosets H \<Longrightarrow> set_inv K \<in> rcosets H" 

838 
by (auto simp add: rcos_inv RCOSETS_def) 

13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

839 

14963  840 
lemma (in normal) rcosets_assoc: 
841 
"\<lbrakk>M1 \<in> rcosets H; M2 \<in> rcosets H; M3 \<in> rcosets H\<rbrakk> 

842 
\<Longrightarrow> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)" 

843 
by (auto simp add: RCOSETS_def rcos_sum m_assoc) 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

844 

14963  845 
lemma (in subgroup) subgroup_in_rcosets: 
27611  846 
assumes "group G" 
14963  847 
shows "H \<in> rcosets H" 
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

848 
proof  
29237  849 
interpret group G by fact 
26203  850 
from _ subgroup_axioms have "H #> \<one> = H" 
23350  851 
by (rule coset_join2) auto 
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

852 
then show ?thesis 
14963  853 
by (auto simp add: RCOSETS_def) 
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

854 
qed 
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

855 

14963  856 
lemma (in normal) rcosets_inv_mult_group_eq: 
857 
"M \<in> rcosets H \<Longrightarrow> set_inv M <#> M = H" 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19380
diff
changeset

858 
by (auto simp add: RCOSETS_def rcos_inv rcos_sum subgroup.subset normal.axioms prems) 
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

859 

14963  860 
theorem (in normal) factorgroup_is_group: 
861 
"group (G Mod H)" 

14666  862 
apply (simp add: FactGroup_def) 
13936  863 
apply (rule groupI) 
14747  864 
apply (simp add: setmult_closed) 
14963  865 
apply (simp add: normal_imp_subgroup subgroup_in_rcosets [OF is_group]) 
866 
apply (simp add: restrictI setmult_closed rcosets_assoc) 

13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

867 
apply (simp add: normal_imp_subgroup 
14963  868 
subgroup_in_rcosets rcosets_mult_eq) 
869 
apply (auto dest: rcosets_inv_mult_group_eq simp add: setinv_closed) 

13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

870 
done 
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset

871 

14803  872 
lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'" 
873 
by (simp add: FactGroup_def) 

874 

14963  875 
lemma (in normal) inv_FactGroup: 
876 
"X \<in> carrier (G Mod H) \<Longrightarrow> inv\<^bsub>G Mod H\<^esub> X = set_inv X" 

14747  877 
apply (rule group.inv_equality [OF factorgroup_is_group]) 
14963  878 
apply (simp_all add: FactGroup_def setinv_closed rcosets_inv_mult_group_eq) 
14747  879 
done 
880 

881 
text{*The coset map is a homomorphism from @{term G} to the quotient group 

14963  882 
@{term "G Mod H"}*} 
883 
lemma (in normal) r_coset_hom_Mod: 

884 
"(\<lambda>a. H #> a) \<in> hom G (G Mod H)" 

885 
by (auto simp add: FactGroup_def RCOSETS_def Pi_def hom_def rcos_sum) 

14747  886 

14963  887 

888 
subsection{*The First Isomorphism Theorem*} 

14803  889 

14963  890 
text{*The quotient by the kernel of a homomorphism is isomorphic to the 
891 
range of that homomorphism.*} 

14803  892 

893 
constdefs 

14963  894 
kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
895 
('a \<Rightarrow> 'b) \<Rightarrow> 'a set" 

14803  896 
{*the kernel of a homomorphism*} 
26310  897 
"kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}" 
14803  898 

899 
lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G" 

14963  900 
apply (rule subgroup.intro) 
14803  901 
apply (auto simp add: kernel_def group.intro prems) 
902 
done 

903 

904 
text{*The kernel of a homomorphism is a normal subgroup*} 

14963  905 
lemma (in group_hom) normal_kernel: "(kernel G H h) \<lhd> G" 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19380
diff
changeset

906 
apply (simp add: G.normal_inv_iff subgroup_kernel) 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19380
diff
changeset

907 
apply (simp add: kernel_def) 
14803  908 
done 
909 

910 
lemma (in group_hom) FactGroup_nonempty: 

911 
assumes X: "X \<in> carrier (G Mod kernel G H h)" 

912 
shows "X \<noteq> {}" 

913 
proof  

914 
from X 

915 
obtain g where "g \<in> carrier G" 

916 
and "X = kernel G H h #> g" 

14963  917 
by (auto simp add: FactGroup_def RCOSETS_def) 
14803  918 
thus ?thesis 
14963  919 
by (auto simp add: kernel_def r_coset_def image_def intro: hom_one) 
14803  920 
qed 
921 

922 

923 
lemma (in group_hom) FactGroup_contents_mem: 

924 
assumes X: "X \<in> carrier (G Mod (kernel G H h))" 

925 
shows "contents (h`X) \<in> carrier H" 

926 
proof  

927 
from X 

928 
obtain g where g: "g \<in> carrier G" 

929 
and "X = kernel G H h #> g" 

14963  930 
by (auto simp add: FactGroup_def RCOSETS_def) 
931 
hence "h ` X = {h g}" by (auto simp add: kernel_def r_coset_def image_def g) 

14803  932 
thus ?thesis by (auto simp add: g) 
933 
qed 

934 

935 
lemma (in group_hom) FactGroup_hom: 

14963  936 
"(\<lambda>X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H" 
31727  937 
apply (simp add: hom_def FactGroup_contents_mem normal.factorgroup_is_group [OF normal_kernel] group.axioms monoid.m_closed) 
938 
proof (intro ballI) 

14803  939 
fix X and X' 
940 
assume X: "X \<in> carrier (G Mod kernel G H h)" 

941 
and X': "X' \<in> carrier (G Mod kernel G H h)" 

942 
then 

943 
obtain g and g' 

944 
where "g \<in> carrier G" and "g' \<in> carrier G" 

945 
and "X = kernel G H h #> g" and "X' = kernel G H h #> g'" 

14963  946 
by (auto simp add: FactGroup_def RCOSETS_def) 
14803  947 
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
948 
and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G" 

949 
by (force simp add: kernel_def r_coset_def image_def)+ 

950 
hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X' 

951 
by (auto dest!: FactGroup_nonempty 

952 
simp add: set_mult_def image_eq_UN 

953 
subsetD [OF Xsub] subsetD [OF X'sub]) 

954 
thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')" 

31727  955 
by (simp add: all image_eq_UN FactGroup_nonempty X X') 
14803  956 
qed 
957 

14963  958 

14803  959 
text{*Lemma for the following injectivity result*} 
960 
lemma (in group_hom) FactGroup_subset: 

14963  961 
"\<lbrakk>g \<in> carrier G; g' \<in> carrier G; h g = h g'\<rbrakk> 
962 
\<Longrightarrow> kernel G H h #> g \<subseteq> kernel G H h #> g'" 

26310  963 
apply (clarsimp simp add: kernel_def r_coset_def image_def) 
14803  964 
apply (rename_tac y) 
965 
apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI) 

26310  966 
apply (simp add: G.m_assoc) 
14803  967 
done 
968 

969 
lemma (in group_hom) FactGroup_inj_on: 

970 
"inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))" 

971 
proof (simp add: inj_on_def, clarify) 

972 
fix X and X' 

973 
assume X: "X \<in> carrier (G Mod kernel G H h)" 

974 
and X': "X' \<in> carrier (G Mod kernel G H h)" 

975 
then 

976 
obtain g and g' 

977 
where gX: "g \<in> carrier G" "g' \<in> carrier G" 

978 
"X = kernel G H h #> g" "X' = kernel G H h #> g'" 

14963  979 
by (auto simp add: FactGroup_def RCOSETS_def) 
14803  980 
hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'" 
981 
by (force simp add: kernel_def r_coset_def image_def)+ 

982 
assume "contents (h ` X) = contents (h ` X')" 

983 
hence h: "h g = h g'" 

984 
by (simp add: image_eq_UN all FactGroup_nonempty X X') 

985 
show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX) 

986 
qed 

987 

988 
text{*If the homomorphism @{term h} is onto @{term H}, then so is the 

989 
homomorphism from the quotient group*} 

990 
lemma (in group_hom) FactGroup_onto: 

991 
assumes h: "h ` carrier G = carrier H" 

992 
shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H" 

993 
proof 

994 
show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H" 

995 
by (auto simp add: FactGroup_contents_mem) 

996 
show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 

997 
proof 

998 
fix y 

999 
assume y: "y \<in> carrier H" 

1000 
with h obtain g where g: "g \<in> carrier G" "h g = y" 

26310  1001 
by (blast elim: equalityE) 
15120  1002 
hence "(\<Union>x\<in>kernel G H h #> g. {h x}) = {y}" 
14803  1003 
by (auto simp add: y kernel_def r_coset_def) 
1004 
with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)" 

14963  1005 
by (auto intro!: bexI simp add: FactGroup_def RCOSETS_def image_eq_UN) 
14803  1006 
qed 
1007 
qed 

1008 

1009 

1010 
text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the 

1011 
quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*} 

1012 
theorem (in group_hom) FactGroup_iso: 

1013 
"h ` carrier G = carrier H 

14963  1014 
\<Longrightarrow> (\<lambda>X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H" 
14803  1015 
by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def 
1016 
FactGroup_onto) 

1017 

14963  1018 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

1019 
end 