|
1 (* Title: HOL/Algebra/Product_Groups.thy |
|
2 Author: LC Paulson (ported from HOL Light) |
|
3 *) |
|
4 |
|
5 section \<open>Product and Sum Groups\<close> |
|
6 |
|
7 theory Product_Groups |
|
8 imports Elementary_Groups "HOL-Library.Equipollence" |
|
9 |
|
10 begin |
|
11 |
|
12 subsection \<open>Product of a Family of Groups\<close> |
|
13 |
|
14 definition product_group:: "'a set \<Rightarrow> ('a \<Rightarrow> ('b, 'c) monoid_scheme) \<Rightarrow> ('a \<Rightarrow> 'b) monoid" |
|
15 where "product_group I G \<equiv> \<lparr>carrier = (\<Pi>\<^sub>E i\<in>I. carrier (G i)), |
|
16 monoid.mult = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)), |
|
17 one = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)\<rparr>" |
|
18 |
|
19 lemma carrier_product_group [simp]: "carrier(product_group I G) = (\<Pi>\<^sub>E i\<in>I. carrier (G i))" |
|
20 by (simp add: product_group_def) |
|
21 |
|
22 lemma one_product_group [simp]: "one(product_group I G) = (\<lambda>i\<in>I. one (G i))" |
|
23 by (simp add: product_group_def) |
|
24 |
|
25 lemma mult_product_group [simp]: "(\<otimes>\<^bsub>product_group I G\<^esub>) = (\<lambda>x y. \<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i)" |
|
26 by (simp add: product_group_def) |
|
27 |
|
28 lemma product_group [simp]: |
|
29 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" shows "group (product_group I G)" |
|
30 proof (rule groupI; simp) |
|
31 show "(\<lambda>i. x i \<otimes>\<^bsub>G i\<^esub> y i) \<in> (\<Pi> i\<in>I. carrier (G i))" |
|
32 if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "y \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x y |
|
33 using that assms group.subgroup_self subgroup.m_closed by fastforce |
|
34 show "(\<lambda>i. \<one>\<^bsub>G i\<^esub>) \<in> (\<Pi> i\<in>I. carrier (G i))" |
|
35 by (simp add: assms group.is_monoid) |
|
36 show "(\<lambda>i\<in>I. (if i \<in> I then x i \<otimes>\<^bsub>G i\<^esub> y i else undefined) \<otimes>\<^bsub>G i\<^esub> z i) = |
|
37 (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> (if i \<in> I then y i \<otimes>\<^bsub>G i\<^esub> z i else undefined))" |
|
38 if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "y \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "z \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x y z |
|
39 using that by (auto simp: PiE_iff assms group.is_monoid monoid.m_assoc intro: restrict_ext) |
|
40 show "(\<lambda>i\<in>I. (if i \<in> I then \<one>\<^bsub>G i\<^esub> else undefined) \<otimes>\<^bsub>G i\<^esub> x i) = x" |
|
41 if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x |
|
42 using assms that by (fastforce simp: Group.group_def PiE_iff) |
|
43 show "\<exists>y\<in>\<Pi>\<^sub>E i\<in>I. carrier (G i). (\<lambda>i\<in>I. y i \<otimes>\<^bsub>G i\<^esub> x i) = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)" |
|
44 if "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" for x |
|
45 by (rule_tac x="\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i" in bexI) (use assms that in \<open>auto simp: PiE_iff group.l_inv\<close>) |
|
46 qed |
|
47 |
|
48 lemma inv_product_group [simp]: |
|
49 assumes "f \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" "\<And>i. i \<in> I \<Longrightarrow> group (G i)" |
|
50 shows "inv\<^bsub>product_group I G\<^esub> f = (\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i)" |
|
51 proof (rule group.inv_equality) |
|
52 show "Group.group (product_group I G)" |
|
53 by (simp add: assms) |
|
54 show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i) \<otimes>\<^bsub>product_group I G\<^esub> f = \<one>\<^bsub>product_group I G\<^esub>" |
|
55 using assms by (auto simp: PiE_iff group.l_inv) |
|
56 show "f \<in> carrier (product_group I G)" |
|
57 using assms by simp |
|
58 show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> f i) \<in> carrier (product_group I G)" |
|
59 using PiE_mem assms by fastforce |
|
60 qed |
|
61 |
|
62 |
|
63 lemma trivial_product_group: "trivial_group(product_group I G) \<longleftrightarrow> (\<forall>i \<in> I. trivial_group(G i))" |
|
64 (is "?lhs = ?rhs") |
|
65 proof |
|
66 assume L: ?lhs |
|
67 then have "inv\<^bsub>product_group I G\<^esub> (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) = \<one>\<^bsub>product_group I G\<^esub>" |
|
68 by (metis group.is_monoid monoid.inv_one one_product_group trivial_group_def) |
|
69 have [simp]: "\<one>\<^bsub>G i\<^esub> \<otimes>\<^bsub>G i\<^esub> \<one>\<^bsub>G i\<^esub> = \<one>\<^bsub>G i\<^esub>" if "i \<in> I" for i |
|
70 unfolding trivial_group_def |
|
71 proof - |
|
72 have 1: "(\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) i = \<one>\<^bsub>G i\<^esub>" |
|
73 by (simp add: that) |
|
74 have "(\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) = (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>) \<otimes>\<^bsub>product_group I G\<^esub> (\<lambda>a\<in>I. \<one>\<^bsub>G a\<^esub>)" |
|
75 by (metis (no_types) L group.is_monoid monoid.l_one one_product_group singletonI trivial_group_def) |
|
76 then show ?thesis |
|
77 using 1 by (simp add: that) |
|
78 qed |
|
79 show ?rhs |
|
80 using L |
|
81 by (auto simp: trivial_group_def product_group_def PiE_eq_singleton intro: groupI) |
|
82 next |
|
83 assume ?rhs |
|
84 then show ?lhs |
|
85 by (simp add: PiE_eq_singleton trivial_group_def) |
|
86 qed |
|
87 |
|
88 |
|
89 lemma PiE_subgroup_product_group: |
|
90 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" |
|
91 shows "subgroup (PiE I H) (product_group I G) \<longleftrightarrow> (\<forall>i \<in> I. subgroup (H i) (G i))" |
|
92 (is "?lhs = ?rhs") |
|
93 proof |
|
94 assume L: ?lhs |
|
95 then have [simp]: "PiE I H \<noteq> {}" |
|
96 using subgroup_nonempty by force |
|
97 show ?rhs |
|
98 proof (clarify; unfold_locales) |
|
99 show sub: "H i \<subseteq> carrier (G i)" if "i \<in> I" for i |
|
100 using that L by (simp add: subgroup_def) (metis (no_types, lifting) L subgroup_nonempty subset_PiE) |
|
101 show "x \<otimes>\<^bsub>G i\<^esub> y \<in> H i" if "i \<in> I" "x \<in> H i" "y \<in> H i" for i x y |
|
102 proof - |
|
103 have *: "\<And>x. x \<in> Pi\<^sub>E I H \<Longrightarrow> (\<forall>y \<in> Pi\<^sub>E I H. \<forall>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i \<in> H i)" |
|
104 using L by (auto simp: subgroup_def Pi_iff) |
|
105 have "\<forall>y\<in>H i. f i \<otimes>\<^bsub>G i\<^esub> y \<in> H i" if f: "f \<in> Pi\<^sub>E I H" and "i \<in> I" for i f |
|
106 using * [OF f] \<open>i \<in> I\<close> |
|
107 by (subst(asm) all_PiE_elements) auto |
|
108 then have "\<forall>f \<in> Pi\<^sub>E I H. \<forall>i \<in> I. \<forall>y\<in>H i. f i \<otimes>\<^bsub>G i\<^esub> y \<in> H i" |
|
109 by blast |
|
110 with that show ?thesis |
|
111 by (subst(asm) all_PiE_elements) auto |
|
112 qed |
|
113 show "\<one>\<^bsub>G i\<^esub> \<in> H i" if "i \<in> I" for i |
|
114 using L subgroup.one_closed that by fastforce |
|
115 show "inv\<^bsub>G i\<^esub> x \<in> H i" if "i \<in> I" and x: "x \<in> H i" for i x |
|
116 proof - |
|
117 have *: "\<forall>y \<in> Pi\<^sub>E I H. \<forall>i\<in>I. inv\<^bsub>G i\<^esub> y i \<in> H i" |
|
118 proof |
|
119 fix y |
|
120 assume y: "y \<in> Pi\<^sub>E I H" |
|
121 then have yc: "y \<in> carrier (product_group I G)" |
|
122 by (metis (no_types) L subgroup_def subsetCE) |
|
123 have "inv\<^bsub>product_group I G\<^esub> y \<in> Pi\<^sub>E I H" |
|
124 by (simp add: y L subgroup.m_inv_closed) |
|
125 moreover have "inv\<^bsub>product_group I G\<^esub> y = (\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> y i)" |
|
126 using yc by (simp add: assms) |
|
127 ultimately show "\<forall>i\<in>I. inv\<^bsub>G i\<^esub> y i \<in> H i" |
|
128 by auto |
|
129 qed |
|
130 then have "\<forall>i\<in>I. \<forall>x\<in>H i. inv\<^bsub>G i\<^esub> x \<in> H i" |
|
131 by (subst(asm) all_PiE_elements) auto |
|
132 then show ?thesis |
|
133 using that(1) x by blast |
|
134 qed |
|
135 qed |
|
136 next |
|
137 assume R: ?rhs |
|
138 show ?lhs |
|
139 proof |
|
140 show "Pi\<^sub>E I H \<subseteq> carrier (product_group I G)" |
|
141 using R by (force simp: subgroup_def) |
|
142 show "x \<otimes>\<^bsub>product_group I G\<^esub> y \<in> Pi\<^sub>E I H" if "x \<in> Pi\<^sub>E I H" "y \<in> Pi\<^sub>E I H" for x y |
|
143 using R that by (auto simp: PiE_iff subgroup_def) |
|
144 show "\<one>\<^bsub>product_group I G\<^esub> \<in> Pi\<^sub>E I H" |
|
145 using R by (force simp: subgroup_def) |
|
146 show "inv\<^bsub>product_group I G\<^esub> x \<in> Pi\<^sub>E I H" if "x \<in> Pi\<^sub>E I H" for x |
|
147 proof - |
|
148 have x: "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" |
|
149 using R that by (force simp: subgroup_def) |
|
150 show ?thesis |
|
151 using assms R that by (fastforce simp: x assms subgroup_def) |
|
152 qed |
|
153 qed |
|
154 qed |
|
155 |
|
156 lemma product_group_subgroup_generated: |
|
157 assumes "\<And>i. i \<in> I \<Longrightarrow> subgroup (H i) (G i)" and gp: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" |
|
158 shows "product_group I (\<lambda>i. subgroup_generated (G i) (H i)) |
|
159 = subgroup_generated (product_group I G) (PiE I H)" |
|
160 proof (rule monoid.equality) |
|
161 have [simp]: "\<And>i. i \<in> I \<Longrightarrow> carrier (G i) \<inter> H i = H i" "(\<Pi>\<^sub>E i\<in>I. carrier (G i)) \<inter> Pi\<^sub>E I H = Pi\<^sub>E I H" |
|
162 using assms by (force simp: subgroup_def)+ |
|
163 have "(\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) = generate (product_group I G) (Pi\<^sub>E I H)" |
|
164 proof (rule group.generateI) |
|
165 show "Group.group (product_group I G)" |
|
166 using assms by simp |
|
167 show "subgroup (\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) (product_group I G)" |
|
168 using assms by (simp add: PiE_subgroup_product_group group.generate_is_subgroup subgroup.subset) |
|
169 show "Pi\<^sub>E I H \<subseteq> (\<Pi>\<^sub>E i\<in>I. generate (G i) (H i))" |
|
170 using assms by (auto simp: PiE_iff generate.incl) |
|
171 show "(\<Pi>\<^sub>E i\<in>I. generate (G i) (H i)) \<subseteq> K" |
|
172 if "subgroup K (product_group I G)" "Pi\<^sub>E I H \<subseteq> K" for K |
|
173 using assms that group.generate_subgroup_incl by fastforce |
|
174 qed |
|
175 with assms |
|
176 show "carrier (product_group I (\<lambda>i. subgroup_generated (G i) (H i))) = |
|
177 carrier (subgroup_generated (product_group I G) (Pi\<^sub>E I H))" |
|
178 by (simp add: carrier_subgroup_generated cong: PiE_cong) |
|
179 qed auto |
|
180 |
|
181 lemma finite_product_group: |
|
182 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" |
|
183 shows |
|
184 "finite (carrier (product_group I G)) \<longleftrightarrow> |
|
185 finite {i. i \<in> I \<and> ~ trivial_group(G i)} \<and> (\<forall>i \<in> I. finite(carrier(G i)))" |
|
186 proof - |
|
187 have [simp]: "\<And>i. i \<in> I \<Longrightarrow> carrier (G i) \<noteq> {}" |
|
188 using assms group.is_monoid by blast |
|
189 show ?thesis |
|
190 by (auto simp: finite_PiE_iff PiE_eq_empty_iff group.trivial_group_alt [OF assms] cong: Collect_cong conj_cong) |
|
191 qed |
|
192 |
|
193 subsection \<open>Sum of a Family of Groups\<close> |
|
194 |
|
195 definition sum_group :: "'a set \<Rightarrow> ('a \<Rightarrow> ('b, 'c) monoid_scheme) \<Rightarrow> ('a \<Rightarrow> 'b) monoid" |
|
196 where "sum_group I G \<equiv> |
|
197 subgroup_generated |
|
198 (product_group I G) |
|
199 {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
200 |
|
201 lemma subgroup_sum_group: |
|
202 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" |
|
203 shows "subgroup {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}} |
|
204 (product_group I G)" |
|
205 proof unfold_locales |
|
206 fix x y |
|
207 have *: "{i. (i \<in> I \<longrightarrow> x i \<otimes>\<^bsub>G i\<^esub> y i \<noteq> \<one>\<^bsub>G i\<^esub>) \<and> i \<in> I} |
|
208 \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}" |
|
209 by (auto simp: Group.group_def dest: assms) |
|
210 assume |
|
211 "x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
212 "y \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
213 then |
|
214 show "x \<otimes>\<^bsub>product_group I G\<^esub> y \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
215 using assms |
|
216 apply (auto simp: Group.group_def monoid.m_closed PiE_iff) |
|
217 apply (rule finite_subset [OF *]) |
|
218 by blast |
|
219 next |
|
220 fix x |
|
221 assume "x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
222 then show "inv\<^bsub>product_group I G\<^esub> x \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
223 using assms |
|
224 by (auto simp: PiE_iff assms group.inv_eq_1_iff [OF assms] conj_commute cong: rev_conj_cong) |
|
225 qed (use assms [unfolded Group.group_def] in auto) |
|
226 |
|
227 lemma carrier_sum_group: |
|
228 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" |
|
229 shows "carrier(sum_group I G) = {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
230 proof - |
|
231 interpret SG: subgroup "{x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" "(product_group I G)" |
|
232 by (simp add: assms subgroup_sum_group) |
|
233 show ?thesis |
|
234 by (simp add: sum_group_def subgroup_sum_group carrier_subgroup_generated_alt) |
|
235 qed |
|
236 |
|
237 lemma one_sum_group [simp]: "\<one>\<^bsub>sum_group I G\<^esub> = (\<lambda>i\<in>I. \<one>\<^bsub>G i\<^esub>)" |
|
238 by (simp add: sum_group_def) |
|
239 |
|
240 lemma mult_sum_group [simp]: "(\<otimes>\<^bsub>sum_group I G\<^esub>) = (\<lambda>x y. (\<lambda>i\<in>I. x i \<otimes>\<^bsub>G i\<^esub> y i))" |
|
241 by (auto simp: sum_group_def) |
|
242 |
|
243 lemma sum_group [simp]: |
|
244 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" shows "group (sum_group I G)" |
|
245 proof (rule groupI) |
|
246 note group.is_monoid [OF assms, simp] |
|
247 show "x \<otimes>\<^bsub>sum_group I G\<^esub> y \<in> carrier (sum_group I G)" |
|
248 if "x \<in> carrier (sum_group I G)" and |
|
249 "y \<in> carrier (sum_group I G)" for x y |
|
250 proof - |
|
251 have *: "{i \<in> I. x i \<otimes>\<^bsub>G i\<^esub> y i \<noteq> \<one>\<^bsub>G i\<^esub>} \<subseteq> {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<union> {i \<in> I. y i \<noteq> \<one>\<^bsub>G i\<^esub>}" |
|
252 by auto |
|
253 show ?thesis |
|
254 using that |
|
255 apply (simp add: assms carrier_sum_group PiE_iff monoid.m_closed conj_commute cong: rev_conj_cong) |
|
256 apply (blast intro: finite_subset [OF *]) |
|
257 done |
|
258 qed |
|
259 show "\<one>\<^bsub>sum_group I G\<^esub> \<otimes>\<^bsub>sum_group I G\<^esub> x = x" |
|
260 if "x \<in> carrier (sum_group I G)" for x |
|
261 using that by (auto simp: assms carrier_sum_group PiE_iff extensional_def) |
|
262 show "\<exists>y\<in>carrier (sum_group I G). y \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>" |
|
263 if "x \<in> carrier (sum_group I G)" for x |
|
264 proof |
|
265 let ?y = "\<lambda>i\<in>I. m_inv (G i) (x i)" |
|
266 show "?y \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>" |
|
267 using that assms |
|
268 by (auto simp: carrier_sum_group PiE_iff group.l_inv) |
|
269 show "?y \<in> carrier (sum_group I G)" |
|
270 using that assms |
|
271 by (auto simp: carrier_sum_group PiE_iff group.inv_eq_1_iff group.l_inv cong: conj_cong) |
|
272 qed |
|
273 qed (auto simp: assms carrier_sum_group PiE_iff group.is_monoid monoid.m_assoc) |
|
274 |
|
275 lemma inv_sum_group [simp]: |
|
276 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and x: "x \<in> carrier (sum_group I G)" |
|
277 shows "m_inv (sum_group I G) x = (\<lambda>i\<in>I. m_inv (G i) (x i))" |
|
278 proof (rule group.inv_equality) |
|
279 show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i) \<otimes>\<^bsub>sum_group I G\<^esub> x = \<one>\<^bsub>sum_group I G\<^esub>" |
|
280 using x by (auto simp: carrier_sum_group PiE_iff group.l_inv assms intro: restrict_ext) |
|
281 show "(\<lambda>i\<in>I. inv\<^bsub>G i\<^esub> x i) \<in> carrier (sum_group I G)" |
|
282 using x by (simp add: carrier_sum_group PiE_iff group.inv_eq_1_iff assms conj_commute cong: rev_conj_cong) |
|
283 qed (auto simp: assms) |
|
284 |
|
285 |
|
286 thm group.subgroups_Inter (*REPLACE*) |
|
287 theorem subgroup_Inter: |
|
288 assumes subgr: "(\<And>H. H \<in> A \<Longrightarrow> subgroup H G)" |
|
289 and not_empty: "A \<noteq> {}" |
|
290 shows "subgroup (\<Inter>A) G" |
|
291 proof |
|
292 show "\<Inter> A \<subseteq> carrier G" |
|
293 by (simp add: Inf_less_eq not_empty subgr subgroup.subset) |
|
294 qed (auto simp: subgr subgroup.m_closed subgroup.one_closed subgroup.m_inv_closed) |
|
295 |
|
296 thm group.subgroups_Inter_pair (*REPLACE*) |
|
297 lemma subgroup_Int: |
|
298 assumes "subgroup I G" "subgroup J G" |
|
299 shows "subgroup (I \<inter> J) G" using subgroup_Inter[ where ?A = "{I,J}"] assms by auto |
|
300 |
|
301 |
|
302 lemma sum_group_subgroup_generated: |
|
303 assumes "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and sg: "\<And>i. i \<in> I \<Longrightarrow> subgroup (H i) (G i)" |
|
304 shows "sum_group I (\<lambda>i. subgroup_generated (G i) (H i)) = subgroup_generated (sum_group I G) (PiE I H)" |
|
305 proof (rule monoid.equality) |
|
306 have "subgroup (carrier (sum_group I G) \<inter> Pi\<^sub>E I H) (product_group I G)" |
|
307 by (rule subgroup_Int) (auto simp: assms carrier_sum_group subgroup_sum_group PiE_subgroup_product_group) |
|
308 moreover have "carrier (sum_group I G) \<inter> Pi\<^sub>E I H |
|
309 \<subseteq> carrier (subgroup_generated (product_group I G) |
|
310 {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}})" |
|
311 by (simp add: assms subgroup_sum_group subgroup.carrier_subgroup_generated_subgroup carrier_sum_group) |
|
312 ultimately |
|
313 have "subgroup (carrier (sum_group I G) \<inter> Pi\<^sub>E I H) (sum_group I G)" |
|
314 by (simp add: assms sum_group_def group.subgroup_subgroup_generated_iff) |
|
315 then have *: "{f \<in> \<Pi>\<^sub>E i\<in>I. carrier (subgroup_generated (G i) (H i)). finite {i \<in> I. f i \<noteq> \<one>\<^bsub>G i\<^esub>}} |
|
316 = carrier (subgroup_generated (sum_group I G) (carrier (sum_group I G) \<inter> Pi\<^sub>E I H))" |
|
317 apply (simp only: subgroup.carrier_subgroup_generated_subgroup) |
|
318 using subgroup.subset [OF sg] |
|
319 apply (auto simp: set_eq_iff PiE_def Pi_def assms carrier_sum_group subgroup.carrier_subgroup_generated_subgroup) |
|
320 done |
|
321 then show "carrier (sum_group I (\<lambda>i. subgroup_generated (G i) (H i))) = |
|
322 carrier (subgroup_generated (sum_group I G) (Pi\<^sub>E I H))" |
|
323 by simp (simp add: assms group.subgroupE(1) group.group_subgroup_generated carrier_sum_group) |
|
324 qed (auto simp: sum_group_def subgroup_generated_def) |
|
325 |
|
326 |
|
327 lemma iso_product_groupI: |
|
328 assumes iso: "\<And>i. i \<in> I \<Longrightarrow> G i \<cong> H i" |
|
329 and G: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and H: "\<And>i. i \<in> I \<Longrightarrow> group (H i)" |
|
330 shows "product_group I G \<cong> product_group I H" (is "?IG \<cong> ?IH") |
|
331 proof - |
|
332 have "\<And>i. i \<in> I \<Longrightarrow> \<exists>h. h \<in> iso (G i) (H i)" |
|
333 using iso by (auto simp: is_iso_def) |
|
334 then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> iso (G i) (H i)" |
|
335 by metis |
|
336 define h where "h \<equiv> \<lambda>x. (\<lambda>i\<in>I. f i (x i))" |
|
337 have hom: "h \<in> iso ?IG ?IH" |
|
338 proof (rule isoI) |
|
339 show hom: "h \<in> hom ?IG ?IH" |
|
340 proof (rule homI) |
|
341 fix x |
|
342 assume "x \<in> carrier ?IG" |
|
343 with f show "h x \<in> carrier ?IH" |
|
344 using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def) |
|
345 next |
|
346 fix x y |
|
347 assume "x \<in> carrier ?IG" "y \<in> carrier ?IG" |
|
348 with f show "h (x \<otimes>\<^bsub>?IG\<^esub> y) = h x \<otimes>\<^bsub>?IH\<^esub> h y" |
|
349 apply (simp add: h_def PiE_def iso_def hom_def) |
|
350 using PiE by (fastforce simp add: h_def PiE_def iso_def hom_def intro: restrict_ext) |
|
351 qed |
|
352 with G H interpret GH : group_hom "?IG" "?IH" h |
|
353 by (simp add: group_hom_def group_hom_axioms_def) |
|
354 show "bij_betw h (carrier ?IG) (carrier ?IH)" |
|
355 unfolding bij_betw_def |
|
356 proof (intro conjI subset_antisym) |
|
357 have "\<gamma> i = \<one>\<^bsub>G i\<^esub>" |
|
358 if \<gamma>: "\<gamma> \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" and eq: "(\<lambda>i\<in>I. f i (\<gamma> i)) = (\<lambda>i\<in>I. \<one>\<^bsub>H i\<^esub>)" and "i \<in> I" |
|
359 for \<gamma> i |
|
360 proof - |
|
361 have "inj_on (f i) (carrier (G i))" "f i \<in> hom (G i) (H i)" |
|
362 using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def) |
|
363 then have *: "\<And>x. \<lbrakk>f i x = \<one>\<^bsub>H i\<^esub>; x \<in> carrier (G i)\<rbrakk> \<Longrightarrow> x = \<one>\<^bsub>G i\<^esub>" |
|
364 by (metis G Group.group_def H hom_one inj_onD monoid.one_closed \<open>i \<in> I\<close>) |
|
365 show ?thesis |
|
366 using eq \<open>i \<in> I\<close> * \<gamma> by (simp add: fun_eq_iff) (meson PiE_iff) |
|
367 qed |
|
368 then show "inj_on h (carrier ?IG)" |
|
369 apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff flip: carrier_product_group) |
|
370 apply (force simp: h_def) |
|
371 done |
|
372 next |
|
373 show "h ` carrier ?IG \<subseteq> carrier ?IH" |
|
374 unfolding h_def using f |
|
375 by (force simp: PiE_def Pi_def Group.iso_def dest!: bij_betwE) |
|
376 next |
|
377 show "carrier ?IH \<subseteq> h ` carrier ?IG" |
|
378 unfolding h_def |
|
379 proof (clarsimp simp: iso_def bij_betw_def) |
|
380 fix x |
|
381 assume "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (H i))" |
|
382 with f have x: "x \<in> (\<Pi>\<^sub>E i\<in>I. f i ` carrier (G i))" |
|
383 unfolding h_def by (auto simp: iso_def bij_betw_def) |
|
384 have "\<And>i. i \<in> I \<Longrightarrow> inj_on (f i) (carrier (G i))" |
|
385 using f by (auto simp: iso_def bij_betw_def) |
|
386 let ?g = "\<lambda>i\<in>I. inv_into (carrier (G i)) (f i) (x i)" |
|
387 show "x \<in> (\<lambda>g. \<lambda>i\<in>I. f i (g i)) ` (\<Pi>\<^sub>E i\<in>I. carrier (G i))" |
|
388 proof |
|
389 show "x = (\<lambda>i\<in>I. f i (?g i))" |
|
390 using x by (auto simp: PiE_iff fun_eq_iff extensional_def f_inv_into_f) |
|
391 show "?g \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" |
|
392 using x by (auto simp: PiE_iff inv_into_into) |
|
393 qed |
|
394 qed |
|
395 qed |
|
396 qed |
|
397 then show ?thesis |
|
398 using is_iso_def by auto |
|
399 qed |
|
400 |
|
401 lemma iso_sum_groupI: |
|
402 assumes iso: "\<And>i. i \<in> I \<Longrightarrow> G i \<cong> H i" |
|
403 and G: "\<And>i. i \<in> I \<Longrightarrow> group (G i)" and H: "\<And>i. i \<in> I \<Longrightarrow> group (H i)" |
|
404 shows "sum_group I G \<cong> sum_group I H" (is "?IG \<cong> ?IH") |
|
405 proof - |
|
406 have "\<And>i. i \<in> I \<Longrightarrow> \<exists>h. h \<in> iso (G i) (H i)" |
|
407 using iso by (auto simp: is_iso_def) |
|
408 then obtain f where f: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> iso (G i) (H i)" |
|
409 by metis |
|
410 then have injf: "inj_on (f i) (carrier (G i))" |
|
411 and homf: "f i \<in> hom (G i) (H i)" if "i \<in> I" for i |
|
412 using \<open>i \<in> I\<close> f by (auto simp: iso_def bij_betw_def) |
|
413 then have one: "\<And>x. \<lbrakk>f i x = \<one>\<^bsub>H i\<^esub>; x \<in> carrier (G i)\<rbrakk> \<Longrightarrow> x = \<one>\<^bsub>G i\<^esub>" if "i \<in> I" for i |
|
414 by (metis G H group.subgroup_self hom_one inj_on_eq_iff subgroup.one_closed that) |
|
415 have fin1: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>} \<Longrightarrow> finite {i \<in> I. f i (x i) \<noteq> \<one>\<^bsub>H i\<^esub>}" for x |
|
416 using homf by (auto simp: G H hom_one elim!: rev_finite_subset) |
|
417 define h where "h \<equiv> \<lambda>x. (\<lambda>i\<in>I. f i (x i))" |
|
418 have hom: "h \<in> iso ?IG ?IH" |
|
419 proof (rule isoI) |
|
420 show hom: "h \<in> hom ?IG ?IH" |
|
421 proof (rule homI) |
|
422 fix x |
|
423 assume "x \<in> carrier ?IG" |
|
424 with f fin1 show "h x \<in> carrier ?IH" |
|
425 by (force simp: h_def PiE_def iso_def hom_def carrier_sum_group assms conj_commute cong: conj_cong) |
|
426 next |
|
427 fix x y |
|
428 assume "x \<in> carrier ?IG" "y \<in> carrier ?IG" |
|
429 with homf show "h (x \<otimes>\<^bsub>?IG\<^esub> y) = h x \<otimes>\<^bsub>?IH\<^esub> h y" |
|
430 by (fastforce simp add: h_def PiE_def hom_def carrier_sum_group assms intro: restrict_ext) |
|
431 qed |
|
432 with G H interpret GH : group_hom "?IG" "?IH" h |
|
433 by (simp add: group_hom_def group_hom_axioms_def) |
|
434 show "bij_betw h (carrier ?IG) (carrier ?IH)" |
|
435 unfolding bij_betw_def |
|
436 proof (intro conjI subset_antisym) |
|
437 have \<gamma>: "\<gamma> i = \<one>\<^bsub>G i\<^esub>" |
|
438 if "\<gamma> \<in> (\<Pi>\<^sub>E i\<in>I. carrier (G i))" and eq: "(\<lambda>i\<in>I. f i (\<gamma> i)) = (\<lambda>i\<in>I. \<one>\<^bsub>H i\<^esub>)" and "i \<in> I" |
|
439 for \<gamma> i |
|
440 using \<open>i \<in> I\<close> one that by (simp add: fun_eq_iff) (meson PiE_iff) |
|
441 show "inj_on h (carrier ?IG)" |
|
442 apply (simp add: iso_def bij_betw_def GH.inj_on_one_iff assms one flip: carrier_sum_group) |
|
443 apply (auto simp: h_def fun_eq_iff carrier_sum_group assms PiE_def Pi_def extensional_def one) |
|
444 done |
|
445 next |
|
446 show "h ` carrier ?IG \<subseteq> carrier ?IH" |
|
447 using homf GH.hom_closed |
|
448 by (fastforce simp: h_def PiE_def Pi_def dest!: bij_betwE) |
|
449 next |
|
450 show "carrier ?IH \<subseteq> h ` carrier ?IG" |
|
451 unfolding h_def |
|
452 proof (clarsimp simp: iso_def bij_betw_def carrier_sum_group assms) |
|
453 fix x |
|
454 assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. carrier (H i))" and fin: "finite {i \<in> I. x i \<noteq> \<one>\<^bsub>H i\<^esub>}" |
|
455 with f have xf: "x \<in> (\<Pi>\<^sub>E i\<in>I. f i ` carrier (G i))" |
|
456 unfolding h_def |
|
457 by (auto simp: iso_def bij_betw_def) |
|
458 have "\<And>i. i \<in> I \<Longrightarrow> inj_on (f i) (carrier (G i))" |
|
459 using f by (auto simp: iso_def bij_betw_def) |
|
460 let ?g = "\<lambda>i\<in>I. inv_into (carrier (G i)) (f i) (x i)" |
|
461 show "x \<in> (\<lambda>g. \<lambda>i\<in>I. f i (g i)) |
|
462 ` {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
463 proof |
|
464 show xeq: "x = (\<lambda>i\<in>I. f i (?g i))" |
|
465 using x by (clarsimp simp: PiE_iff fun_eq_iff extensional_def) (metis iso_iff f_inv_into_f f) |
|
466 have "finite {i \<in> I. inv_into (carrier (G i)) (f i) (x i) \<noteq> \<one>\<^bsub>G i\<^esub>}" |
|
467 apply (rule finite_subset [OF _ fin]) |
|
468 using G H group.subgroup_self hom_one homf injf inv_into_f_eq subgroup.one_closed by fastforce |
|
469 with x show "?g \<in> {x \<in> \<Pi>\<^sub>E i\<in>I. carrier (G i). finite {i \<in> I. x i \<noteq> \<one>\<^bsub>G i\<^esub>}}" |
|
470 apply (auto simp: PiE_iff inv_into_into conj_commute cong: conj_cong) |
|
471 by (metis (no_types, hide_lams) iso_iff f inv_into_into) |
|
472 qed |
|
473 qed |
|
474 qed |
|
475 qed |
|
476 then show ?thesis |
|
477 using is_iso_def by auto |
|
478 qed |
|
479 |
|
480 end |