author paulson Wed May 26 11:43:50 2004 +0200 (2004-05-26) changeset 14803 f7557773cc87 parent 14802 e05116289ff9 child 14804 8de39d3e8eb6
more group isomorphisms
 src/HOL/Algebra/Coset.thy file | annotate | diff | revisions src/HOL/Algebra/Group.thy file | annotate | diff | revisions src/HOL/Algebra/Sylow.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/Coset.thy	Mon May 24 18:35:34 2004 +0200
1.2 +++ b/src/HOL/Algebra/Coset.thy	Wed May 26 11:43:50 2004 +0200
1.3 @@ -33,7 +33,7 @@
1.4    normal :: "['a set, ('a,'b) monoid_scheme] => bool"  (infixl "\<lhd>" 60)
1.5
1.6
1.7 -subsection {*Lemmas Using Locale Constants*}
1.8 +subsection {*Basic Properties of Cosets*}
1.9
1.10  lemma (in group) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}"
1.11  by (auto simp add: r_coset_def)
1.12 @@ -187,6 +187,8 @@
1.13    qed
1.14  qed
1.15
1.16 +subsection{*More Properties of Cosets*}
1.17 +
1.18  lemma (in group) lcos_m_assoc:
1.19       "[| M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G |]
1.20        ==> g <# (h <# M) = (g \<otimes> h) <# M"
1.21 @@ -300,7 +302,7 @@
1.22  done
1.23
1.24
1.25 -subsubsection {* Some rules for @{text "<#>"} with @{text "#>"} or @{text "<#"}. *}
1.26 +subsubsection {*Theorems for @{text "<#>"} with @{text "#>"} or @{text "<#"}.*}
1.27
1.28  lemma (in group) setmult_rcos_assoc:
1.29       "[| H \<subseteq> carrier G; K \<subseteq> carrier G; x \<in> carrier G |]
1.30 @@ -345,7 +347,29 @@
1.31      setmult_rcos_assoc subgroup_mult_id)
1.32
1.33
1.34 -subsection {*Lemmas Leading to Lagrange's Theorem *}
1.35 +subsubsection{*Two distinct right cosets are disjoint*}
1.36 +
1.37 +lemma (in group) rcos_equation:
1.38 +     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
1.39 +        h \<in> H;  ha \<in> H;  hb \<in> H|]
1.40 +      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
1.41 +apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
1.42 +apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
1.43 +apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
1.44 +done
1.45 +
1.46 +lemma (in group) rcos_disjoint:
1.47 +     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
1.48 +apply (simp add: setrcos_eq r_coset_eq)
1.49 +apply (blast intro: rcos_equation sym)
1.50 +done
1.51 +
1.52 +
1.53 +subsection {*Order of a Group and Lagrange's Theorem*}
1.54 +
1.55 +constdefs
1.56 +  order :: "('a, 'b) semigroup_scheme => nat"
1.57 +  "order S == card (carrier S)"
1.58
1.59  lemma (in group) setrcos_part_G: "subgroup H G ==> \<Union>rcosets G H = carrier G"
1.60  apply (rule equalityI)
1.61 @@ -387,41 +411,34 @@
1.62  apply (blast intro: finite_subset)
1.63  done
1.64
1.65 -
1.66 -subsection{*Two distinct right cosets are disjoint*}
1.67 -
1.68 -lemma (in group) rcos_equation:
1.69 -     "[|subgroup H G;  a \<in> carrier G;  b \<in> carrier G;  ha \<otimes> a = h \<otimes> b;
1.70 -        h \<in> H;  ha \<in> H;  hb \<in> H|]
1.71 -      ==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a"
1.72 -apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"])
1.73 -apply (simp  add: m_assoc transpose_inv subgroup.subset [THEN subsetD])
1.74 -apply (simp add: subgroup.m_closed subgroup.m_inv_closed)
1.75 -done
1.76 -
1.77 -lemma (in group) rcos_disjoint:
1.78 -     "[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}"
1.79 -apply (simp add: setrcos_eq r_coset_eq)
1.80 -apply (blast intro: rcos_equation sym)
1.81 -done
1.82 -
1.83  lemma (in group) setrcos_subset_PowG:
1.84       "subgroup H G  ==> rcosets G H \<subseteq> Pow(carrier G)"
1.86  apply (blast dest: r_coset_subset_G subgroup.subset)
1.87  done
1.88
1.89 +
1.90 +theorem (in group) lagrange:
1.91 +     "[| finite(carrier G); subgroup H G |]
1.92 +      ==> card(rcosets G H) * card(H) = order(G)"
1.93 +apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
1.94 +apply (subst mult_commute)
1.95 +apply (rule card_partition)
1.96 +   apply (simp add: setrcos_subset_PowG [THEN finite_subset])
1.97 +  apply (simp add: setrcos_part_G)
1.98 + apply (simp add: card_cosets_equal subgroup.subset)
1.100 +done
1.101 +
1.102 +
1.103  subsection {*Quotient Groups: Factorization of a Group*}
1.104
1.105  constdefs
1.106    FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid"
1.107 -     (infixl "Mod" 60)
1.108 +     (infixl "Mod" 65)
1.109      --{*Actually defined for groups rather than monoids*}
1.110    "FactGroup G H ==
1.111 -    (| carrier = rcosets G H,
1.112 -       mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y),
1.113 -       one = H |)"
1.114 -
1.115 +    (| carrier = rcosets G H, mult = set_mult G, one = H |)"
1.116
1.117  lemma (in group) setmult_closed:
1.118       "[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |]
1.119 @@ -435,15 +452,6 @@
1.120                     subgroup.subset rcos_inv
1.121                     setrcos_eq)
1.122
1.123 -(*
1.124 -The old version is no longer valid: "group G" has to be an explicit premise.
1.125 -
1.126 -lemma setinv_closed:
1.127 -     "[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H"
1.128 -by (auto simp add:  normal_imp_subgroup
1.129 -                   subgroup.subset coset.rcos_inv coset.setrcos_eq)
1.130 -*)
1.131 -
1.132  lemma (in group) setrcos_assoc:
1.133       "[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|]
1.134        ==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)"
1.135 @@ -461,18 +469,6 @@
1.136      by (auto simp add: setrcos_eq)
1.137  qed
1.138
1.139 -(*
1.140 -lemma subgroup_in_rcosets:
1.141 -  "subgroup H G ==> H \<in> rcosets G H"
1.142 -apply (frule subgroup_imp_coset)
1.143 -apply (frule subgroup_imp_group)
1.145 -apply (blast del: equalityI
1.146 -             intro!: group.subgroup.one_closed group.one_closed
1.147 -                     coset.coset_join2 [symmetric])
1.148 -done
1.149 -*)
1.150 -
1.151  lemma (in group) setrcos_inv_mult_group_eq:
1.152       "[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H"
1.153  by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup
1.154 @@ -499,6 +495,9 @@
1.155  apply (auto dest: setrcos_inv_mult_group_eq simp add: setinv_closed)
1.156  done
1.157
1.158 +lemma mult_FactGroup [simp]: "X \<otimes>\<^bsub>(G Mod H)\<^esub> X' = X <#>\<^bsub>G\<^esub> X'"
1.159 +  by (simp add: FactGroup_def)
1.160 +
1.161  lemma (in group) inv_FactGroup:
1.162       "N <| G ==> X \<in> carrier (G Mod N) ==> inv\<^bsub>G Mod N\<^esub> X = set_inv G X"
1.163  apply (rule group.inv_equality [OF factorgroup_is_group])
1.164 @@ -512,4 +511,130 @@
1.165    shows "(r_coset G N) \<in> hom G (G Mod N)"
1.166  by (simp add: FactGroup_def rcosets_def Pi_def hom_def rcos_sum N)
1.167
1.168 +
1.169 +subsection{*Quotienting by the Kernel of a Homomorphism*}
1.170 +
1.171 +constdefs
1.172 +  kernel :: "('a, 'm) monoid_scheme => ('b, 'n) monoid_scheme =>
1.173 +             ('a => 'b) => 'a set"
1.174 +    --{*the kernel of a homomorphism*}
1.175 +  "kernel G H h == {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}";
1.176 +
1.177 +lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
1.178 +apply (rule group.subgroupI)
1.179 +apply (auto simp add: kernel_def group.intro prems)
1.180 +done
1.181 +
1.182 +text{*The kernel of a homomorphism is a normal subgroup*}
1.183 +lemma (in group_hom) normal_kernel: "(kernel G H h) <| G"
1.184 +apply (simp add: group.normal_inv_iff subgroup_kernel group.intro prems)
1.186 +done
1.187 +
1.188 +lemma (in group_hom) FactGroup_nonempty:
1.189 +  assumes X: "X \<in> carrier (G Mod kernel G H h)"
1.190 +  shows "X \<noteq> {}"
1.191 +proof -
1.192 +  from X
1.193 +  obtain g where "g \<in> carrier G"
1.194 +             and "X = kernel G H h #> g"
1.195 +    by (auto simp add: FactGroup_def rcosets_def)
1.196 +  thus ?thesis
1.197 +   by (force simp add: kernel_def r_coset_def image_def intro: hom_one)
1.198 +qed
1.199 +
1.200 +
1.201 +lemma (in group_hom) FactGroup_contents_mem:
1.202 +  assumes X: "X \<in> carrier (G Mod (kernel G H h))"
1.203 +  shows "contents (h`X) \<in> carrier H"
1.204 +proof -
1.205 +  from X
1.206 +  obtain g where g: "g \<in> carrier G"
1.207 +             and "X = kernel G H h #> g"
1.208 +    by (auto simp add: FactGroup_def rcosets_def)
1.209 +  hence "h ` X = {h g}" by (force simp add: kernel_def r_coset_def image_def g)
1.210 +  thus ?thesis by (auto simp add: g)
1.211 +qed
1.212 +
1.213 +lemma (in group_hom) FactGroup_hom:
1.214 +     "(%X. contents (h`X)) \<in> hom (G Mod (kernel G H h)) H"
1.215 +proof (simp add: hom_def funcsetI FactGroup_contents_mem, intro ballI)
1.216 +  fix X and X'
1.217 +  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
1.218 +     and X': "X' \<in> carrier (G Mod kernel G H h)"
1.219 +  then
1.220 +  obtain g and g'
1.221 +           where "g \<in> carrier G" and "g' \<in> carrier G"
1.222 +             and "X = kernel G H h #> g" and "X' = kernel G H h #> g'"
1.223 +    by (auto simp add: FactGroup_def rcosets_def)
1.224 +  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
1.225 +    and Xsub: "X \<subseteq> carrier G" and X'sub: "X' \<subseteq> carrier G"
1.226 +    by (force simp add: kernel_def r_coset_def image_def)+
1.227 +  hence "h ` (X <#> X') = {h g \<otimes>\<^bsub>H\<^esub> h g'}" using X X'
1.228 +    by (auto dest!: FactGroup_nonempty
1.229 +             simp add: set_mult_def image_eq_UN
1.230 +                       subsetD [OF Xsub] subsetD [OF X'sub])
1.231 +  thus "contents (h ` (X <#> X')) = contents (h ` X) \<otimes>\<^bsub>H\<^esub> contents (h ` X')"
1.232 +    by (simp add: all image_eq_UN FactGroup_nonempty X X')
1.233 +qed
1.234 +
1.235 +text{*Lemma for the following injectivity result*}
1.236 +lemma (in group_hom) FactGroup_subset:
1.237 +     "[|g \<in> carrier G; g' \<in> carrier G; h g = h g'|]
1.238 +      ==>  kernel G H h #> g \<subseteq> kernel G H h #> g'"
1.239 +apply (clarsimp simp add: kernel_def r_coset_def image_def);
1.240 +apply (rename_tac y)
1.241 +apply (rule_tac x="y \<otimes> g \<otimes> inv g'" in exI)
1.243 +done
1.244 +
1.245 +lemma (in group_hom) FactGroup_inj_on:
1.246 +     "inj_on (\<lambda>X. contents (h ` X)) (carrier (G Mod kernel G H h))"
1.247 +proof (simp add: inj_on_def, clarify)
1.248 +  fix X and X'
1.249 +  assume X:  "X  \<in> carrier (G Mod kernel G H h)"
1.250 +     and X': "X' \<in> carrier (G Mod kernel G H h)"
1.251 +  then
1.252 +  obtain g and g'
1.253 +           where gX: "g \<in> carrier G"  "g' \<in> carrier G"
1.254 +              "X = kernel G H h #> g" "X' = kernel G H h #> g'"
1.255 +    by (auto simp add: FactGroup_def rcosets_def)
1.256 +  hence all: "\<forall>x\<in>X. h x = h g" "\<forall>x\<in>X'. h x = h g'"
1.257 +    by (force simp add: kernel_def r_coset_def image_def)+
1.258 +  assume "contents (h ` X) = contents (h ` X')"
1.259 +  hence h: "h g = h g'"
1.260 +    by (simp add: image_eq_UN all FactGroup_nonempty X X')
1.261 +  show "X=X'" by (rule equalityI) (simp_all add: FactGroup_subset h gX)
1.262 +qed
1.263 +
1.264 +text{*If the homomorphism @{term h} is onto @{term H}, then so is the
1.265 +homomorphism from the quotient group*}
1.266 +lemma (in group_hom) FactGroup_onto:
1.267 +  assumes h: "h ` carrier G = carrier H"
1.268 +  shows "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) = carrier H"
1.269 +proof
1.270 +  show "(\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h) \<subseteq> carrier H"
1.271 +    by (auto simp add: FactGroup_contents_mem)
1.272 +  show "carrier H \<subseteq> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
1.273 +  proof
1.274 +    fix y
1.275 +    assume y: "y \<in> carrier H"
1.276 +    with h obtain g where g: "g \<in> carrier G" "h g = y"
1.277 +      by (blast elim: equalityE);
1.278 +    hence "(\<Union>\<^bsub>x\<in>kernel G H h #> g\<^esub> {h x}) = {y}"
1.279 +      by (auto simp add: y kernel_def r_coset_def)
1.280 +    with g show "y \<in> (\<lambda>X. contents (h ` X)) ` carrier (G Mod kernel G H h)"
1.281 +      by (auto intro!: bexI simp add: FactGroup_def rcosets_def image_eq_UN)
1.282 +  qed
1.283 +qed
1.284 +
1.285 +
1.286 +text{*If @{term h} is a homomorphism from @{term G} onto @{term H}, then the
1.287 + quotient group @{term "G Mod (kernel G H h)"} is isomorphic to @{term H}.*}
1.288 +theorem (in group_hom) FactGroup_iso:
1.289 +  "h ` carrier G = carrier H
1.290 +   \<Longrightarrow> (%X. contents (h`X)) \<in> (G Mod (kernel G H h)) \<cong> H"
1.291 +by (simp add: iso_def FactGroup_hom FactGroup_inj_on bij_betw_def
1.292 +              FactGroup_onto)
1.293 +
1.294  end
```
```     2.1 --- a/src/HOL/Algebra/Group.thy	Mon May 24 18:35:34 2004 +0200
2.2 +++ b/src/HOL/Algebra/Group.thy	Wed May 26 11:43:50 2004 +0200
2.3 @@ -593,15 +593,15 @@
2.4
2.5  subsection {* Isomorphisms *}
2.6
2.7 -constdefs (structure G and H)
2.8 -  iso :: "_ => _ => ('a => 'b) set"
2.9 -  "iso G H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
2.10 +constdefs
2.11 +  iso :: "_ => _ => ('a => 'b) set"  (infixr "\<cong>" 60)
2.12 +  "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
2.13
2.14 -lemma iso_refl: "(%x. x) \<in> iso G G"
2.15 +lemma iso_refl: "(%x. x) \<in> G \<cong> G"
2.16  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
2.17
2.18  lemma (in group) iso_sym:
2.19 -     "h \<in> iso G H \<Longrightarrow> Inv (carrier G) h \<in> iso H G"
2.20 +     "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
2.21  apply (simp add: iso_def bij_betw_Inv)
2.22  apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
2.23   prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
2.24 @@ -609,15 +609,15 @@
2.25  done
2.26
2.27  lemma (in group) iso_trans:
2.28 -     "[|h \<in> iso G H; i \<in> iso H I|] ==> (compose (carrier G) i h) \<in> iso G I"
2.29 +     "[|h \<in> G \<cong> H; i \<in> H \<cong> I|] ==> (compose (carrier G) i h) \<in> G \<cong> I"
2.30  by (auto simp add: iso_def hom_compose bij_betw_compose)
2.31
2.32  lemma DirProdGroup_commute_iso:
2.33 -  shows "(%(x,y). (y,x)) \<in> iso (G \<times>\<^sub>g H) (H \<times>\<^sub>g G)"
2.34 +  shows "(%(x,y). (y,x)) \<in> (G \<times>\<^sub>g H) \<cong> (H \<times>\<^sub>g G)"
2.35  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
2.36
2.37  lemma DirProdGroup_assoc_iso:
2.38 -  shows "(%(x,y,z). (x,(y,z))) \<in> iso (G \<times>\<^sub>g H \<times>\<^sub>g I) (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
2.39 +  shows "(%(x,y,z). (x,(y,z))) \<in> (G \<times>\<^sub>g H \<times>\<^sub>g I) \<cong> (G \<times>\<^sub>g (H \<times>\<^sub>g I))"
2.40  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
2.41
2.42
```
```     3.1 --- a/src/HOL/Algebra/Sylow.thy	Mon May 24 18:35:34 2004 +0200
3.2 +++ b/src/HOL/Algebra/Sylow.thy	Wed May 26 11:43:50 2004 +0200
3.3 @@ -11,25 +11,6 @@
3.5  *}
3.6
3.7 -subsection {*Order of a Group and Lagrange's Theorem*}
3.8 -
3.9 -constdefs
3.10 -  order :: "('a, 'b) semigroup_scheme => nat"
3.11 -  "order S == card (carrier S)"
3.12 -
3.13 -theorem (in group) lagrange:
3.14 -     "[| finite(carrier G); subgroup H G |]
3.15 -      ==> card(rcosets G H) * card(H) = order(G)"
3.16 -apply (simp (no_asm_simp) add: order_def setrcos_part_G [symmetric])
3.17 -apply (subst mult_commute)
3.18 -apply (rule card_partition)
3.19 -   apply (simp add: setrcos_subset_PowG [THEN finite_subset])
3.20 -  apply (simp add: setrcos_part_G)
3.21 - apply (simp add: card_cosets_equal subgroup.subset)