author | paulson <lp15@cam.ac.uk> |
Sun, 08 Jul 2018 16:07:26 +0100 | |
changeset 68604 | 57721285d4ef |
parent 68555 | 22d51874f37d |
child 68605 | 440aa6b7d99a |
permissions | -rw-r--r-- |
68466 | 1 |
(* Title: HOL/Algebra/Zassenhaus.thy |
2 |
Author: Martin Baillon |
|
3 |
*) |
|
4 |
||
5 |
section \<open>The Zassenhaus Lemma\<close> |
|
6 |
||
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
theory Zassenhaus |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
imports Coset Group_Action |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
9 |
begin |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
10 |
|
68466 | 11 |
text \<open>Proves the second isomorphism theorem and the Zassenhaus lemma.\<close> |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
12 |
|
68466 | 13 |
subsection \<open>Lemmas about normalizer\<close> |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
14 |
|
68466 | 15 |
lemma (in group) subgroup_in_normalizer: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
16 |
assumes "subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
17 |
shows "normal H (G\<lparr>carrier:= (normalizer G H)\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
18 |
proof(intro group.normal_invI) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
19 |
show "Group.group (G\<lparr>carrier := normalizer G H\<rparr>)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
20 |
by (simp add: assms group.normalizer_imp_subgroup is_group subgroup_imp_group subgroup.subset) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
21 |
have K:"H \<subseteq> (normalizer G H)" unfolding normalizer_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
22 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
23 |
fix x assume xH: "x \<in> H" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
24 |
from xH have xG : "x \<in> carrier G" using subgroup.subset assms by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
25 |
have "x <# H = H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
26 |
by (metis \<open>x \<in> H\<close> assms group.lcos_mult_one is_group |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
27 |
l_repr_independence one_closed subgroup.subset) |
68466 | 28 |
moreover have "H #> inv x = H" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
29 |
by (simp add: xH assms is_group subgroup.rcos_const subgroup.m_inv_closed) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
30 |
ultimately have "x <# H #> (inv x) = H" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
31 |
thus " x \<in> stabilizer G (\<lambda>g. \<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
32 |
using assms xG subgroup.subset unfolding stabilizer_def by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
33 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
34 |
thus "subgroup H (G\<lparr>carrier:= (normalizer G H)\<rparr>)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
35 |
using subgroup_incl normalizer_imp_subgroup assms by (simp add: subgroup.subset) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
36 |
show " \<And>x h. x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>) \<Longrightarrow> h \<in> H \<Longrightarrow> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
37 |
x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
38 |
\<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
39 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
40 |
fix x h assume xnorm : "x \<in> carrier (G\<lparr>carrier := normalizer G H\<rparr>)" and hH : "h \<in> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
41 |
have xnormalizer:"x \<in> normalizer G H" using xnorm by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
42 |
moreover have hnormalizer:"h \<in> normalizer G H" using hH K by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
43 |
ultimately have "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h = x \<otimes> h" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
44 |
moreover have " inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x = inv x" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
45 |
using xnormalizer |
68555
22d51874f37d
a few more lemmas from Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
68466
diff
changeset
|
46 |
by (simp add: assms normalizer_imp_subgroup subgroup.subset m_inv_consistent) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
47 |
ultimately have xhxegal: "x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
48 |
\<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
49 |
= x \<otimes>h \<otimes> inv x" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
50 |
using hnormalizer by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
51 |
have "x \<otimes>h \<otimes> inv x \<in> (x <# H #> inv x)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
52 |
unfolding l_coset_def r_coset_def using hH by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
53 |
moreover have "x <# H #> inv x = H" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
54 |
using xnormalizer assms subgroup.subset[OF assms] |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
55 |
unfolding normalizer_def stabilizer_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
56 |
ultimately have "x \<otimes>h \<otimes> inv x \<in> H" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
57 |
thus " x \<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> h |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
58 |
\<otimes>\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> inv\<^bsub>G\<lparr>carrier := normalizer G H\<rparr>\<^esub> x \<in> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
59 |
using xhxegal hH xnorm by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
60 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
61 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
62 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
63 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
64 |
lemma (in group) normal_imp_subgroup_normalizer: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
65 |
assumes "subgroup H G" |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
66 |
and "N \<lhd> (G\<lparr>carrier := H\<rparr>)" |
68466 | 67 |
shows "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
68 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
69 |
have N_carrierG : "N \<subseteq> carrier(G)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
70 |
using assms normal_imp_subgroup subgroup.subset |
68604 | 71 |
using incl_subgroup by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
72 |
{have "H \<subseteq> normalizer G N" unfolding normalizer_def stabilizer_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
73 |
proof |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
74 |
fix x assume xH : "x \<in> H" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
75 |
hence xcarrierG : "x \<in> carrier(G)" using assms subgroup.subset by auto |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
76 |
have " N #> x = x <# N" using assms xH |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
77 |
unfolding r_coset_def l_coset_def normal_def normal_axioms_def subgroup_imp_group by auto |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
78 |
hence "x <# N #> inv x =(N #> x) #> inv x" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
79 |
by simp |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
80 |
also have "... = N #> \<one>" |
68466 | 81 |
using assms r_inv xcarrierG coset_mult_assoc[OF N_carrierG] by simp |
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
82 |
finally have "x <# N #> inv x = N" by (simp add: N_carrierG) |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
83 |
thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) N = N}" |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
84 |
using xcarrierG by (simp add : N_carrierG) |
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
85 |
qed} |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
86 |
thus "subgroup H (G\<lparr>carrier := normalizer G N\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
87 |
using subgroup_incl[OF assms(1) normalizer_imp_subgroup] |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
88 |
assms normal_imp_subgroup subgroup.subset |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
89 |
by (metis group.incl_subgroup is_group) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
90 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
91 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
92 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
93 |
subsection \<open>Second Isomorphism Theorem\<close> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
94 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
95 |
lemma (in group) mult_norm_subgroup: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
96 |
assumes "normal N G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
97 |
and "subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
98 |
shows "subgroup (N<#>H) G" unfolding subgroup_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
99 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
100 |
have A :"N <#> H \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
101 |
using assms setmult_subset_G by (simp add: normal_imp_subgroup subgroup.subset) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
102 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
103 |
have B :"\<And> x y. \<lbrakk>x \<in> (N <#> H); y \<in> (N <#> H)\<rbrakk> \<Longrightarrow> (x \<otimes> y) \<in> (N<#>H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
104 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
105 |
fix x y assume B1a: "x \<in> (N <#> H)" and B1b: "y \<in> (N <#> H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
106 |
obtain n1 h1 where B2:"n1 \<in> N \<and> h1 \<in> H \<and> n1\<otimes>h1 = x" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
107 |
using set_mult_def B1a by (metis (no_types, lifting) UN_E singletonD) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
108 |
obtain n2 h2 where B3:"n2 \<in> N \<and> h2 \<in> H \<and> n2\<otimes>h2 = y" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
109 |
using set_mult_def B1b by (metis (no_types, lifting) UN_E singletonD) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
110 |
have "N #> h1 = h1 <# N" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
111 |
using normalI B2 assms normal.coset_eq subgroup.subset by blast |
68466 | 112 |
hence "h1\<otimes>n2 \<in> N #> h1" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
113 |
using B2 B3 assms l_coset_def by fastforce |
68466 | 114 |
from this obtain y2 where y2_def:"y2 \<in> N" and y2_prop:"y2\<otimes>h1 = h1\<otimes>n2" |
115 |
using singletonD by (metis (no_types, lifting) UN_E r_coset_def) |
|
68604 | 116 |
have "\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G" "\<And>a. a \<in> H \<Longrightarrow> a \<in> carrier G" |
117 |
by (meson assms normal_def subgroup.mem_carrier)+ |
|
118 |
then have "x\<otimes>y = n1 \<otimes> y2 \<otimes> h1 \<otimes> h2" using y2_def B2 B3 |
|
119 |
by (metis (no_types) B2 B3 \<open>\<And>a. a \<in> N \<Longrightarrow> a \<in> carrier G\<close> m_assoc m_closed y2_def y2_prop) |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
120 |
moreover have B4 :"n1 \<otimes> y2 \<in>N" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
121 |
using B2 y2_def assms normal_imp_subgroup by (metis subgroup_def) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
122 |
moreover have "h1 \<otimes> h2 \<in>H" using B2 B3 assms by (simp add: subgroup.m_closed) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
123 |
hence "(n1 \<otimes> y2) \<otimes> (h1 \<otimes> h2) \<in>(N<#>H) " |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
124 |
using B4 unfolding set_mult_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
125 |
hence "n1 \<otimes> y2 \<otimes> h1 \<otimes> h2 \<in>(N<#>H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
126 |
using m_assoc B2 B3 assms normal_imp_subgroup by (metis B4 subgroup.mem_carrier) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
127 |
ultimately show "x \<otimes> y \<in> N <#> H" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
128 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
129 |
have C :"\<And> x. x\<in>(N<#>H) \<Longrightarrow> (inv x)\<in>(N<#>H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
130 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
131 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
132 |
fix x assume C1 : "x \<in> (N<#>H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
133 |
obtain n h where C2:"n \<in> N \<and> h \<in> H \<and> n\<otimes>h = x" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
134 |
using set_mult_def C1 by (metis (no_types, lifting) UN_E singletonD) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
135 |
have C3 :"inv(n\<otimes>h) = inv(h)\<otimes>inv(n)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
136 |
by (meson C2 assms inv_mult_group normal_imp_subgroup subgroup.mem_carrier) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
137 |
hence "... \<otimes>h \<in> N" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
138 |
using assms C2 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
139 |
by (meson normal.inv_op_closed1 normal_def subgroup.m_inv_closed subgroup.mem_carrier) |
68466 | 140 |
hence C4:"(inv h \<otimes> inv n \<otimes> h) \<otimes> inv h \<in> (N<#>H)" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
141 |
using C2 assms subgroup.m_inv_closed[of H G h] unfolding set_mult_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
142 |
have "inv h \<otimes> inv n \<otimes> h \<otimes> inv h = inv h \<otimes> inv n" |
68466 | 143 |
using subgroup.subset[OF assms(2)] |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
144 |
by (metis A C1 C2 C3 inv_closed inv_solve_right m_closed subsetCE) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
145 |
thus "inv(x)\<in>N<#>H" using C4 C2 C3 by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
146 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
147 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
148 |
have D : "\<one> \<in> N <#> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
149 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
150 |
have D1 : "\<one> \<in> N" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
151 |
using assms by (simp add: normal_def subgroup.one_closed) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
152 |
have D2 :"\<one> \<in> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
153 |
using assms by (simp add: subgroup.one_closed) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
154 |
thus "\<one> \<in> (N <#> H)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
155 |
using set_mult_def D1 assms by fastforce |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
156 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
157 |
thus "(N <#> H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> N <#> H \<longrightarrow> y \<in> N <#> H \<longrightarrow> x \<otimes> y \<in> N <#> H)) \<and> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
158 |
\<one> \<in> N <#> H \<and> (\<forall>x. x \<in> N <#> H \<longrightarrow> inv x \<in> N <#> H)" using A B C D assms by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
159 |
qed |
68466 | 160 |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
161 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
162 |
lemma (in group) mult_norm_sub_in_sub: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
163 |
assumes "normal N (G\<lparr>carrier:=K\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
164 |
assumes "subgroup H (G\<lparr>carrier:=K\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
165 |
assumes "subgroup K G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
166 |
shows "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
167 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
168 |
have Hyp:"subgroup (N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) (G\<lparr>carrier := K\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
169 |
using group.mult_norm_subgroup[where ?G = "G\<lparr>carrier := K\<rparr>"] assms subgroup_imp_group by auto |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
170 |
have "H \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms subgroup.subset by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
171 |
also have "... \<subseteq> K" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
172 |
finally have Incl1:"H \<subseteq> K" by simp |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
173 |
have "N \<subseteq> carrier(G\<lparr>carrier := K\<rparr>)" using assms normal_imp_subgroup subgroup.subset by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
174 |
also have "... \<subseteq> K" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
175 |
finally have Incl2:"N \<subseteq> K" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
176 |
have "(N <#>\<^bsub>G\<lparr>carrier := K\<rparr>\<^esub> H) = (N <#> H)" |
68555
22d51874f37d
a few more lemmas from Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
68466
diff
changeset
|
177 |
using set_mult_consistent by simp |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
178 |
thus "subgroup (N<#>H) (G\<lparr>carrier:=K\<rparr>)" using Hyp by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
179 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
180 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
181 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
182 |
lemma (in group) subgroup_of_normal_set_mult: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
183 |
assumes "normal N G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
184 |
and "subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
185 |
shows "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
186 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
187 |
have "\<one> \<in> N" using normal_imp_subgroup assms(1) subgroup_def by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
188 |
hence "\<one> <# H \<subseteq> N <#> H" unfolding set_mult_def l_coset_def by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
189 |
hence H_incl : "H \<subseteq> N <#> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
190 |
by (metis assms(2) lcos_mult_one subgroup_def) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
191 |
show "subgroup H (G\<lparr>carrier := N <#> H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
192 |
using subgroup_incl[OF assms(2) mult_norm_subgroup[OF assms(1) assms(2)] H_incl] . |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
193 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
194 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
195 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
196 |
lemma (in group) normal_in_normal_set_mult: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
197 |
assumes "normal N G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
198 |
and "subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
199 |
shows "normal N (G\<lparr>carrier := N <#> H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
200 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
201 |
have "\<one> \<in> H" using assms(2) subgroup_def by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
202 |
hence "N #> \<one> \<subseteq> N <#> H" unfolding set_mult_def r_coset_def by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
203 |
hence N_incl : "N \<subseteq> N <#> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
204 |
by (metis assms(1) normal_imp_subgroup coset_mult_one subgroup_def) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
205 |
thus "normal N (G\<lparr>carrier := N <#> H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
206 |
using normal_inter_subgroup[OF mult_norm_subgroup[OF assms] assms(1)] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
207 |
by (simp add : inf_absorb1) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
208 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
209 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
210 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
211 |
proposition (in group) weak_snd_iso_thme: |
68466 | 212 |
assumes "subgroup H G" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
213 |
and "N\<lhd>G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
214 |
shows "(G\<lparr>carrier := N<#>H\<rparr> Mod N \<cong> G\<lparr>carrier:=H\<rparr> Mod (N\<inter>H))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
215 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
216 |
define f where "f = (#>) N" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
217 |
have GroupNH : "Group.group (G\<lparr>carrier := N<#>H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
218 |
using subgroup_imp_group assms mult_norm_subgroup by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
219 |
have HcarrierNH :"H \<subseteq> carrier(G\<lparr>carrier := N<#>H\<rparr>)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
220 |
using assms subgroup_of_normal_set_mult subgroup.subset by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
221 |
hence HNH :"H \<subseteq> N<#>H" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
222 |
have op_hom : "f \<in> hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N)" unfolding hom_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
223 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
224 |
have "\<And>x . x \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<Longrightarrow> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
225 |
(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
226 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
227 |
fix x assume "x \<in> carrier (G\<lparr>carrier :=H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
228 |
hence xH : "x \<in> H" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
229 |
hence "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in> rcosets\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> N" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
230 |
using HcarrierNH RCOSETS_def[where ?G = "G\<lparr>carrier := N <#> H\<rparr>"] by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
231 |
thus "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N x \<in> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
232 |
unfolding FactGroup_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
233 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
234 |
hence "(#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<rightarrow> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
235 |
carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
236 |
hence "f \<in> carrier (G\<lparr>carrier :=H\<rparr>) \<rightarrow> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
237 |
unfolding r_coset_def f_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
238 |
moreover have "\<And>x y. x\<in>carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> y\<in>carrier (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
239 |
f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) = f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
240 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
241 |
fix x y assume "x\<in>carrier (G\<lparr>carrier := H\<rparr>)" "y\<in>carrier (G\<lparr>carrier := H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
242 |
hence xHyH :"x \<in> H" "y \<in> H" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
243 |
have Nxeq :"N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x = N #>x" unfolding r_coset_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
244 |
have Nyeq :"N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y = N #>y" unfolding r_coset_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
245 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
246 |
have "x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y =x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
247 |
hence "N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
248 |
= N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x \<otimes>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
249 |
also have "... = (N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> x) <#>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
250 |
(N #>\<^bsub>G\<lparr>carrier := N<#>H\<rparr>\<^esub> y)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
251 |
using normal.rcos_sum[OF normal_in_normal_set_mult[OF assms(2) assms(1)], of x y] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
252 |
xHyH assms HcarrierNH by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
253 |
finally show "f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) = f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
254 |
unfolding FactGroup_def r_coset_def f_def using Nxeq Nyeq by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
255 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
256 |
hence "(\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>). |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
257 |
f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) = f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))" by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
258 |
ultimately show " f \<in> carrier (G\<lparr>carrier := H\<rparr>) \<rightarrow> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N) \<and> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
259 |
(\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>). |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
260 |
f (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) = f(x) \<otimes>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub> f(y))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
261 |
by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
262 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
263 |
hence homomorphism : "group_hom (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N <#> H\<rparr> Mod N) f" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
264 |
unfolding group_hom_def group_hom_axioms_def using subgroup_imp_group[OF assms(1)] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
265 |
normal.factorgroup_is_group[OF normal_in_normal_set_mult[OF assms(2) assms(1)]] by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
266 |
moreover have im_f : "(f ` carrier(G\<lparr>carrier:=H\<rparr>)) = carrier(G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
267 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
268 |
show "f ` carrier (G\<lparr>carrier := H\<rparr>) \<subseteq> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
269 |
using op_hom unfolding hom_def using funcset_image by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
270 |
next |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
271 |
show "carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N) \<subseteq> f ` carrier (G\<lparr>carrier := H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
272 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
273 |
fix x assume p : " x \<in> carrier (G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
274 |
hence "x \<in> \<Union>{y. \<exists>x\<in>carrier (G\<lparr>carrier := N <#> H\<rparr>). y = {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> x}}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
275 |
unfolding FactGroup_def RCOSETS_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
276 |
hence hyp :"\<exists>y. \<exists>h\<in>carrier (G\<lparr>carrier := N <#> H\<rparr>). y = {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> h} \<and> x \<in> y" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
277 |
using Union_iff by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
278 |
from hyp obtain nh where nhNH:"nh \<in>carrier (G\<lparr>carrier := N <#> H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
279 |
and "x \<in> {N #>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub> nh}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
280 |
by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
281 |
hence K: "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N nh" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
282 |
have "nh \<in> N <#> H" using nhNH by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
283 |
from this obtain n h where nN : "n \<in> N" and hH : " h \<in> H" and nhnh: "n \<otimes> h = nh" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
284 |
unfolding set_mult_def by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
285 |
have "x = (#>\<^bsub>G\<lparr>carrier := N <#> H\<rparr>\<^esub>) N (n \<otimes> h)" using K nhnh by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
286 |
hence "x = (#>) N (n \<otimes> h)" using K nhnh unfolding r_coset_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
287 |
also have "... = (N #> n) #>h" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
288 |
using coset_mult_assoc hH nN assms subgroup.subset normal_imp_subgroup |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
289 |
by (metis subgroup.mem_carrier) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
290 |
finally have "x = (#>) N h" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
291 |
using coset_join2[of n N] nN assms by (simp add: normal_imp_subgroup subgroup.mem_carrier) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
292 |
thus "x \<in> f ` carrier (G\<lparr>carrier := H\<rparr>)" using hH unfolding f_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
293 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
294 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
295 |
moreover have ker_f :"kernel (G\<lparr>carrier := H\<rparr>) (G\<lparr>carrier := N<#>H\<rparr> Mod N) f = N\<inter>H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
296 |
unfolding kernel_def f_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
297 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
298 |
have "{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = \<one>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub>} = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
299 |
{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N #> x = N}" unfolding FactGroup_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
300 |
also have "... = {x \<in> carrier (G\<lparr>carrier := H\<rparr>). x \<in> N}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
301 |
using coset_join1 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
302 |
by (metis (no_types, lifting) assms group.subgroup_self incl_subgroup is_group |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
303 |
normal_imp_subgroup subgroup.mem_carrier subgroup.rcos_const subgroup_imp_group) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
304 |
also have "... =N \<inter> (carrier(G\<lparr>carrier := H\<rparr>))" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
305 |
finally show "{x \<in> carrier (G\<lparr>carrier := H\<rparr>). N#>x = \<one>\<^bsub>G\<lparr>carrier := N <#> H\<rparr> Mod N\<^esub>} = N \<inter> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
306 |
by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
307 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
308 |
ultimately have "(G\<lparr>carrier := H\<rparr> Mod N \<inter> H) \<cong> (G\<lparr>carrier := N <#> H\<rparr> Mod N)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
309 |
using group_hom.FactGroup_iso[OF homomorphism im_f] by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
310 |
hence "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
311 |
by (simp add: group.iso_sym assms normal.factorgroup_is_group normal_inter_subgroup) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
312 |
thus "G\<lparr>carrier := N <#> H\<rparr> Mod N \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
313 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
314 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
315 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
316 |
theorem (in group) snd_iso_thme: |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
317 |
assumes "subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
318 |
and "subgroup N G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
319 |
and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
320 |
shows "(G\<lparr>carrier:= N<#>H\<rparr> Mod N) \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
321 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
322 |
have "G\<lparr>carrier := normalizer G N, carrier := H\<rparr> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
323 |
= G\<lparr>carrier := H\<rparr>" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
324 |
hence "G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
325 |
G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
326 |
moreover have "G\<lparr>carrier := normalizer G N, |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
327 |
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
328 |
G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr>" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
329 |
hence "G\<lparr>carrier := normalizer G N, |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
330 |
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
331 |
G\<lparr>carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
332 |
hence "G\<lparr>carrier := normalizer G N, |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
333 |
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N \<cong> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
334 |
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
335 |
(G\<lparr>carrier:= N<#>H\<rparr> Mod N) \<cong> |
68466 | 336 |
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" |
68555
22d51874f37d
a few more lemmas from Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
68466
diff
changeset
|
337 |
using subgroup.subset[OF assms(3)] |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
338 |
subgroup.subset[OF normal_imp_subgroup[OF subgroup_in_normalizer[OF assms(2)]]] |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
339 |
by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
340 |
ultimately have "G\<lparr>carrier := normalizer G N, |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
341 |
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N \<cong> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
342 |
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
343 |
(G\<lparr>carrier:= N<#>H\<rparr> Mod N) \<cong> G\<lparr>carrier := H\<rparr> Mod N \<inter> H" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
344 |
moreover have "G\<lparr>carrier := normalizer G N, |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
345 |
carrier := N <#>\<^bsub>G\<lparr>carrier := normalizer G N\<rparr>\<^esub> H\<rparr> Mod N \<cong> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
346 |
G\<lparr>carrier := normalizer G N, carrier := H\<rparr> Mod N \<inter> H" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
347 |
using group.weak_snd_iso_thme[OF subgroup_imp_group[OF normalizer_imp_subgroup[OF |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
348 |
subgroup.subset[OF assms(2)]]] assms(3) subgroup_in_normalizer[OF assms(2)]] |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
349 |
by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
350 |
moreover have "H\<inter>N = N\<inter>H" using assms by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
351 |
ultimately show "(G\<lparr>carrier:= N<#>H\<rparr> Mod N) \<cong> G\<lparr>carrier := H\<rparr> Mod H \<inter> N" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
352 |
qed |
68466 | 353 |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
354 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
355 |
corollary (in group) snd_iso_thme_recip : |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
356 |
assumes "subgroup H G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
357 |
and "subgroup N G" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
358 |
and "subgroup H (G\<lparr>carrier:= (normalizer G N)\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
359 |
shows "(G\<lparr>carrier:= H<#>N\<rparr> Mod N) \<cong> (G\<lparr>carrier:= H\<rparr> Mod (H\<inter>N))" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
360 |
by (metis assms commut_normal_subgroup group.subgroup_in_normalizer is_group subgroup.subset |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
361 |
normalizer_imp_subgroup snd_iso_thme) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
362 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
363 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
364 |
subsection\<open>The Zassenhaus Lemma\<close> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
365 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
366 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
367 |
lemma (in group) distinc: |
68466 | 368 |
assumes "subgroup H G" |
369 |
and "H1\<lhd>G\<lparr>carrier := H\<rparr>" |
|
370 |
and "subgroup K G" |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
371 |
and "K1\<lhd>G\<lparr>carrier:=K\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
372 |
shows "subgroup (H\<inter>K) (G\<lparr>carrier:=(normalizer G (H1<#>(H\<inter>K1))) \<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
373 |
proof (intro subgroup_incl[OF subgroups_Inter_pair[OF assms(1) assms(3)]]) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
374 |
show "subgroup (normalizer G (H1 <#> H \<inter> K1)) G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
375 |
using normalizer_imp_subgroup assms normal_imp_subgroup subgroup.subset |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
376 |
by (metis group.incl_subgroup is_group setmult_subset_G subgroups_Inter_pair) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
377 |
next |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
378 |
show "H \<inter> K \<subseteq> normalizer G (H1 <#> H \<inter> K1)" unfolding normalizer_def stabilizer_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
379 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
380 |
fix x assume xHK : "x \<in> H \<inter> K" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
381 |
hence xG : "{x} \<subseteq> carrier G" "{inv x} \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
382 |
using subgroup.subset assms inv_closed xHK by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
383 |
have allG : "H \<subseteq> carrier G" "K \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K1 \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
384 |
using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+ . |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
385 |
have HK1_normal: "H\<inter>K1 \<lhd> (G\<lparr>carrier := H \<inter> K\<rparr>)" using normal_inter[OF assms(3)assms(1)assms(4)] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
386 |
by (simp add : inf_commute) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
387 |
have "H \<inter> K \<subseteq> normalizer G (H \<inter> K1)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
388 |
using subgroup.subset[OF normal_imp_subgroup_normalizer[OF subgroups_Inter_pair[OF |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
389 |
assms(1)assms(3)]HK1_normal]] by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
390 |
hence "x <# (H \<inter> K1) #> inv x = (H \<inter> K1)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
391 |
using xHK subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF assms(3) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
392 |
normal_imp_subgroup[OF assms(4)]]]] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
393 |
unfolding normalizer_def stabilizer_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
394 |
moreover have "H \<subseteq> normalizer G H1" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
395 |
using subgroup.subset[OF normal_imp_subgroup_normalizer[OF assms(1)assms(2)]] by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
396 |
hence "x <# H1 #> inv x = H1" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
397 |
using xHK subgroup.subset[OF incl_subgroup[OF assms(1) normal_imp_subgroup[OF assms(2)]]] |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
398 |
unfolding normalizer_def stabilizer_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
399 |
ultimately have "H1 <#> H \<inter> K1 = (x <# H1 #> inv x) <#> (x <# H \<inter> K1 #> inv x)" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
400 |
also have "... = ({x} <#> H1) <#> {inv x} <#> ({x} <#> H \<inter> K1 <#> {inv x})" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
401 |
by (simp add : r_coset_eq_set_mult l_coset_eq_set_mult) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
402 |
also have "... = ({x} <#> H1 <#> {inv x} <#> {x}) <#> (H \<inter> K1 <#> {inv x})" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
403 |
by (smt Int_lower1 allG xG set_mult_assoc subset_trans setmult_subset_G) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
404 |
also have "... = ({x} <#> H1 <#> {\<one>}) <#> (H \<inter> K1 <#> {inv x})" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
405 |
using allG xG coset_mult_assoc by (simp add: r_coset_eq_set_mult setmult_subset_G) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
406 |
also have "... =({x} <#> H1) <#> (H \<inter> K1 <#> {inv x})" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
407 |
using coset_mult_one r_coset_eq_set_mult[of G H1 \<one>] set_mult_assoc[OF xG(1) allG(3)] allG |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
408 |
by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
409 |
also have "... = {x} <#> (H1 <#> H \<inter> K1) <#> {inv x}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
410 |
using allG xG set_mult_assoc setmult_subset_G by (metis inf.coboundedI2) |
68466 | 411 |
finally have "H1 <#> H \<inter> K1 = x <# (H1 <#> H \<inter> K1) #> inv x" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
412 |
using xG setmult_subset_G allG by (simp add: l_coset_eq_set_mult r_coset_eq_set_mult) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
413 |
thus "x \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H1 <#> H \<inter> K1) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
414 |
= H1 <#> H \<inter> K1}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
415 |
using xG allG setmult_subset_G[OF allG(3), where ?K = "H\<inter>K1"] xHK |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
416 |
by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
417 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
418 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
419 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
420 |
lemma (in group) preliminary1: |
68466 | 421 |
assumes "subgroup H G" |
422 |
and "H1\<lhd>G\<lparr>carrier := H\<rparr>" |
|
423 |
and "subgroup K G" |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
424 |
and "K1\<lhd>G\<lparr>carrier:=K\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
425 |
shows " (H\<inter>K) \<inter> (H1<#>(H\<inter>K1)) = (H1\<inter>K)<#>(H\<inter>K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
426 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
427 |
have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
428 |
using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+. |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
429 |
show "H \<inter> K \<inter> (H1 <#> H \<inter> K1) \<subseteq> H1 \<inter> K <#> H \<inter> K1" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
430 |
proof |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
431 |
fix x assume x_def : "x \<in> (H \<inter> K) \<inter> (H1 <#> (H \<inter> K1))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
432 |
from x_def have x_incl : "x \<in> H" "x \<in> K" "x \<in> (H1 <#> (H \<inter> K1))" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
433 |
then obtain h1 hk1 where h1hk1_def : "h1 \<in> H1" "hk1 \<in> H \<inter> K1" "h1 \<otimes> hk1 = x" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
434 |
using assms unfolding set_mult_def by blast |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
435 |
hence "hk1 \<in> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
436 |
hence "inv hk1 \<in> H \<inter> K" using subgroup.m_inv_closed[OF subgroups_Inter_pair] assms by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
437 |
moreover have "h1 \<otimes> hk1 \<in> H \<inter> K" using x_incl h1hk1_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
438 |
ultimately have "h1 \<otimes> hk1 \<otimes> inv hk1 \<in> H \<inter> K" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
439 |
using subgroup.m_closed[OF subgroups_Inter_pair] assms by auto |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
440 |
hence "h1 \<in> H \<inter> K" using h1hk1_def assms subgroup.subset incl_subgroup normal_imp_subgroup |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
441 |
by (metis Int_iff contra_subsetD inv_solve_right m_closed) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
442 |
hence "h1 \<in> H1 \<inter> H \<inter> K" using h1hk1_def by auto |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
443 |
hence "h1 \<in> H1 \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
444 |
hence "h1 \<otimes> hk1 \<in> (H1\<inter>K)<#>(H\<inter>K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
445 |
using h1hk1_def unfolding set_mult_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
446 |
thus " x \<in> (H1\<inter>K)<#>(H\<inter>K1)" using h1hk1_def x_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
447 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
448 |
show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
449 |
proof- |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
450 |
have "H1 \<inter> K \<subseteq> H \<inter> K" using subgroup.subset[OF normal_imp_subgroup[OF assms(2)]] by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
451 |
moreover have "H \<inter> K1 \<subseteq> H \<inter> K" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
452 |
using subgroup.subset[OF normal_imp_subgroup[OF assms(4)]] by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
453 |
ultimately have "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K" unfolding set_mult_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
454 |
using subgroup.m_closed[OF subgroups_Inter_pair [OF assms(1)assms(3)]] by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
455 |
moreover have "H1 \<inter> K \<subseteq> H1" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
456 |
hence "H1 \<inter> K <#> H \<inter> K1 \<subseteq> (H1 <#> H \<inter> K1)" unfolding set_mult_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
457 |
ultimately show "H1 \<inter> K <#> H \<inter> K1 \<subseteq> H \<inter> K \<inter> (H1 <#> H \<inter> K1)" by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
458 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
459 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
460 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
461 |
lemma (in group) preliminary2: |
68466 | 462 |
assumes "subgroup H G" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
463 |
and "H1\<lhd>G\<lparr>carrier := H\<rparr>" |
68466 | 464 |
and "subgroup K G" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
465 |
and "K1\<lhd>G\<lparr>carrier:=K\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
466 |
shows "(H1<#>(H\<inter>K1)) \<lhd> G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
467 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
468 |
have all_inclG : "H \<subseteq> carrier G" "H1 \<subseteq> carrier G" "K \<subseteq> carrier G" "K1 \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
469 |
using assms subgroup.subset normal_imp_subgroup incl_subgroup apply blast+. |
68466 | 470 |
have subH1:"subgroup (H1 <#> H \<inter> K) (G\<lparr>carrier := H\<rparr>)" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
471 |
using mult_norm_sub_in_sub[OF assms(2)subgroup_incl[OF subgroups_Inter_pair[OF assms(1)assms(3)] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
472 |
assms(1)]] assms by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
473 |
have "Group.group (G\<lparr>carrier:=(H1<#>(H\<inter>K))\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
474 |
using subgroup_imp_group[OF incl_subgroup[OF assms(1) subH1]]. |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
475 |
moreover have subH2 : "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := H\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
476 |
using mult_norm_sub_in_sub[OF assms(2) subgroup_incl[OF subgroups_Inter_pair[OF |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
477 |
assms(1) incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]]] assms by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
478 |
hence "(H\<inter>K1) \<subseteq> (H\<inter>K)" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
479 |
using assms subgroup.subset normal_imp_subgroup monoid.cases_scheme |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
480 |
by (metis inf.mono partial_object.simps(1) partial_object.update_convs(1) subset_refl) |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
481 |
hence incl:"(H1<#>(H\<inter>K1)) \<subseteq> H1<#>(H\<inter>K)" using assms subgroup.subset normal_imp_subgroup |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
482 |
unfolding set_mult_def by blast |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
483 |
hence "subgroup (H1 <#> H \<inter> K1) (G\<lparr>carrier := (H1<#>(H\<inter>K))\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
484 |
using assms subgroup_incl[OF incl_subgroup[OF assms(1)subH2]incl_subgroup[OF assms(1) |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
485 |
subH1]] normal_imp_subgroup subgroup.subset unfolding set_mult_def by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
486 |
moreover have " (\<And> x. x\<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>) \<Longrightarrow> |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
487 |
H1 <#> H\<inter>K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> x = x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
488 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
489 |
fix x assume "x \<in>carrier (G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
490 |
hence x_def : "x \<in> H1 <#> H \<inter> K" by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
491 |
from this obtain h1 hk where h1hk_def :"h1 \<in> H1" "hk \<in> H \<inter> K" "h1 \<otimes> hk = x" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
492 |
unfolding set_mult_def by blast |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
493 |
have xH : "x \<in> H" using subgroup.subset[OF subH1] using x_def by auto |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
494 |
hence allG : "h1 \<in> carrier G" "hk \<in> carrier G" "x \<in> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
495 |
using assms subgroup.subset h1hk_def normal_imp_subgroup incl_subgroup apply blast+. |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
496 |
hence "x <#\<^bsub>G\<lparr>carrier := H1 <#> H\<inter>K\<rparr>\<^esub> (H1 <#> H\<inter>K1) =h1 \<otimes> hk <# (H1 <#> H\<inter>K1)" |
68555
22d51874f37d
a few more lemmas from Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
68466
diff
changeset
|
497 |
using subgroup.subset xH h1hk_def by (simp add: l_coset_def) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
498 |
also have "... = h1 <# (hk <# (H1 <#> H\<inter>K1))" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
499 |
using lcos_m_assoc[OF subgroup.subset[OF incl_subgroup[OF assms(1) subH1]]allG(1)allG(2)] |
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
500 |
by (metis allG(1) allG(2) assms(1) incl_subgroup lcos_m_assoc subH2 subgroup.subset) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
501 |
also have "... = h1 <# (hk <# H1 <#> H\<inter>K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
502 |
using set_mult_assoc all_inclG allG by (simp add: l_coset_eq_set_mult inf.coboundedI1) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
503 |
also have "... = h1 <# (hk <# H1 #> \<one> <#> H\<inter>K1 #> \<one>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
504 |
using coset_mult_one allG all_inclG l_coset_subset_G |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
505 |
by (smt inf_le2 setmult_subset_G subset_trans) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
506 |
also have "... = h1 <# (hk <# H1 #> inv hk #> hk <#> H\<inter>K1 #> inv hk #> hk)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
507 |
using all_inclG allG coset_mult_assoc l_coset_subset_G |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
508 |
by (simp add: inf.coboundedI1 setmult_subset_G) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
509 |
finally have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
510 |
h1 <# ((hk <# H1 #> inv hk) <#> (hk <# H\<inter>K1 #> inv hk) #> hk)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
511 |
using rcos_assoc_lcos allG all_inclG |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
512 |
by (smt inf_le1 inv_closed l_coset_subset_G r_coset_subset_G setmult_rcos_assoc subset_trans) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
513 |
moreover have "H \<subseteq> normalizer G H1" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
514 |
using assms h1hk_def subgroup.subset[OF normal_imp_subgroup_normalizer] by simp |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
515 |
hence "\<And>g. g \<in> H \<Longrightarrow> g \<in> {g \<in> carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) H1 = H1}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
516 |
using all_inclG assms unfolding normalizer_def stabilizer_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
517 |
hence "\<And>g. g \<in> H \<Longrightarrow> g <# H1 #> inv g = H1" using all_inclG by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
518 |
hence "(hk <# H1 #> inv hk) = H1" using h1hk_def all_inclG by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
519 |
moreover have "H\<inter>K \<subseteq> normalizer G (H\<inter>K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
520 |
using normal_inter[OF assms(3)assms(1)assms(4)] assms subgroups_Inter_pair |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
521 |
subgroup.subset[OF normal_imp_subgroup_normalizer] by (simp add: inf_commute) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
522 |
hence "\<And>g. g\<in>H\<inter>K \<Longrightarrow> g\<in>{g\<in>carrier G. (\<lambda>H\<in>{H. H \<subseteq> carrier G}. g <# H #> inv g) (H\<inter>K1) = H\<inter>K1}" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
523 |
using all_inclG assms unfolding normalizer_def stabilizer_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
524 |
hence "\<And>g. g \<in> H\<inter>K \<Longrightarrow> g <# (H\<inter>K1) #> inv g = H\<inter>K1" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
525 |
using subgroup.subset[OF subgroups_Inter_pair[OF assms(1) incl_subgroup[OF |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
526 |
assms(3)normal_imp_subgroup[OF assms(4)]]]] by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
527 |
hence "(hk <# H\<inter>K1 #> inv hk) = H\<inter>K1" using h1hk_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
528 |
ultimately have "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = h1 <#(H1 <#> (H \<inter> K1)#> hk)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
529 |
by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
530 |
also have "... = h1 <# H1 <#> ((H \<inter> K1)#> hk)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
531 |
using set_mult_assoc[where ?M = "{h1}" and ?H = "H1" and ?K = "(H \<inter> K1)#> hk"] allG all_inclG |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
532 |
by (simp add: l_coset_eq_set_mult inf.coboundedI2 r_coset_subset_G setmult_rcos_assoc) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
533 |
also have "... = H1 <#> ((H \<inter> K1)#> hk)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
534 |
using coset_join3 allG incl_subgroup[OF assms(1)normal_imp_subgroup[OF assms(2)]] h1hk_def |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
535 |
by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
536 |
finally have eq1 : "x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1) = H1 <#> (H \<inter> K1) #> hk" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
537 |
by (simp add: allG(2) all_inclG inf.coboundedI2 setmult_rcos_assoc) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
538 |
have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = H1 <#> H \<inter> K1 #> (h1 \<otimes> hk)" |
68555
22d51874f37d
a few more lemmas from Paulo and Martin
paulson <lp15@cam.ac.uk>
parents:
68466
diff
changeset
|
539 |
using subgroup.subset xH h1hk_def by (simp add: r_coset_def) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
540 |
also have "... = H1 <#> H \<inter> K1 #> h1 #> hk" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
541 |
using coset_mult_assoc by (simp add: allG all_inclG inf.coboundedI2 setmult_subset_G) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
542 |
also have"... = H \<inter> K1 <#> H1 #> h1 #> hk" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
543 |
using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
544 |
assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
545 |
also have "... = H \<inter> K1 <#> H1 #> hk" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
546 |
using coset_join2[OF allG(1)incl_subgroup[OF assms(1)normal_imp_subgroup] |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
547 |
h1hk_def(1)] all_inclG allG assms by (metis inf.coboundedI2 setmult_rcos_assoc) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
548 |
finally have "H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x =H1 <#> H \<inter> K1 #> hk" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
549 |
using commut_normal_subgroup[OF assms(1)assms(2)subgroup_incl[OF subgroups_Inter_pair[OF |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
550 |
assms(1)incl_subgroup[OF assms(3)normal_imp_subgroup[OF assms(4)]]]assms(1)]] by simp |
68466 | 551 |
thus " H1 <#> H \<inter> K1 #>\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> x = |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
552 |
x <#\<^bsub>G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>\<^esub> (H1 <#> H \<inter> K1)" using eq1 by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
553 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
554 |
ultimately show "H1 <#> H \<inter> K1 \<lhd> G\<lparr>carrier := H1 <#> H \<inter> K\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
555 |
unfolding normal_def normal_axioms_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
556 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
557 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
558 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
559 |
proposition (in group) Zassenhaus_1: |
68466 | 560 |
assumes "subgroup H G" |
561 |
and "H1\<lhd>G\<lparr>carrier := H\<rparr>" |
|
562 |
and "subgroup K G" |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
563 |
and "K1\<lhd>G\<lparr>carrier:=K\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
564 |
shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>H\<inter>K1)) \<cong> (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod ((H1\<inter>K)<#>(H\<inter>K1)))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
565 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
566 |
define N and N1 where "N = (H\<inter>K)" and "N1 =H1<#>(H\<inter>K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
567 |
have normal_N_N1 : "subgroup N (G\<lparr>carrier:=(normalizer G N1)\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
568 |
by (simp add: N1_def N_def assms distinc normal_imp_subgroup) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
569 |
have Hp:"(G\<lparr>carrier:= N<#>N1\<rparr> Mod N1) \<cong> (G\<lparr>carrier:= N\<rparr> Mod (N\<inter>N1))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
570 |
by (metis N1_def N_def assms incl_subgroup inf_le1 mult_norm_sub_in_sub |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
571 |
normal_N_N1 normal_imp_subgroup snd_iso_thme_recip subgroup_incl subgroups_Inter_pair) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
572 |
have H_simp: "N<#>N1 = H1<#> (H\<inter>K)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
573 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
574 |
have H1_incl_G : "H1 \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
575 |
using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
576 |
have K1_incl_G :"K1 \<subseteq> carrier G" |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
577 |
using assms normal_imp_subgroup incl_subgroup subgroup.subset by blast |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
578 |
have "N<#>N1= (H\<inter>K)<#> (H1<#>(H\<inter>K1))" by (auto simp add: N_def N1_def) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
579 |
also have "... = ((H\<inter>K)<#>H1) <#>(H\<inter>K1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
580 |
using set_mult_assoc[where ?M = "H\<inter>K"] K1_incl_G H1_incl_G assms |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
581 |
by (simp add: inf.coboundedI2 subgroup.subset) |
68466 | 582 |
also have "... = (H1<#>(H\<inter>K))<#>(H\<inter>K1)" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
583 |
using commut_normal_subgroup assms subgroup_incl subgroups_Inter_pair by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
584 |
also have "... = H1 <#> ((H\<inter>K)<#>(H\<inter>K1))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
585 |
using set_mult_assoc K1_incl_G H1_incl_G assms |
68452
c027dfbfad30
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
paulson <lp15@cam.ac.uk>
parents:
68445
diff
changeset
|
586 |
by (simp add: inf.coboundedI2 subgroup.subset) |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
587 |
also have " ((H\<inter>K)<#>(H\<inter>K1)) = (H\<inter>K)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
588 |
proof (intro set_mult_subgroup_idem[where ?H = "H\<inter>K" and ?N="H\<inter>K1", |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
589 |
OF subgroups_Inter_pair[OF assms(1) assms(3)]]) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
590 |
show "subgroup (H \<inter> K1) (G\<lparr>carrier := H \<inter> K\<rparr>)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
591 |
using subgroup_incl[where ?I = "H\<inter>K1" and ?J = "H\<inter>K",OF subgroups_Inter_pair[OF assms(1) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
592 |
incl_subgroup[OF assms(3) normal_imp_subgroup]] subgroups_Inter_pair] assms |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
593 |
normal_imp_subgroup by (metis inf_commute normal_inter) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
594 |
qed |
68466 | 595 |
hence " H1 <#> ((H\<inter>K)<#>(H\<inter>K1)) = H1 <#> ((H\<inter>K))" |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
596 |
by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
597 |
thus "N <#> N1 = H1 <#> H \<inter> K" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
598 |
by (simp add: calculation) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
599 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
600 |
|
68466 | 601 |
have "N\<inter>N1 = (H1\<inter>K)<#>(H\<inter>K1)" |
602 |
using preliminary1 assms N_def N1_def by simp |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
603 |
thus "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod N1) \<cong> (G\<lparr>carrier:= N\<rparr> Mod ((H1\<inter>K)<#>(H\<inter>K1)))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
604 |
using H_simp Hp by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
605 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
606 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
607 |
|
68445
c183a6a69f2d
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
paulson <lp15@cam.ac.uk>
parents:
68443
diff
changeset
|
608 |
theorem (in group) Zassenhaus: |
68466 | 609 |
assumes "subgroup H G" |
610 |
and "H1\<lhd>G\<lparr>carrier := H\<rparr>" |
|
611 |
and "subgroup K G" |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
612 |
and "K1\<lhd>G\<lparr>carrier:=K\<rparr>" |
68466 | 613 |
shows "(G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1))) \<cong> |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
614 |
(G\<lparr>carrier:= K1 <#> (H\<inter>K)\<rparr> Mod (K1<#>(K\<inter>H1)))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
615 |
proof- |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
616 |
define Gmod1 Gmod2 Gmod3 Gmod4 |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
617 |
where "Gmod1 = (G\<lparr>carrier:= H1 <#> (H\<inter>K)\<rparr> Mod (H1<#>(H\<inter>K1))) " |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
618 |
and "Gmod2 = (G\<lparr>carrier:= K1 <#> (K\<inter>H)\<rparr> Mod (K1<#>(K\<inter>H1)))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
619 |
and "Gmod3 = (G\<lparr>carrier:= (H\<inter>K)\<rparr> Mod ((H1\<inter>K)<#>(H\<inter>K1)))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
620 |
and "Gmod4 = (G\<lparr>carrier:= (K\<inter>H)\<rparr> Mod ((K1\<inter>H)<#>(K\<inter>H1)))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
621 |
have Hyp : "Gmod1 \<cong> Gmod3" "Gmod2 \<cong> Gmod4" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
622 |
using Zassenhaus_1 assms Gmod1_def Gmod2_def Gmod3_def Gmod4_def by auto |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
623 |
have Hp : "Gmod3 = G\<lparr>carrier:= (K\<inter>H)\<rparr> Mod ((K\<inter>H1)<#>(K1\<inter>H))" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
624 |
by (simp add: Gmod3_def inf_commute) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
625 |
have "(K\<inter>H1)<#>(K1\<inter>H) = (K1\<inter>H)<#>(K\<inter>H1)" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
626 |
proof (intro commut_normal_subgroup[OF subgroups_Inter_pair[OF assms(1)assms(3)]]) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
627 |
show "K1 \<inter> H \<lhd> G\<lparr>carrier := H \<inter> K\<rparr>" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
628 |
using normal_inter[OF assms(3)assms(1)assms(4)] by (simp add: inf_commute) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
629 |
next |
68466 | 630 |
show "subgroup (K \<inter> H1) (G\<lparr>carrier := H \<inter> K\<rparr>)" |
631 |
using subgroup_incl by (simp add: assms inf_commute normal_imp_subgroup normal_inter) |
|
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
632 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
633 |
hence "Gmod3 = Gmod4" using Hp Gmod4_def by simp |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
634 |
hence "Gmod1 \<cong> Gmod2" |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
635 |
using group.iso_sym group.iso_trans Hyp normal.factorgroup_is_group |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
636 |
by (metis assms Gmod1_def Gmod2_def preliminary2) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
637 |
thus ?thesis using Gmod1_def Gmod2_def by (simp add: inf_commute) |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
638 |
qed |
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
639 |
|
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
640 |
end |