171 and "inj_on g1 (carrier G1)" |
175 and "inj_on g1 (carrier G1)" |
172 and "g2 ` (carrier G2) = carrier G3" |
176 and "g2 ` (carrier G2) = carrier G3" |
173 shows "(solvable G1) \<and> (solvable G3) \<longleftrightarrow> solvable G2" |
177 shows "(solvable G1) \<and> (solvable G3) \<longleftrightarrow> solvable G2" |
174 using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast |
178 using exact_seq_solvable_recip exact_seq_solvable_imp assms by blast |
175 |
179 |
|
180 |
|
181 lemma exact_seq_eq_triviality: |
|
182 assumes "exact_seq ([E,D,C,B,A], [k,h,g,f])" |
|
183 shows "trivial_group C \<longleftrightarrow> f ` carrier A = carrier B \<and> inj_on k (carrier D)" (is "_ = ?rhs") |
|
184 proof |
|
185 assume C: "trivial_group C" |
|
186 with assms have "inj_on k (carrier D)" |
|
187 apply (auto simp: group_hom.image_from_trivial_group trivial_group_def hom_one) |
|
188 apply (simp add: group_hom_def group_hom_axioms_def group_hom.inj_iff_trivial_ker) |
|
189 done |
|
190 with assms C show ?rhs |
|
191 apply (auto simp: group_hom.image_from_trivial_group trivial_group_def hom_one) |
|
192 apply (auto simp: group_hom_def group_hom_axioms_def hom_def kernel_def) |
|
193 done |
|
194 next |
|
195 assume ?rhs |
|
196 with assms show "trivial_group C" |
|
197 apply (simp add: trivial_group_def) |
|
198 by (metis group_hom.inj_iff_trivial_ker group_hom.trivial_hom_iff group_hom_axioms.intro group_hom_def) |
|
199 qed |
|
200 |
|
201 lemma exact_seq_imp_triviality: |
|
202 "\<lbrakk>exact_seq ([E,D,C,B,A], [k,h,g,f]); f \<in> iso A B; k \<in> iso D E\<rbrakk> \<Longrightarrow> trivial_group C" |
|
203 by (metis (no_types, lifting) Group.iso_def bij_betw_def exact_seq_eq_triviality mem_Collect_eq) |
|
204 |
|
205 lemma exact_seq_epi_eq_triviality: |
|
206 "exact_seq ([D,C,B,A], [h,g,f]) \<Longrightarrow> (f ` carrier A = carrier B) \<longleftrightarrow> trivial_homomorphism B C g" |
|
207 by (auto simp: trivial_homomorphism_def kernel_def) |
|
208 |
|
209 lemma exact_seq_mon_eq_triviality: |
|
210 "exact_seq ([D,C,B,A], [h,g,f]) \<Longrightarrow> inj_on h (carrier C) \<longleftrightarrow> trivial_homomorphism B C g" |
|
211 by (auto simp: trivial_homomorphism_def kernel_def group.is_monoid inj_on_one_iff' image_def) blast |
|
212 |
|
213 lemma exact_sequence_sum_lemma: |
|
214 assumes "comm_group G" and h: "h \<in> iso A C" and k: "k \<in> iso B D" |
|
215 and ex: "exact_seq ([D,G,A], [g,i])" "exact_seq ([C,G,B], [f,j])" |
|
216 and fih: "\<And>x. x \<in> carrier A \<Longrightarrow> f(i x) = h x" |
|
217 and gjk: "\<And>x. x \<in> carrier B \<Longrightarrow> g(j x) = k x" |
|
218 shows "(\<lambda>(x, y). i x \<otimes>\<^bsub>G\<^esub> j y) \<in> Group.iso (A \<times>\<times> B) G \<and> (\<lambda>z. (f z, g z)) \<in> Group.iso G (C \<times>\<times> D)" |
|
219 (is "?ij \<in> _ \<and> ?gf \<in> _") |
|
220 proof (rule epi_iso_compose_rev) |
|
221 interpret comm_group G |
|
222 by (rule assms) |
|
223 interpret f: group_hom G C f |
|
224 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
225 interpret g: group_hom G D g |
|
226 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
227 interpret i: group_hom A G i |
|
228 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
229 interpret j: group_hom B G j |
|
230 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
231 have kerf: "kernel G C f = j ` carrier B" and "group A" "group B" "i \<in> hom A G" |
|
232 using ex by (auto simp: group_hom_def group_hom_axioms_def) |
|
233 then obtain h' where "h' \<in> hom C A" "(\<forall>x \<in> carrier A. h'(h x) = x)" |
|
234 and hh': "(\<forall>y \<in> carrier C. h(h' y) = y)" and "group_isomorphisms A C h h'" |
|
235 using h by (auto simp: group.iso_iff_group_isomorphisms group_isomorphisms_def) |
|
236 have homij: "?ij \<in> hom (A \<times>\<times> B) G" |
|
237 unfolding case_prod_unfold |
|
238 apply (rule hom_group_mult) |
|
239 using ex by (simp_all add: group_hom_def hom_of_fst [unfolded o_def] hom_of_snd [unfolded o_def]) |
|
240 show homgf: "?gf \<in> hom G (C \<times>\<times> D)" |
|
241 using ex by (simp add: hom_paired) |
|
242 show "?ij \<in> epi (A \<times>\<times> B) G" |
|
243 proof (clarsimp simp add: epi_iff_subset homij) |
|
244 fix x |
|
245 assume x: "x \<in> carrier G" |
|
246 with \<open>i \<in> hom A G\<close> \<open>h' \<in> hom C A\<close> have "x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub>(i(h'(f x))) \<in> kernel G C f" |
|
247 by (simp add: kernel_def hom_in_carrier hh' fih) |
|
248 with kerf obtain y where y: "y \<in> carrier B" "j y = x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub>(i(h'(f x)))" |
|
249 by auto |
|
250 have "i (h' (f x)) \<otimes>\<^bsub>G\<^esub> (x \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> i (h' (f x))) = x \<otimes>\<^bsub>G\<^esub> (i (h' (f x)) \<otimes>\<^bsub>G\<^esub> inv\<^bsub>G\<^esub> i (h' (f x)))" |
|
251 by (meson \<open>h' \<in> hom C A\<close> x f.hom_closed hom_in_carrier i.hom_closed inv_closed m_lcomm) |
|
252 also have "\<dots> = x" |
|
253 using \<open>h' \<in> hom C A\<close> hom_in_carrier x by fastforce |
|
254 finally show "x \<in> (\<lambda>(x, y). i x \<otimes>\<^bsub>G\<^esub> j y) ` (carrier A \<times> carrier B)" |
|
255 using x y apply (clarsimp simp: image_def) |
|
256 apply (rule_tac x="h'(f x)" in bexI) |
|
257 apply (rule_tac x=y in bexI, auto) |
|
258 by (meson \<open>h' \<in> hom C A\<close> f.hom_closed hom_in_carrier) |
|
259 qed |
|
260 show "(\<lambda>z. (f z, g z)) \<circ> (\<lambda>(x, y). i x \<otimes>\<^bsub>G\<^esub> j y) \<in> Group.iso (A \<times>\<times> B) (C \<times>\<times> D)" |
|
261 apply (rule group.iso_eq [where f = "\<lambda>(x,y). (h x,k y)"]) |
|
262 using ex |
|
263 apply (auto simp: group_hom_def group_hom_axioms_def DirProd_group iso_paired2 h k fih gjk kernel_def set_eq_iff) |
|
264 apply (metis f.hom_closed f.r_one fih imageI) |
|
265 apply (metis g.hom_closed g.l_one gjk imageI) |
|
266 done |
|
267 qed |
|
268 |
|
269 subsection \<open>Splitting lemmas and Short exact sequences\<close> |
|
270 text\<open>Ported from HOL Light by LCP\<close> |
|
271 |
|
272 definition short_exact_sequence |
|
273 where "short_exact_sequence A B C f g \<equiv> \<exists>T1 T2 e1 e2. exact_seq ([T1,A,B,C,T2], [e1,f,g,e2]) \<and> trivial_group T1 \<and> trivial_group T2" |
|
274 |
|
275 lemma short_exact_sequenceD: |
|
276 assumes "short_exact_sequence A B C f g" shows "exact_seq ([A,B,C], [f,g]) \<and> f \<in> epi B A \<and> g \<in> mon C B" |
|
277 using assms |
|
278 apply (auto simp: short_exact_sequence_def group_hom_def group_hom_axioms_def) |
|
279 apply (simp add: epi_iff_subset group_hom.intro group_hom.kernel_to_trivial_group group_hom_axioms.intro) |
|
280 by (metis (no_types, lifting) group_hom.inj_iff_trivial_ker group_hom.intro group_hom_axioms.intro |
|
281 hom_one image_empty image_insert mem_Collect_eq mon_def trivial_group_def) |
|
282 |
|
283 lemma short_exact_sequence_iff: |
|
284 "short_exact_sequence A B C f g \<longleftrightarrow> exact_seq ([A,B,C], [f,g]) \<and> f \<in> epi B A \<and> g \<in> mon C B" |
|
285 proof - |
|
286 have "short_exact_sequence A B C f g" |
|
287 if "exact_seq ([A, B, C], [f, g])" and "f \<in> epi B A" and "g \<in> mon C B" |
|
288 proof - |
|
289 show ?thesis |
|
290 unfolding short_exact_sequence_def |
|
291 proof (intro exI conjI) |
|
292 have "kernel A (singleton_group \<one>\<^bsub>A\<^esub>) (\<lambda>x. \<one>\<^bsub>A\<^esub>) = f ` carrier B" |
|
293 using that by (simp add: kernel_def singleton_group_def epi_def) |
|
294 moreover have "kernel C B g = {\<one>\<^bsub>C\<^esub>}" |
|
295 using that group_hom.inj_iff_trivial_ker mon_def by fastforce |
|
296 ultimately show "exact_seq ([singleton_group (one A), A, B, C, singleton_group (one C)], [\<lambda>x. \<one>\<^bsub>A\<^esub>, f, g, id])" |
|
297 using that |
|
298 by (simp add: group_hom_def group_hom_axioms_def group.id_hom_singleton) |
|
299 qed auto |
|
300 qed |
|
301 then show ?thesis |
|
302 using short_exact_sequenceD by blast |
|
303 qed |
|
304 |
|
305 lemma very_short_exact_sequence: |
|
306 assumes "exact_seq ([D,C,B,A], [h,g,f])" "trivial_group A" "trivial_group D" |
|
307 shows "g \<in> iso B C" |
|
308 using assms |
|
309 apply simp |
|
310 by (metis (no_types, lifting) group_hom.image_from_trivial_group group_hom.iso_iff |
|
311 group_hom.kernel_to_trivial_group group_hom.trivial_ker_imp_inj group_hom_axioms.intro group_hom_def hom_carrier inj_on_one_iff') |
|
312 |
|
313 lemma splitting_sublemma_gen: |
|
314 assumes ex: "exact_seq ([C,B,A], [g,f])" and fim: "f ` carrier A = H" |
|
315 and "subgroup K B" and 1: "H \<inter> K \<subseteq> {one B}" and eq: "set_mult B H K = carrier B" |
|
316 shows "g \<in> iso (subgroup_generated B K) (subgroup_generated C(g ` carrier B))" |
|
317 proof - |
|
318 interpret KB: subgroup K B |
|
319 by (rule assms) |
|
320 interpret fAB: group_hom A B f |
|
321 using ex by simp |
|
322 interpret gBC: group_hom B C g |
|
323 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
324 have "group A" "group B" "group C" and kerg: "kernel B C g = f ` carrier A" |
|
325 using ex by (auto simp: group_hom_def group_hom_axioms_def) |
|
326 have ker_eq: "kernel B C g = H" |
|
327 using ex by (simp add: fim) |
|
328 then have "subgroup H B" |
|
329 using ex by (simp add: group_hom.img_is_subgroup) |
|
330 show ?thesis |
|
331 unfolding iso_iff |
|
332 proof (intro conjI) |
|
333 show "g \<in> hom (subgroup_generated B K) (subgroup_generated C(g ` carrier B))" |
|
334 by (metis ker_eq \<open>subgroup K B\<close> eq gBC.hom_between_subgroups gBC.set_mult_ker_hom(2) order_refl subgroup.subset) |
|
335 show "g ` carrier (subgroup_generated B K) = carrier (subgroup_generated C(g ` carrier B))" |
|
336 by (metis assms(3) eq fAB.H.subgroupE(1) gBC.img_is_subgroup gBC.set_mult_ker_hom(2) ker_eq subgroup.carrier_subgroup_generated_subgroup) |
|
337 interpret gKBC: group_hom "subgroup_generated B K" C g |
|
338 apply (auto simp: group_hom_def group_hom_axioms_def \<open>group C\<close>) |
|
339 by (simp add: fAB.H.hom_from_subgroup_generated gBC.homh) |
|
340 have *: "x = \<one>\<^bsub>B\<^esub>" |
|
341 if x: "x \<in> carrier (subgroup_generated B K)" and "g x = \<one>\<^bsub>C\<^esub>" for x |
|
342 proof - |
|
343 have x': "x \<in> carrier B" |
|
344 using that fAB.H.carrier_subgroup_generated_subset by blast |
|
345 moreover have "x \<in> H" |
|
346 using kerg fim x' that by (auto simp: kernel_def set_eq_iff) |
|
347 ultimately show ?thesis |
|
348 by (metis "1" x Int_iff singletonD KB.carrier_subgroup_generated_subgroup subsetCE) |
|
349 qed |
|
350 show "inj_on g (carrier (subgroup_generated B K))" |
|
351 using "*" gKBC.inj_on_one_iff by auto |
|
352 qed |
|
353 qed |
|
354 |
|
355 lemma splitting_sublemma: |
|
356 assumes ex: "short_exact_sequence C B A g f" and fim: "f ` carrier A = H" |
|
357 and "subgroup K B" and 1: "H \<inter> K \<subseteq> {one B}" and eq: "set_mult B H K = carrier B" |
|
358 shows "f \<in> iso A (subgroup_generated B H)" (is ?f) |
|
359 "g \<in> iso (subgroup_generated B K) C" (is ?g) |
|
360 proof - |
|
361 show ?f |
|
362 using short_exact_sequenceD [OF ex] |
|
363 apply (clarsimp simp add: group_hom_def group.iso_onto_image) |
|
364 using fim group.iso_onto_image by blast |
|
365 have "C = subgroup_generated C(g ` carrier B)" |
|
366 using short_exact_sequenceD [OF ex] |
|
367 apply simp |
|
368 by (metis epi_iff_subset group.subgroup_generated_group_carrier hom_carrier subset_antisym) |
|
369 then show ?g |
|
370 using short_exact_sequenceD [OF ex] |
|
371 by (metis "1" \<open>subgroup K B\<close> eq fim splitting_sublemma_gen) |
|
372 qed |
|
373 |
|
374 lemma splitting_lemma_left_gen: |
|
375 assumes ex: "exact_seq ([C,B,A], [g,f])" and f': "f' \<in> hom B A" and iso: "(f' \<circ> f) \<in> iso A A" |
|
376 and injf: "inj_on f (carrier A)" and surj: "g ` carrier B = carrier C" |
|
377 obtains H K where "H \<lhd> B" "K \<lhd> B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B" |
|
378 "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C" |
|
379 proof - |
|
380 interpret gBC: group_hom B C g |
|
381 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
382 have "group A" "group B" "group C" and kerg: "kernel B C g = f ` carrier A" |
|
383 using ex by (auto simp: group_hom_def group_hom_axioms_def) |
|
384 then have *: "f ` carrier A \<inter> kernel B A f' = {\<one>\<^bsub>B\<^esub>} \<and> f ` carrier A <#>\<^bsub>B\<^esub> kernel B A f' = carrier B" |
|
385 using group_semidirect_sum_image_ker [of f A B f' A] assms by auto |
|
386 interpret f'AB: group_hom B A f' |
|
387 using assms by (auto simp: group_hom_def group_hom_axioms_def) |
|
388 let ?H = "f ` carrier A" |
|
389 let ?K = "kernel B A f'" |
|
390 show thesis |
|
391 proof |
|
392 show "?H \<lhd> B" |
|
393 by (simp add: gBC.normal_kernel flip: kerg) |
|
394 show "?K \<lhd> B" |
|
395 by (rule f'AB.normal_kernel) |
|
396 show "?H \<inter> ?K \<subseteq> {\<one>\<^bsub>B\<^esub>}" "?H <#>\<^bsub>B\<^esub> ?K = carrier B" |
|
397 using * by auto |
|
398 show "f \<in> Group.iso A (subgroup_generated B ?H)" |
|
399 using ex by (simp add: injf iso_onto_image group_hom_def group_hom_axioms_def) |
|
400 have C: "C = subgroup_generated C(g ` carrier B)" |
|
401 using surj by (simp add: gBC.subgroup_generated_group_carrier) |
|
402 show "g \<in> Group.iso (subgroup_generated B ?K) C" |
|
403 apply (subst C) |
|
404 apply (rule splitting_sublemma_gen [OF ex refl]) |
|
405 using * by (auto simp: f'AB.subgroup_kernel) |
|
406 qed |
|
407 qed |
|
408 |
|
409 lemma splitting_lemma_left: |
|
410 assumes ex: "exact_seq ([C,B,A], [g,f])" and f': "f' \<in> hom B A" |
|
411 and inv: "(\<And>x. x \<in> carrier A \<Longrightarrow> f'(f x) = x)" |
|
412 and injf: "inj_on f (carrier A)" and surj: "g ` carrier B = carrier C" |
|
413 obtains H K where "H \<lhd> B" "K \<lhd> B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B" |
|
414 "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C" |
|
415 proof - |
|
416 interpret fAB: group_hom A B f |
|
417 using ex by simp |
|
418 interpret gBC: group_hom B C g |
|
419 using ex by (simp add: group_hom_def group_hom_axioms_def) |
|
420 have "group A" "group B" "group C" and kerg: "kernel B C g = f ` carrier A" |
|
421 using ex by (auto simp: group_hom_def group_hom_axioms_def) |
|
422 have iso: "f' \<circ> f \<in> Group.iso A A" |
|
423 using ex by (auto simp: inv intro: group.iso_eq [OF \<open>group A\<close> id_iso]) |
|
424 show thesis |
|
425 by (metis that splitting_lemma_left_gen [OF ex f' iso injf surj]) |
|
426 qed |
|
427 |
|
428 lemma splitting_lemma_right_gen: |
|
429 assumes ex: "short_exact_sequence C B A g f" and g': "g' \<in> hom C B" and iso: "(g \<circ> g') \<in> iso C C" |
|
430 obtains H K where "H \<lhd> B" "subgroup K B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B" |
|
431 "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C" |
|
432 proof |
|
433 interpret fAB: group_hom A B f |
|
434 using short_exact_sequenceD [OF ex] by (simp add: group_hom_def group_hom_axioms_def) |
|
435 interpret gBC: group_hom B C g |
|
436 using short_exact_sequenceD [OF ex] by (simp add: group_hom_def group_hom_axioms_def) |
|
437 have *: "f ` carrier A \<inter> g' ` carrier C = {\<one>\<^bsub>B\<^esub>}" |
|
438 "f ` carrier A <#>\<^bsub>B\<^esub> g' ` carrier C = carrier B" |
|
439 "group A" "group B" "group C" |
|
440 "kernel B C g = f ` carrier A" |
|
441 using group_semidirect_sum_ker_image [of g g' C C B] short_exact_sequenceD [OF ex] |
|
442 by (simp_all add: g' iso group_hom_def) |
|
443 show "kernel B C g \<lhd> B" |
|
444 by (simp add: gBC.normal_kernel) |
|
445 show "(kernel B C g) \<inter> (g' ` carrier C) \<subseteq> {\<one>\<^bsub>B\<^esub>}" "(kernel B C g) <#>\<^bsub>B\<^esub> (g' ` carrier C) = carrier B" |
|
446 by (auto simp: *) |
|
447 show "f \<in> Group.iso A (subgroup_generated B (kernel B C g))" |
|
448 by (metis "*"(6) fAB.group_hom_axioms group.iso_onto_image group_hom_def short_exact_sequenceD [OF ex]) |
|
449 show "subgroup (g' ` carrier C) B" |
|
450 using splitting_sublemma |
|
451 by (simp add: fAB.H.is_group g' gBC.is_group group_hom.img_is_subgroup group_hom_axioms_def group_hom_def) |
|
452 then show "g \<in> Group.iso (subgroup_generated B (g' ` carrier C)) C" |
|
453 by (metis (no_types, lifting) iso_iff fAB.H.hom_from_subgroup_generated gBC.homh image_comp inj_on_imageI iso subgroup.carrier_subgroup_generated_subgroup) |
|
454 qed |
|
455 |
|
456 lemma splitting_lemma_right: |
|
457 assumes ex: "short_exact_sequence C B A g f" and g': "g' \<in> hom C B" and gg': "\<And>z. z \<in> carrier C \<Longrightarrow> g(g' z) = z" |
|
458 obtains H K where "H \<lhd> B" "subgroup K B" "H \<inter> K \<subseteq> {one B}" "set_mult B H K = carrier B" |
|
459 "f \<in> iso A (subgroup_generated B H)" "g \<in> iso (subgroup_generated B K) C" |
|
460 proof - |
|
461 have *: "group A" "group B" "group C" |
|
462 using group_semidirect_sum_ker_image [of g g' C C B] short_exact_sequenceD [OF ex] |
|
463 by (simp_all add: g' group_hom_def) |
|
464 show thesis |
|
465 apply (rule splitting_lemma_right_gen [OF ex g' group.iso_eq [OF _ id_iso]]) |
|
466 using * apply (auto simp: gg' intro: that) |
|
467 done |
|
468 qed |
|
469 |
|
470 |
176 end |
471 end |