1(* ------------------------------------------------------------------------- *) 2(* Group Theory -- Normal subgroup and Quotient Groups. *) 3(* ------------------------------------------------------------------------- *) 4 5(* 6 7Normal Subgroup 8=============== 9left Coset = right Coset 10 11Quotient Group 12============== 13G/N where N is a normal subgroup. 14 15*) 16 17(*===========================================================================*) 18 19(* add all dependent libraries for script *) 20open HolKernel boolLib bossLib Parse; 21 22(* declare new theory at start *) 23val _ = new_theory "quotientGroup"; 24 25(* ------------------------------------------------------------------------- *) 26 27 28 29(* val _ = load "jcLib"; *) 30open jcLib; 31 32(* open dependent theories *) 33open pred_setTheory; 34 35(* 36(* val _ = load "helperFunctionTheory"; *) 37open helperFunctionTheory; 38*) 39 40(* Get dependent theories local *) 41(* val _ = load "monoidOrderTheory"; *) 42open monoidTheory monoidOrderTheory; 43 44(* val _ = load "subgroupTheory"; *) 45open groupTheory subgroupTheory; 46open monoidMapTheory groupMapTheory; 47 48(* Get dependent theories in lib *) 49(* (* val _ = load "helperSetTheory"; loaded by monoidTheory *) *) 50open helperSetTheory; 51 52 53(* ------------------------------------------------------------------------- *) 54(* Quotient Group Documentation *) 55(* ------------------------------------------------------------------------- *) 56(* Overloads: 57 x / y = group_div g x y 58 h << g = normal_subgroup h g 59 h == g = group_equiv g h 60 x o y = coset_op g h x y 61 g / h = quotient_group g h 62*) 63(* Definitions and Theorems (# are exported): 64 65 Group element division: 66# group_div_def |- !g x y. x / y = x * |/ y 67# group_div_element |- !g. Group g ==> !x y. x IN G /\ y IN G ==> x / y IN G 68# group_div_cancel |- !g. Group g ==> !x. x IN G ==> (x / x = #e) 69 group_div_pair |- !g. Group g ==> !x1 y1 x2 y2. x1 IN G /\ y1 IN G /\ x2 IN G /\ y2 IN G ==> 70 (x1 * y1 / (x2 * y2) = x1 * (y1 / y2) / x1 * (x1 / x2)) 71 group_div_lsame |- !g. Group g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> (z * x / (z * y) = z * (x / y) / z) 72 group_div_rsame |- !g. Group g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> (x * z / (y * z) = x / y) 73 74 Normal Subgroup: 75 normal_subgroup_def |- !h g. h << g <=> h <= g /\ !a z. a IN G /\ z IN H ==> a * z / a IN H 76 normal_subgroup_subgroup |- !h g. h << g ==> h <= g 77 normal_subgroup_property |- !h g. h << g ==> !a z. a IN G /\ z IN H ==> a * z / a IN H 78 normal_subgroup_groups |- !g h. h << g ==> h <= g /\ Group h /\ Group g 79 normal_subgroup_refl |- !g. Group g ==> g << g 80 normal_subgroup_antisym |- !g h. h << g /\ g << h ==> (h = g) 81 normal_subgroup_alt |- !g h. h << g <=> h <= g /\ !a. a IN G ==> (a * H = H * a) 82 normal_subgroup_coset_eq |- !g h. h << g ==> !x y. x IN G /\ y IN G ==> ((x * H = y * H) <=> x / y IN H) 83 84 Equivalence induced by Normal Subgroup: 85 group_equiv_def |- !g h x y. x == y <=> x / y IN H 86 group_normal_equiv_reflexive |- !g h. h << g ==> !z. z IN G ==> z == z 87 group_normal_equiv_symmetric |- !g h. h << g ==> !x y. x IN G /\ y IN G ==> (x == y <=> y == x) 88 group_normal_equiv_transitive |- !g h. h << g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> x == y /\ y == z ==> x == z 89 group_normal_equiv |- !g h. h << g ==> $== equiv_on G 90 group_normal_equiv_property |- !h g. h << g ==> !x y. x IN G /\ y IN G ==> (x == y <=> x IN y * H) 91 92 Binary operation for cosets: 93 cogen_def |- !g h e. h <= g /\ e IN CosetPartition g h ==> cogen g h e IN G /\ (e = cogen g h e * H) 94 cogen_element |- !h g e. h <= g /\ e IN CosetPartition g h ==> cogen g h e IN G 95 coset_cogen_property |- !h g e. h <= g /\ e IN CosetPartition g h ==> (e = cogen g h e * H) 96 coset_op_def |- !g h x y. x o y = cogen g h x * cogen g h y * H 97 cogen_of_subgroup |- !g h. h <= g ==> (cogen g h H * H = H 98 cogen_coset_element |- !g h. h <= g ==> !x. x IN G ==> cogen g h (x * H) IN G 99 normal_cogen_property |- !g h. h << g ==> !x. x IN G ==> x / cogen g h (x * H) IN H 100 normal_coset_property1 |- !g h. h << g ==> !a b. a IN G /\ b IN G ==> (cogen g h (a * H) * b * H = a * b * H) 101 normal_coset_property2 |- !g h. h << g ==> !a b. a IN G /\ b IN G ==> (a * cogen g h (b * H) * H = a * b * H) 102 normal_coset_property |- !g h. h << g ==> !a b. a IN G /\ b IN G ==> (cogen g h (a * H) * cogen g h (b * H) * H = a * b * H) 103 104 Quotient Group: 105 quotient_group_def |- !g h. g / h = <|carrier := CosetPartition g h; op := $o; id := H|> 106 quotient_group_closure |- !g h. h <= g ==> 107 !x y. x IN CosetPartition g h /\ y IN CosetPartition g h ==> x o y IN CosetPartition g h 108 quotient_group_assoc |- !g h. h << g ==> 109 !x y z. x IN CosetPartition g h /\ y IN CosetPartition g h /\ z IN CosetPartition g h ==> ((x o y) o z = x o y o z) 110 quotient_group_id |- !g h. h << g ==> H IN CosetPartition g h /\ !x. x IN CosetPartition g h ==> (H o x = x) 111 quotient_group_inv |- !g h. h << g ==> !x. x IN CosetPartition g h ==> ?y. y IN CosetPartition g h /\ (y o x = H) 112 quotient_group_group |- !g h. h << g ==> Group (g / h) 113 114 Group Homomorphism by left_coset via normal subgroup: 115 normal_subgroup_coset_homo |- !g h. h << g ==> GroupHomo (left_coset g H) g (g / h) 116 normal_coset_op_property |- !g h. h << g ==> !x y. x IN CosetPartition g h /\ y IN CosetPartition g h ==> 117 (x o y = CHOICE (preimage (left_coset g H) G x) * CHOICE (preimage (left_coset g H) G y) * H) 118 coset_homo_group_iso_quotient_group |- !g h. h << g ==> GroupIso I (homo_group g (left_coset g H)) (g / h) 119 120 Kernel Group of Group Homomorphism: 121 kernel_def |- !f g h. kernel f g h = preimage f G h.id 122 kernel_group_def |- !f g h. kernel_group f g h = <|carrier := kernel f g h; id := #e; op := $* |> 123# kernel_property |- !g h f x. x IN kernel f g h <=> x IN G /\ (f x = h.id) 124 kernel_element |- !g h f x. x IN kernel f g h <=> x IN G /\ (f x = h.id) 125 kernel_group_group |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> Group (kernel_group f g h) 126 kernel_group_subgroup |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> kernel_group f g h <= g 127 kernel_group_normal |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> kernel_group f g h << g 128 kernel_quotient_group |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> Group (g / kernel_group f g h) 129 130 Homomorphic Image and Kernel: 131 homo_image_def |- !f g h. homo_image f g h = <|carrier := IMAGE f G; op := h.op; id := h.id|> 132 homo_image_monoid |- !g h f. Monoid g /\ Monoid h /\ MonoidHomo f g h ==> Monoid (homo_image f g h) 133 homo_image_group |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> Group (homo_image f g h) 134 homo_image_subgroup |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> homo_image f g h <= h 135 group_homo_image_surj_property |- !g h f. Group g /\ Group h /\ 136 SURJ f G h.carrier ==> GroupIso I h (homo_image f g h) 137 monoid_homo_homo_image_monoid |- !g h f. Monoid g /\ MonoidHomo f g h ==> Monoid (homo_image f g h) 138 group_homo_homo_image_group |- !g h f. Group g /\ MonoidHomo f g h ==> Group (homo_image f g h) 139 140 First Isomorphic Theorem for Group: 141 homo_image_homo_quotient_kernel |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> 142 GroupHomo (\z. CHOICE (preimage f G z) * kernel f g h) (homo_image f g h) (g / kernel_group f g h) 143 homo_image_to_quotient_kernel_bij |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> 144 BIJ (\z. CHOICE (preimage f G z) * kernel f g h) (homo_image f g h).carrier (g / kernel_group f g h).carrier 145 homo_image_iso_quotient_kernel |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> 146 GroupIso (\z. CHOICE (preimage f G z) * kernel f g h) (homo_image f g h) (g / kernel_group f g h) 147 group_first_isomorphism_thm |- !g h f. Group g /\ Group h /\ GroupHomo f g h ==> 148 kernel_group f g h << g /\ homo_image f g h <= h /\ 149 GroupIso (\z. CHOICE (preimage f G z) * kernel f g h) (homo_image f g h) (g / kernel_group f g h) /\ 150 (SURJ f G h.carrier ==> GroupIso I h (homo_image f g h)) 151*) 152 153(* ------------------------------------------------------------------------- *) 154(* Group element division. *) 155(* ------------------------------------------------------------------------- *) 156(* Define group division *) 157val group_div_def = Define ` 158 group_div (g:'a group) (x:'a) (y:'a) = x * |/ y 159`; 160 161(* set overloading *) 162val _ = overload_on ("/", ``group_div g``); 163val _ = set_fixity "/" (Infixl 600); (* same as "*" in arithmeticScript.sml *) 164 165(* export simple defintion *) 166val _ = export_rewrites ["group_div_def"]; 167 168(* Theorem: x / y IN G *) 169(* Proof: 170 x / y = x * |/y by group_div_def 171 and |/y IN G by group_inv_element 172 hence true by group_op_element 173*) 174val group_div_element = store_thm( 175 "group_div_element", 176 ``!g:'a group. Group g ==> !x y. x IN G /\ y IN G ==> x / y IN G``, 177 rw[group_div_def]); 178 179val _ = export_rewrites ["group_div_element"]; 180 181(* Theorem: x / x = #e *) 182(* Proof: 183 x / x = x * |/x by group_div_def 184 = #e by group_rinv 185*) 186val group_div_cancel = store_thm( 187 "group_div_cancel", 188 ``!g:'a group. Group g ==> !x. x IN G ==> (x / x = #e)``, 189 rw[group_div_def]); 190 191val _ = export_rewrites ["group_div_cancel"]; 192 193(* Theorem: (x1 * y1) / (x2 * y2) = x1 * (y1 / y2) / x1 * (x1 / x2) *) 194(* Proof: 195 (x1 * y1) / (x2 * y2) 196 = (x1 * y1) * |/ (x2 * y2) by group_div_def 197 = (x1 * y1) * ( |/ y2 * |/ x2) by group_inv_op 198 = x1 * (y1 * ( |/ y2 * |/ x2)) by group_assoc 199 = x1 * (y1 * |/ y2 * |/ x2) by group_assoc 200 = x1 * (y1 * |/ y2 * ( |/ x1 * x1 * |/ x2)) by group_linv, group_lid 201 = x1 * (y1 * |/ y2 * ( |/ x1 * (x1 * |/ x2))) by group_assoc 202 = x1 * (y1 / y2) * |/ x1 * (x1 / x2) by group_assoc 203 = x1 * (y1 / y2) / x1 * (x1 / x2) by group_div_def 204*) 205val group_div_pair = store_thm( 206 "group_div_pair", 207 ``!g:'a group. Group g ==> !x1 y1 x2 y2. x1 IN G /\ y1 IN G /\ x2 IN G /\ y2 IN G ==> 208 ((x1 * y1) / (x2 * y2) = (x1 * (y1 / y2) / x1) * (x1 / x2))``, 209 rw_tac std_ss[group_div_def] >> 210 `|/ x1 IN G /\ |/ y1 IN G /\ |/ x2 IN G /\ |/ y2 IN G` by rw[group_assoc] >> 211 `(x1 * y1) * |/ (x2 * y2) = x1 * y1 * ( |/ y2 * |/ x2)` by rw[group_inv_op] >> 212 `_ = x1 * (y1 * |/ y2 * |/ x2)` by rw[group_assoc] >> 213 `_ = x1 * (y1 * |/ y2 * ( |/ x1 * x1 * |/ x2))` by rw_tac std_ss[group_linv, group_lid] >> 214 `_ = (x1 * (y1 * |/ y2) * |/ x1) * (x1 * |/ x2)` by rw[group_assoc] >> 215 rw_tac std_ss[]); 216 217(* Theorem: (z * x) / (z * y) = z * (x / y) / z *) 218(* Proof: 219 (z * x) / (z * y) 220 = z * (x / y) / z * (z / z) by group_div_pair 221 = z * (x / y) / z * #e by group_div_cancel 222 = z * (x / y) / z by group_rid 223*) 224val group_div_lsame = store_thm( 225 "group_div_lsame", 226 ``!g:'a group. Group g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> ((z * x) / (z * y) = z * (x / y) / z)``, 227 rw[group_assoc, group_div_pair]); 228 229(* Theorem: (x * z) / (y * z) = x / y *) 230(* Proof: 231 (x * z) / (y * z) 232 = x * (z / z) / x * (x / y) by group_div_pair 233 = x * #e / x * (x / y) by group_div_cancel 234 = x / x * (x / y) by group_rid 235 = #e * (x / y) by group_div_cancel 236 = x / y by group_lid 237*) 238val group_div_rsame = store_thm( 239 "group_div_rsame", 240 ``!g:'a group. Group g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> ((x * z) / (y * z) = x / y)``, 241 rw[group_assoc, group_div_pair]); 242 243(* ------------------------------------------------------------------------- *) 244(* Normal Subgroup *) 245(* ------------------------------------------------------------------------- *) 246 247(* A Normal Subgroup: for all x IN H, for all a IN G, a * x / a IN H 248 i.e. A subgroup, H, of a group, G, is called a normal subgroup if it is invariant under conjugation. *) 249val normal_subgroup_def = Define ` 250 normal_subgroup (h:'a group) (g:'a group) <=> 251 h <= g /\ (!a z. a IN G /\ z IN H ==> a * z / a IN H) 252`; 253 254(* set overloading *) 255val _ = overload_on ("<<", ``normal_subgroup``); 256val _ = set_fixity "<<" (Infixl 650); (* higher than * or / *) 257 258(* Theorem: Normal subgroup is a subgroup. *) 259val normal_subgroup_subgroup = save_thm("normal_subgroup_subgroup", 260 normal_subgroup_def |> SPEC_ALL |> #1 o EQ_IMP_RULE |> UNDISCH_ALL |> CONJUNCT1 |> DISCH_ALL |> GEN_ALL); 261(* > val normal_subgroup_subgroup = |- !h g. h << g ==> h <= g : thm *) 262 263(* Theorem: Normal subgroup is invariant under conjugation. *) 264val normal_subgroup_property = save_thm("normal_subgroup_property", 265 normal_subgroup_def |> SPEC_ALL |> #1 o EQ_IMP_RULE |> UNDISCH_ALL |> CONJUNCT2 |> DISCH_ALL |> GEN_ALL); 266(* > val normal_subgroup_property = |- !h g. h << g ==> !a z. a IN G /\ z IN H ==> a * z / a IN H : thm *) 267 268(* Theorem: h << g ==> h <= g /\ Group h /\ Group g *) 269(* Proof: by normal_subgroup_def and subgroup_property. *) 270val normal_subgroup_groups = store_thm( 271 "normal_subgroup_groups", 272 ``!g h:'a group. h << g ==> h <= g /\ Group h /\ Group g``, 273 metis_tac[normal_subgroup_def, subgroup_property]); 274 275(* Theorem: g << g *) 276(* Proof: by definition, this is to show: 277 g <= g, 278 True by subgroup_refl 279*) 280val normal_subgroup_refl = store_thm( 281 "normal_subgroup_refl", 282 ``!g:'a group. Group g ==> g << g``, 283 rw[normal_subgroup_def, subgroup_refl]); 284 285(* Theorem: h << g /\ g << h ==> h = g *) 286(* Proof: by definition, this is to show: 287 h <= g /\ g <= h ==> h = g, 288 True by subgroup_antisym. 289*) 290val normal_subgroup_antisym = store_thm( 291 "normal_subgroup_antisym", 292 ``!(g:'a group) (h:'a group). h << g /\ g << h ==> (h = g)``, 293 rw[normal_subgroup_def, subgroup_antisym]); 294 295(* Note: Subgroup normality is not transitive: 296see: http://groupprops.subwiki.org/wiki/Normality_is_not_transitive 297 298D4 = <a, x | a^4 = x^2 = e, x a x = |/a > 299Let H1 = <x>, H2 = <a^2 x>, K = <x, a^2> 300Then H1 << K, H2 << K, K << D4, but neither H1 << D4 nor H2 << D4. 301 302i.e. <s> << <r^2, s> << <r, s>=D4, but <s> is not normal in D4. 303 304or 305In S4 and its following subgroup A={(12)(34)} and B={(12)(34),(13)(42),(23)(41),e} 306Try to show A is normal in B and B is normal in S4 but A is not normal in G. 307 308*) 309 310(* Property of Normal Subgroup: a subgroup with left coset = right coset. *) 311(* Theorem: h << g <=> h <= g /\ aH = Ha for all a in G. *) 312(* Proof: 313 If-part: 314 h << g ==> !a. a IN G ==> (IMAGE (\z. z * a) H = IMAGE (\z. a * z) H) 315 This essentially boils down to 2 cases: 316 case 1. h <= g /\ a IN G /\ z IN H ==> ?z'. (z * a = a * z') /\ z' IN H 317 By group property, z' = |/a * z * a, need to show that z' IN H 318 This is because, a IN G ==> |/a IN G, 319 hence |/a * z * |/( |/ a) IN H by by conjugate property 320 or |/a * z * a IN H by group_inv_inv 321 case 2. h <= g /\ a IN G /\ z IN H ==> ?z'. (a * z = z' * a) /\ z' IN H 322 By group property, z' = a * z / a, need to show z' IN H 323 This is because a IN G, hence true by conjugate property. 324 Only-if part: 325 h <= g /\ !a. a IN G ==> (IMAGE (\z. z * a) H = IMAGE (\z. a * z) H) ==> a * z * |/ a IN H 326 Since a * z IN right image, there is z' such that z' * a = a * z and z' IN H 327 i.e. z' = a * z * |/a IN H, 328 = a * z / a IN H. 329*) 330val normal_subgroup_alt = store_thm( 331 "normal_subgroup_alt", 332 ``!g h:'a group. h << g <=> h <= g /\ (!a. a IN G ==> (a * H = H * a))``, 333 rw_tac std_ss[normal_subgroup_def, coset_def, right_coset_def, EQ_IMP_THM] >| [ 334 rw[EXTENSION] >> 335 `Group h /\ Group g` by metis_tac[subgroup_property] >> 336 `|/a IN G` by rw[] >> 337 rw_tac std_ss[EQ_IMP_THM] >| [ 338 qexists_tac `a * z / a` >> 339 `z IN G` by metis_tac[subgroup_element] >> 340 rw[group_rinv_assoc], 341 qexists_tac `|/a * z * a` >> 342 `z IN G` by metis_tac[subgroup_element] >> 343 rw[group_assoc, group_linv_assoc] >> 344 `|/ a * (z * a) = |/a * z * a` by rw[group_assoc] >> 345 metis_tac[group_inv_inv, group_div_def] 346 ], 347 full_simp_tac std_ss [IMAGE_DEF, EXTENSION, GSPECIFICATION] >> 348 `?z'. (a * z = z' * a) /\ z' IN H` by metis_tac[] >> 349 metis_tac[group_rinv_assoc, group_div_def, Subgroup_def, SUBSET_DEF] 350 ]); 351 352(* Theorem: x * H = y * H ==> x / y IN H if H is a normal subgroup *) 353(* Proof: 354 By subgroup_coset_eq, |/y * x IN H 355 i.e. y * ( |/y * x) * |/ y IN H by normal_subgroup_property 356 or x * |/ y IN H by group_assoc, group_rinv, group_lid 357 or x / y IN H by group_div_def 358*) 359val normal_subgroup_coset_eq = store_thm( 360 "normal_subgroup_coset_eq", 361 ``!g h:'a group. h << g ==> !x y. x IN G /\ y IN G ==> ((x * H = y * H) <=> x / y IN H)``, 362 rw_tac std_ss[normal_subgroup_def, group_div_def] >> 363 `|/y * x IN H <=> x * |/ y IN H` suffices_by rw_tac std_ss[subgroup_coset_eq] >> 364 `Group h /\ Group g` by metis_tac[subgroup_property] >> 365 `y * ( |/y * x) * |/ y = y * |/y * x * |/ y` by rw[group_assoc] >> 366 `_ = x * |/ y` by rw_tac std_ss[group_rinv, group_lid] >> 367 `|/ x * (x * |/ y) * x = |/ x * x * |/ y * x` by rw[group_assoc] >> 368 `_ = |/ y * x` by rw_tac std_ss[group_linv, group_lid, group_inv_element] >> 369 metis_tac[group_inv_element, group_inv_inv]); 370 371(* ------------------------------------------------------------------------- *) 372(* Equivalence induced by Normal Subgroup *) 373(* ------------------------------------------------------------------------- *) 374 375(* Two group elements x y are equivalent if x / y = x * |/y in normal subgroup. *) 376 377(* Define group element equivalence by normal subgroup. *) 378val group_equiv_def = Define ` 379 group_equiv (g:'a group) (h:'a group) x y <=> x / y IN H 380`; 381 382(* set overloading *) 383val _ = overload_on ("==", ``group_equiv g h``); 384val _ = set_fixity "==" (Infix(NONASSOC, 450)); 385 386(* Theorem: [== is reflexive] h << g ==> z == z for z IN G. *) 387(* Proof: 388 z == z iff z / z IN H by group_equiv_def 389 iff z * |/z = #e IN H by group_div_def, group_rinv 390 which is true since h <= g, and Group h. 391 or: since h << g, h.id = #e by subgroup_id 392 hence z * |/z = z * #e * |/z IN H by normal_subgroup_property. 393*) 394val group_normal_equiv_reflexive = store_thm( 395 "group_normal_equiv_reflexive", 396 ``!g h:'a group. h << g ==> !z. z IN G ==> z == z``, 397 rw_tac std_ss[normal_subgroup_def, group_equiv_def, group_div_def] >> 398 metis_tac[group_id_element, subgroup_id, group_rid, Subgroup_def]); 399 400(* Theorem: [== is symmetric] h << g ==> x == y <=> y == x for x, y IN G. *) 401(* Proof: 402 x == y iff x / y IN H by group_equiv_def 403 iff x * |/ y IN H by group_div_def 404 iff |/ (x * |/ y) IN H by group_inv_element 405 iff y * |/ x IN H by group_inv_op, group_inv_inv 406 if y / x IN H by group_div_def 407 iff y == x by group_equiv_def 408*) 409val group_normal_equiv_symmetric = store_thm( 410 "group_normal_equiv_symmetric", 411 ``!g h:'a group. h << g ==> !x y. x IN G /\ y IN G ==> (x == y <=> y == x)``, 412 rw_tac std_ss[normal_subgroup_def, group_equiv_def, group_div_def] >> 413 `Group h /\ Group g` by metis_tac[Subgroup_def] >> 414 `|/ ( x * |/ y) = y * |/ x` by rw[group_inv_inv, group_inv_op] >> 415 `|/ ( y * |/ x) = x * |/ y` by rw[group_inv_inv, group_inv_op] >> 416 metis_tac[group_inv_element, subgroup_inv]); 417 418(* Theorem: [== is transitive] h << g ==> x == y /\ y == z ==> x == z for x, y, z IN G. *) 419(* Proof: 420 x == y iff x * |/ y IN H by group_equiv_def, group_div_def 421 y == z iff y * |/ z IN H by by group_equiv_def, group_div_def 422 Together, 423 (x * |/ y) * (y * |/ z) IN H by group_op_element 424 or x * |/ z IN H by group_assoc, group_linv 425 i..e. x == z by by group_equiv_def, group_div_def 426*) 427val group_normal_equiv_transitive = store_thm( 428 "group_normal_equiv_transitive", 429 ``!g h:'a group. h << g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> (x == y /\ y == z ==> x == z)``, 430 rw_tac std_ss[normal_subgroup_def, group_equiv_def, group_div_def] >> 431 `Group h /\ Group g` by metis_tac[Subgroup_def] >> 432 `(x * |/ y) * (y * |/ z) = (x * |/ y) * y * |/ z` by rw[group_assoc] >> 433 `_ = x * |/ z` by rw_tac std_ss[group_linv, group_rid, group_assoc, group_inv_element] >> 434 metis_tac[group_op_element, subgroup_property]); 435 436(* Theorem: [== is an equivalence relation] h << g ==> $== equiv_on G. *) 437(* Proof: by group_normal_equiv_reflexive, group_normal_equiv_symmetric, group_normal_equiv_transitive. *) 438val group_normal_equiv = store_thm( 439 "group_normal_equiv", 440 ``!g h:'a group. h << g ==> $== equiv_on G``, 441 rw_tac std_ss[equiv_on_def] >| [ 442 rw_tac std_ss[group_normal_equiv_reflexive], 443 rw_tac std_ss[group_normal_equiv_symmetric], 444 metis_tac[group_normal_equiv_transitive] 445 ]); 446 447(* ------------------------------------------------------------------------- *) 448(* Normal Equivalence Classes are Cosets of Normal Subgroup. *) 449(* ------------------------------------------------------------------------- *) 450 451(* Theorem: for x, y in G, x == y iff x IN y * H, the coset of y with normal subgroup. *) 452(* Proof: 453 x == y iff x / y IN H by group_equiv_def 454 iff x * |/ y IN H by group_div_def 455 iff x * |/ y = z, where z IN H 456 iff x = z * y 457 iff x IN IMAGE (\z. z * y) H by IMAGE definition 458 iff x IN IMAGE (\z. y * z) H by normal_subgroup_alt 459 iff x IN yH by coset definition 460*) 461val group_normal_equiv_property = store_thm( 462 "group_normal_equiv_property", 463 ``!h g:'a group. h << g ==> !x y. x IN G /\ y IN G ==> (x == y <=> x IN y * H)``, 464 rw_tac std_ss[group_equiv_def] >> 465 `x / y IN H <=> x IN H * y` suffices_by metis_tac[normal_subgroup_alt] >> 466 rw_tac std_ss[group_div_def, right_coset_def, IN_IMAGE] >> 467 `x * |/ y IN H <=> ?z. z IN H /\ (z = x * |/ y)` by rw_tac std_ss[] >> 468 metis_tac[group_lsolve, normal_subgroup_subgroup, Subgroup_def, SUBSET_DEF]); 469 470(* ------------------------------------------------------------------------- *) 471(* The map to set of costes and the induced binary operation. *) 472(* Aim: coset g H is a homomorphism: G -> Group of {a * H | a IN G} *) 473(* ------------------------------------------------------------------------- *) 474 475(* from subgroupTheory: 476 477- inCoset_def; 478> val it = |- !g h a b. inCoset g h a b <=> b IN a * H : thm 479 480- inCoset_equiv_on_carrier; 481> val it = |- !g h. h <= g ==> inCoset g h equiv_on G : thm 482 483- CosetPartition_def; 484> val it = |- !g h. CosetPartition g h = partition (inCoset g h) G : thm 485 486- coset_partition_element; 487> val it = |- !g h. h <= g ==> !e. e IN CosetPartition g h ==> ?a. a IN G /\ (e = a * H) : thm 488 489- GroupHomo_def; 490> val it = |- !f g h. GroupHomo f g h <=> (!x. x IN G ==> f x IN H) /\ 491 !x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y)) : thm 492- type_of ``a * H``; 493> val it = ``:'a -> bool`` : hol_type 494 495*) 496 497(* Existence of coset generator: e IN CosetPartition g h ==> ?a. a IN G /\ (e = a * H) *) 498val lemma = prove( 499 ``!g h e. ?a. h <= g /\ e IN CosetPartition g h ==> a IN G /\ (e = a * H)``, 500 metis_tac[coset_partition_element]); 501(* 502- SKOLEM_THM; 503> val it = |- !P. (!x. ?y. P x y) <=> ?f. !x. P x (f x) : thm 504*) 505(* Define coset generator *) 506val cogen_def = new_specification( 507 "cogen_def", 508 ["cogen"], 509 SIMP_RULE (srw_ss()) [SKOLEM_THM] lemma); 510(* > val cogen_def = |- !g h e. h <= g /\ e IN CosetPartition g h ==> cogen g h e IN G /\ (e = (cogen g h e) * H) : thm *) 511 512(* Theorem: h <= g /\ e IN CosetPartition g h ==> cogen g h e IN G *) 513val cogen_element = save_thm("cogen_element", 514 cogen_def |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT1 |> DISCH_ALL |> GEN_ALL); 515(* > val cogen_element = |- !h g e. h <= g /\ e IN CosetPartition g h ==> cogen g h e IN G : thm *) 516 517(* Theorem: h <= g /\ e IN CosetPartition g h ==> (cogen g h e) * H = e *) 518val coset_cogen_property = save_thm("coset_cogen_property", 519 cogen_def |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT2 |> DISCH_ALL |> GEN_ALL); 520(* > val coset_cogen_property = |- !h g e. h <= g /\ e IN CosetPartition g h ==> (e = (cogen g h e) * H) : thm *) 521 522(* Define coset multiplication *) 523val coset_op_def = Define ` 524 coset_op (g:'a group) (h:'a group) (x:'a -> bool) (y:'a -> bool) = ((cogen g h x) * (cogen g h y)) * H 525`; 526 527(* set overloading *) 528val _ = overload_on ("o", ``coset_op g h``); 529 530(* Theorem: h <= g ==> cogen g h H * H = H *) 531(* Proof: 532 Since H = #e * H by coset_id_eq_subgroup 533 H IN CosetPartition g h by coset_partition_element 534 hence cogen g h H * H = H by cogen_def 535*) 536val cogen_of_subgroup = store_thm( 537 "cogen_of_subgroup", 538 ``!g h:'a group. h <= g ==> (cogen g h H * H = H)``, 539 rpt strip_tac >> 540 `#e * H = H` by rw_tac std_ss[coset_id_eq_subgroup] >> 541 `Group g` by metis_tac[Subgroup_def] >> 542 `H IN CosetPartition g h` by metis_tac[coset_partition_element, group_id_element] >> 543 rw_tac std_ss[cogen_def]); 544 545(* Theorem: h <= g ==> !x. x IN G ==> cogen g h (x * H) IN G *) 546(* Proof: 547 Since x * H IN CosetPartition g h by coset_partition_element 548 cogen g h (x * H) IN G by cogen_def 549*) 550val cogen_coset_element = store_thm( 551 "cogen_coset_element", 552 ``!g h:'a group. h <= g ==> !x. x IN G ==> cogen g h (x * H) IN G``, 553 metis_tac[cogen_def, coset_partition_element]); 554 555(* Theorem: x / cogen g h (x * H) IN H if H is a normal subgroup. *) 556(* Proof: 557 Since x * H IN CosetPartition g h by coset_partition_element 558 cogen g h (x * H) IN G /\ 559 ((cogen g h (x * H)) * H = x * H) by cogen_def 560 hence x / cogen g h (x * H) IN H by normal_subgroup_coset_eq 561*) 562val normal_cogen_property = store_thm( 563 "normal_cogen_property", 564 ``!g h:'a group. h << g ==> !x. x IN G ==> x / cogen g h (x * H) IN H``, 565 rpt strip_tac >> 566 `h <= g` by rw_tac std_ss[normal_subgroup_subgroup] >> 567 `x * H IN CosetPartition g h` by metis_tac[coset_partition_element] >> 568 `cogen g h (x * H) IN G /\ ((cogen g h (x * H)) * H = x * H)` by rw_tac std_ss[cogen_def] >> 569 metis_tac[normal_subgroup_coset_eq]); 570 571(* Theorem: h << g ==> cogen g h (a * H) * b * H = a * b * H *) 572(* Proof: 573 By normal_subgroup_coset_eq, and reversing the equality, 574 this is to show: (a * b) / (cogen g h (a * H) * b) IN H 575 but (a * b) / (cogen g h (a * H) * b) = a / cogen g h (a * H) by group_div_rsame 576 and a / cogen g h (a * H) IN H by normal_cogen_property. 577*) 578val normal_coset_property1 = store_thm( 579 "normal_coset_property1", 580 ``!g h:'a group. h << g ==> !a b. a IN G /\ b IN G ==> (cogen g h (a * H) * b * H = a * b * H)``, 581 rpt strip_tac >> 582 `h <= g /\ Group g` by metis_tac[normal_subgroup_groups] >> 583 `cogen g h (a * H) IN G` by rw_tac std_ss[cogen_coset_element] >> 584 `a / cogen g h (a * H) IN H` by rw_tac std_ss[normal_cogen_property] >> 585 `(a * b) / (cogen g h (a * H) * b) = a / cogen g h (a * H)` by rw_tac std_ss[group_div_rsame] >> 586 metis_tac[normal_subgroup_coset_eq, group_op_element]); 587 588(* Theorem: h << g ==> a * cogen g h (b * H) * H = a * b * H *) 589(* Proof: 590 By normal_subgroup_coset_eq, and reversing the equality, 591 this is to show: (a * b) / (a * cogen g h (b * H)) IN H 592 but (a * b) / (a * cogen g h (b * H)) = a * (b / cogen g h (b * H)) / a by group_div_lsame 593 and b / cogen g h (b * H) IN H by normal_cogen_property 594 hence a * b / cogen g h (b * H) / a IN H by normal_subgroup_property 595*) 596val normal_coset_property2 = store_thm( 597 "normal_coset_property2", 598 ``!g h:'a group. h << g ==> !a b. a IN G /\ b IN G ==> (a * cogen g h (b * H) * H = a * b * H)``, 599 rpt strip_tac >> 600 `h <= g /\ Group g` by metis_tac[normal_subgroup_groups] >> 601 `cogen g h (b * H) IN G` by rw_tac std_ss[cogen_coset_element] >> 602 `b / cogen g h (b * H) IN H` by rw_tac std_ss[normal_cogen_property] >> 603 `a * b / (a * cogen g h (b * H)) = a * (b / cogen g h (b * H)) / a` by rw_tac std_ss[group_div_lsame] >> 604 `a * b / (a * cogen g h (b * H)) IN H` by rw_tac std_ss[normal_subgroup_property] >> 605 metis_tac[normal_subgroup_coset_eq, group_op_element]); 606 607(* Theorem: h << g ==> !a b. a IN G /\ b IN G ==> (cogen g h (a * H) * cogen g h (b * H) * H = a * b * H) *) 608(* Proof: 609 h << g ==> h <= g by normal_subgroup_subgroup 610 a IN G ==> cogen g h (a * H) IN G by cogen_coset_element, h <= g 611 b IN G ==> cogen g h (b * H) IN G by cogen_coset_element, h <= g 612 cogen g h (a * H) * cogen g h (b * H) * H 613 = a * cogen g h (b * H) * H by normal_coset_property1, h << g 614 = a * b * H by normal_coset_property2, h << g 615*) 616val normal_coset_property = store_thm( 617 "normal_coset_property", 618 ``!g h:'a group. h << g ==> !a b. a IN G /\ b IN G ==> (cogen g h (a * H) * cogen g h (b * H) * H = a * b * H)``, 619 rw_tac std_ss[normal_subgroup_subgroup, cogen_coset_element, normal_coset_property1, normal_coset_property2]); 620 621(* ------------------------------------------------------------------------- *) 622(* Quotient Group *) 623(* ------------------------------------------------------------------------- *) 624(* Define the quotient group, the group divided by a normal subgroup. *) 625val quotient_group_def = Define` 626 quotient_group (g:'a group) (h:'a group) = 627 <| carrier := (CosetPartition g h); 628 op := coset_op g h; 629 id := H 630 |> 631`; 632 633(* set overloading *) 634val _ = overload_on ("/", ``quotient_group``); 635val _ = set_fixity "/" (Infixl 600); (* same as "*" in arithmeticScript.sml *) 636 637(* 638- type_of ``(g:'a group) / (h:'a group)``; 639> val it = ``:('a -> bool) group`` : hol_type 640- type_of ``coset g H``; 641> val it = ``:'a -> 'a -> bool`` : hol_type 642*) 643 644(* Theorem: [Quotient Group Closure] 645 h << g ==> x IN CosetPartition g h /\ y IN CosetPartition g h ==> x o y IN CosetPartition g h *) 646(* Proof: 647 x o y = cogen g h x * cogen g h y * H by coset_op_def 648 Since cogen g h x IN G by cogen_def 649 and cogen g h y IN G by cogen_def 650 hence cogen g h x * cogen g h y IN G by group_op_element 651 or (cogen g h x * cogen g h y IN G) * H IN CosetPartition g h by coset_partition_element. 652 653*) 654val quotient_group_closure = store_thm( 655 "quotient_group_closure", 656 ``!g h:'a group. h <= g ==> !x y. x IN CosetPartition g h /\ y IN CosetPartition g h ==> x o y IN CosetPartition g h``, 657 rw_tac std_ss[coset_op_def] >> 658 `cogen g h x IN G /\ cogen g h y IN G` by rw_tac std_ss[cogen_def] >> 659 metis_tac[group_op_element, coset_partition_element, Subgroup_def]); 660 661(* Theorem: [Quotient Group Associativity] 662 h << g ==> x IN CosetPartition g h /\ y IN CosetPartition g h /\ z IN CosetPartition g h ==> (x o y) o z = x o (y o z) *) 663(* Proof: 664 By coset_op_def, 665 (x o y) o z 666 = cogen g h (cogen g h x * cogen g h y * H) * cogen g h z * H by coset_op_def 667 = ((cogen g h x * cogen g h y) * cogen g h z) * H by normal_coset_property1 668 = (cogen g h x * (cogen g h y * cogen g h z)) * H by group_assoc 669 = cogen g h x * cogen g h (cogen g h y * cogen g h z * H) * H by normal_coset_property2 670 = x o (y o z) by coset_op_def 671 672 Since cogen g h x IN G by cogen_def 673 and cogen g h y IN G by cogen_def 674 and cogen g h z IN G by cogen_def 675 Let t = cogen g h x * cogen g h y IN G 676 t * H IN CosetPartition g h 677 cogen g h (t * H) IN G /\ (cogen g h (t * H)) * H = t * H 678 For h << g, this implies t / cogen g h (t * H) IN H by normal_cogen_property 679 680*) 681val quotient_group_assoc = store_thm( 682 "quotient_group_assoc", 683 ``!g h:'a group. h << g ==> !x y z. x IN CosetPartition g h /\ y IN CosetPartition g h /\ z IN CosetPartition g h 684 ==> ((x o y) o z = x o (y o z))``, 685 rw_tac std_ss[coset_op_def] >> 686 `h <= g /\ Group g` by metis_tac[normal_subgroup_groups] >> 687 rw[group_assoc, normal_coset_property1, normal_coset_property2, cogen_coset_element, cogen_def]); 688 689(* Theorem: [Quotient Group Identity] 690 h << g ==> H IN CosetPartition g h /\ !x. x INCosetPartition g h ==> H o x = x *) 691(* Proof: 692 Since #e * H = H by coset_id_eq_subgroup 693 hence H IN CosetPartition g h by coset_partition_element, group_id_element 694 Since cogen g h x IN G and x = cogen g h x * H by cogen_def 695 By normal_coset_property1, 696 cogen g h (#e * H) * cogen g h x * H = #e * cogen g h x * H 697 or cogen g h H * cogen g h x * H = cogen g h x * H by group_lid 698 Hence 699 H o x = cogen g h H * cogen g h x * H by coset_op_def 700 = cogen g h x * H by above 701 = x 702*) 703val quotient_group_id = store_thm( 704 "quotient_group_id", 705 ``!g h:'a group. h << g ==> H IN CosetPartition g h /\ !x. x IN CosetPartition g h ==> (H o x = x)``, 706 ntac 3 strip_tac >> 707 `h <= g /\ Group g` by metis_tac[normal_subgroup_def, Subgroup_def] >> 708 `#e * H = H` by rw_tac std_ss[coset_id_eq_subgroup] >> 709 `#e IN G` by rw_tac std_ss[group_id_element] >> 710 rw_tac std_ss[coset_op_def] >| [ 711 metis_tac[coset_partition_element], 712 `cogen g h x IN G /\ (cogen g h x * H = x)` by rw_tac std_ss[cogen_def] >> 713 `cogen g h (#e * H) * cogen g h x * H = #e * cogen g h x * H` by rw_tac std_ss[normal_coset_property1] >> 714 metis_tac[group_lid] 715 ]); 716 717(* Theorem: [Quotient Group Inverse] 718 h << g ==> x IN CosetPartition g h ==> ?y. y IN CosetPartition g h /\ (y o x = H) *) 719(* Proof: 720 Since x IN CosetPartition g h, 721 cogen g h x IN G /\ (cogen g h x * H = x) by cogen_def 722 and |/ (cogen g h x) IN G /\ |/ (cogen g h x) * cogen g h x = #e by group_inv_element, group_linv 723 hence |/ (cogen g h x) * H IN CosetPartition g h by coset_partition_element 724 Let y = |/ (cogen g h x) * H, then 725 y o x = cogen g h ( |/ (cogen g h x) * H) * cogen g h x * H 726 = |/ (cogen g h x) * H o cogen g h x * H by normal_coset_property1 727 = ( |/ (cogen g h x) * cogen g h x) * H by coset_op_def 728 = #e * H = H by coset_id_eq_subgroup 729*) 730val quotient_group_inv = store_thm( 731 "quotient_group_inv", 732 ``!g h:'a group. h << g ==> !x. x IN CosetPartition g h ==> ?y. y IN CosetPartition g h /\ (y o x = H)``, 733 rpt strip_tac >> 734 `h <= g /\ Group g` by metis_tac[normal_subgroup_groups] >> 735 `cogen g h x IN G /\ (cogen g h x * H = x)` by rw_tac std_ss[cogen_def] >> 736 `|/ (cogen g h x) IN G /\ ( |/ (cogen g h x) * cogen g h x = #e)` by rw[] >> 737 `|/ (cogen g h x) * H IN CosetPartition g h` by metis_tac[coset_partition_element] >> 738 metis_tac[coset_op_def, normal_coset_property1, coset_id_eq_subgroup]); 739 740(* Theorem: quotient_group is a group for normal subgroup 741 i.e. h << g ==> Group (quotient_group g h) *) 742(* Proof: 743 This is to prove: 744 (1) x IN CosetPartition g h /\ y IN CosetPartition g h ==> x o y IN CosetPartition g h 745 true by quotient_group_closure. 746 (2) x IN CosetPartition g h /\ y IN CosetPartition g h /\ z IN CosetPartition g h ==> (x o y) o z = x o y o z 747 true by quotient_group_assoc. 748 (3) H IN CosetPartition g h 749 true by quotient_group_id. 750 (4) x IN CosetPartition g h ==> H o x = x 751 true by quotient_group_id. 752 (5) x IN CosetPartition g h ==> ?y. y IN CosetPartition g h /\ (y o x = H) 753 true by quotient_group_inv. 754*) 755val quotient_group_group = store_thm( 756 "quotient_group_group", 757 ``!g h:'a group. h << g ==> Group (quotient_group g h)``, 758 rpt strip_tac >> 759 `h <= g /\ Group h /\ Group g` by metis_tac[normal_subgroup_groups] >> 760 rw_tac std_ss[group_def_alt, quotient_group_def] >| [ 761 rw_tac std_ss[quotient_group_closure], 762 rw_tac std_ss[quotient_group_assoc], 763 rw_tac std_ss[quotient_group_id], 764 rw_tac std_ss[quotient_group_id], 765 rw_tac std_ss[quotient_group_inv] 766 ]); 767 768(* ------------------------------------------------------------------------- *) 769(* Group Homomorphism by left_coset via normal subgroup. *) 770(* ------------------------------------------------------------------------- *) 771 772(* Theorem: A normal subgroup induces a natural homomorphism to its quotient group, i.e. 773 h << g ==> GroupHomo (left_coset g H) g (g / h) *) 774(* Proof: 775 After expanding by quotient_group_def, this is to show 2 things: 776 (1) h << g /\ x IN G ==> x * H IN CosetPartition g h 777 This is true by coset_partition_element, and normal_subgroup_subgroup. 778 (2) h << g /\ x IN G /\ y IN G ==> (x * y) * H = x * H o y * H 779 This is to show: 780 (x * y) * H = (cogen g h (x * H) * cogen g h (y * H)) * H 781 Since x * H IN CosetPartition g h by coset_partition_element 782 y * H IN CosetPartition g h by coset_partition_element 783 hence cogen g h (x * H) IN G by cogen_def 784 cogen g h (y * H) IN G by cogen_def 785 By normal_subgroup_coset_eq, this is to show: 786 (x * y) / (cogen g h (x * H) * cogen g h (y * H)) IN H 787 But (x * y) / (cogen g h (x * H) * cogen g h (y * H)) 788 = x * (y / cogen g h (y * H)) / x * (x / cogen g h (x * H) by group_div_pair 789 790 Since x / cogen g h (x * H) IN H by normal_cogen_property 791 and z = y / cogen g h (y * H) IN H by normal_cogen_property 792 so x * z * / x IN H since z IN H by normal_subgroup_property 793 hence their product is IN H by group_op_element 794*) 795val normal_subgroup_coset_homo = store_thm( 796 "normal_subgroup_coset_homo", 797 ``!g h:'a group. h << g ==> GroupHomo (left_coset g H) g (g / h)``, 798 rw_tac std_ss[GroupHomo_def, quotient_group_def, left_coset_def] >- 799 metis_tac[coset_partition_element, normal_subgroup_subgroup] >> 800 rw_tac std_ss[coset_op_def] >> 801 `h <= g /\ !a z. a IN G /\ z IN H ==> a * z / a IN H` by metis_tac[normal_subgroup_def] >> 802 `Group h /\ Group g /\ !x y. x IN H /\ y IN H ==> (h.op x y = x * y)` by metis_tac[subgroup_property] >> 803 `x * H IN CosetPartition g h /\ y * H IN CosetPartition g h` by metis_tac[coset_partition_element] >> 804 `cogen g h (x * H) IN G /\ cogen g h (y * H) IN G` by rw_tac std_ss[cogen_def] >> 805 `(x * y) / (cogen g h (x * H) * cogen g h (y * H)) IN H` 806 suffices_by rw_tac std_ss[normal_subgroup_coset_eq, group_op_element] >> 807 rw_tac std_ss[group_div_pair] >> 808 `x / cogen g h (x * H) IN H /\ y / cogen g h (y * H) IN H` by rw_tac std_ss[normal_cogen_property] >> 809 `x * (y / cogen g h (y * H)) / x IN H` by rw_tac std_ss[normal_subgroup_property] >> 810 metis_tac[group_op_element]); 811 812(* Theorem: x o y = (CHOICE (preimage (left_coset g H) G x) * CHOICE (preimage (left_coset g H) G y)) * H *) 813(* Proof: 814 This is to show: 815 cogen g h x * cogen g h y * H = CHOICE (preimage (left_coset g H) G x) * CHOICE (preimage (left_coset g H) G y) * H 816 By normal_subgroup_coset_eq, need to show: 817 (cogen g h x * cogen g h y) / (CHOICE (preimage (left_coset g H) G x) * CHOICE (preimage (left_coset g H) G y)) IN H 818 i.e. (cogen g h x) * ((cogen g h y) / CHOICE (preimage (left_coset g H) G y)) / (cogen g h x) * 819 ((cogen g h x) / CHOICE (preimage (left_coset g H) G x)) IN H by group_div_pair 820 Since x = (cogen g h x) * H by cogen_def 821 x = (CHOICE (preimage (left_coset g H) G x)) * H by preimage_choice_property 822 (cogen g h x) / (CHOICE (preimage (left_coset g H) G x)) IN H by normal_subgroup_coset_eq 823 Similarly, 824 y = (cogen g h y) * H by cogen_def 825 y = (CHOICE (preimage (left_coset g H) G y)) * H by preimage_def 826 (cogen g h y) / (CHOICE (preimage (left_coset g H) G y)) IN H by normal_subgroup_coset_eq 827 Hence (cogen g h x) * ((cogen g h y) / (CHOICE (preimage (left_coset g H) G y))) / (cogen g h x) by normal_subgroup_property 828 and the whole product is thus in H by group_op_element, as h <= g ==> Group h. 829*) 830val normal_coset_op_property = store_thm( 831 "normal_coset_op_property", 832 ``!g h:'a group. h << g ==> !x y. x IN CosetPartition g h /\ y IN CosetPartition g h ==> 833 (x o y = (CHOICE (preimage (left_coset g H) G x) * CHOICE (preimage (left_coset g H) G y)) * H)``, 834 rw_tac std_ss[coset_op_def] >> 835 `h <= g /\ Group g /\ !a z. a IN G /\ z IN H ==> a * z / a IN H` by metis_tac[normal_subgroup_def, subgroup_property] >> 836 `cogen g h x IN G /\ ((cogen g h x) * H = x)` by rw_tac std_ss[cogen_def] >> 837 `cogen g h y IN G /\ ((cogen g h y) * H = y)` by rw_tac std_ss[cogen_def] >> 838 `x IN IMAGE (left_coset g H) G` by metis_tac[coset_partition_element, left_coset_def, IN_IMAGE] >> 839 `y IN IMAGE (left_coset g H) G` by metis_tac[coset_partition_element, left_coset_def, IN_IMAGE] >> 840 `CHOICE (preimage (left_coset g H) G x) IN G /\ (x = (CHOICE (preimage (left_coset g H) G x)) * H)` by metis_tac[preimage_choice_property, left_coset_def] >> 841 `CHOICE (preimage (left_coset g H) G y) IN G /\ (y = (CHOICE (preimage (left_coset g H) G y)) * H)` by metis_tac[preimage_choice_property, left_coset_def] >> 842 `(cogen g h x) / CHOICE (preimage (left_coset g H) G x) IN H` by metis_tac[normal_subgroup_coset_eq] >> 843 `(cogen g h y) / CHOICE (preimage (left_coset g H) G y) IN H` by metis_tac[normal_subgroup_coset_eq] >> 844 `(cogen g h x * cogen g h y) / (CHOICE (preimage (left_coset g H) G x) * CHOICE (preimage (left_coset g H) G y)) IN H` suffices_by rw_tac std_ss[normal_subgroup_coset_eq, group_op_element] >> 845 rw_tac std_ss[group_div_pair] >> 846 prove_tac[group_op_element, subgroup_property]); 847(* This theorem does not help to prove identity below, but helps to prove isomorphism. *) 848 849(* Theorem: h << g ==> GroupIso I (homo_group g (left_coset g H)) (g / h) *) 850(* Proof: 851 This is to show: 852 (1) h << g ==> GroupHomo I (homo_group g (left_coset g H)) (g / h) 853 This is to show: 854 (1.1) x IN IMAGE (left_coset g H) G ==> x IN CosetPartition g h 855 true by subgroup_coset_in_partition. 856 (1.2) x IN IMAGE (left_coset g H) G /\ y IN IMAGE (left_coset g H) G ==> image_op g (left_coset g H) x y = x o y 857 Since x IN CosetPartition g h by subgroup_coset_in_partition 858 y IN CosetPartition g h by subgroup_coset_in_partition 859 hence true by normal_coset_op_property, image_op_def, left_coset_def. 860 (2) h << g ==> BIJ I (homo_group g (left_coset g H)).carrier (g / h).carrier 861 This is to show: BIJ I (IMAGE (left_coset g H) G) (CosetPartition g h) 862 Since h <= g by normal_subgroup_def 863 this is true by BIJ and subgroup_coset_in_partition. 864*) 865val coset_homo_group_iso_quotient_group = store_thm( 866 "coset_homo_group_iso_quotient_group", 867 ``!g h:'a group. h << g ==> GroupIso I (homo_group g (left_coset g H)) (g / h)``, 868 rw_tac std_ss[GroupIso_def] >| [ 869 `h <= g` by metis_tac[normal_subgroup_def] >> 870 rw_tac std_ss[GroupHomo_def, homo_monoid_def, quotient_group_def] >| [ 871 rw_tac std_ss[GSYM subgroup_coset_in_partition], 872 `x IN CosetPartition g h` by rw_tac std_ss[GSYM subgroup_coset_in_partition] >> 873 `y IN CosetPartition g h` by rw_tac std_ss[GSYM subgroup_coset_in_partition] >> 874 rw_tac std_ss[image_op_def, left_coset_def, normal_coset_op_property] 875 ], 876 `h <= g` by metis_tac[normal_subgroup_def] >> 877 rw_tac std_ss[homo_monoid_def, quotient_group_def] >> 878 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF, subgroup_coset_in_partition] 879 ]); 880 881(* ------------------------------------------------------------------------- *) 882(* Kernel Group of Group Homomorphism. *) 883(* ------------------------------------------------------------------------- *) 884 885(* Define kernel of a mapping: the preimage of identity. *) 886val kernel_def = Define` 887 kernel f (g:'a group) (h:'b group) = preimage f G h.id 888`; 889 890(* Convert kernel to a group structure *) 891val kernel_group_def = Define` 892 kernel_group f (g:'a group) (h:'b group) = 893 <| carrier := kernel f g h; 894 id := g.id; 895 op := g.op 896 |>`; 897 898(* Theorem: !x. x IN kernel f g h <=> x IN G /\ f x = h.id *) 899(* Proof: by definition. *) 900val kernel_property = store_thm( 901 "kernel_property", 902 ``!(g:'a group) (h:'b group). !f x. x IN kernel f g h <=> x IN G /\ (f x = h.id)``, 903 simp_tac std_ss [kernel_def, preimage_def] >> 904 rw[]); 905 906(* export trivial truth. *) 907val _ = export_rewrites ["kernel_property"]; 908 909(* Theorem alias *) 910val kernel_element = save_thm("kernel_element", kernel_property); 911(* 912val kernel_element = |- !g h f x. x IN kernel f g h <=> x IN G /\ (f x = h.id): thm 913*) 914 915(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> Group (kernel_group f g h) *) 916(* Proof: 917 This is to show: 918 (1) x IN kernel f g h /\ y IN kernel f g h ==> x * y IN kernel f g h 919 By kernel property, x IN G and y IN G. 920 f (x * y) = (f x) o (f y) by GroupHomo_def 921 = h.id o h.id by kernel_property 922 = h.id by group_id_id 923 Since x * y IN G by group_op_element 924 Hence x * y IN kernel f g h by preimage_of_image 925 (2) x IN kernel f g h /\ y IN kernel f g h /\ z IN kernel f g h ==> x * y * z = x * (y * z) 926 By kernel_property, x IN G, y IN G and z IN G, 927 Hence x * y * z = x * (y * z) by group_assoc 928 (3) #e IN kernel f g h 929 Since #e IN G by group_id_element 930 and f #e = h.id by group_homo_id 931 Hence #e IN kernel f g h by preimage_of_image 932 (4) x IN kernel f g h ==> #e * x = x 933 By kernel property, x IN G. 934 Hence #e * x = x by group_lid 935 (5) x IN kernel f g h ==> ?y. y IN kernel f g h /\ (y * x = #e) 936 By kernel property, x IN G. 937 Also, |/ x IN G by group_inv_element 938 Let y = |/ x, then y * x = #e by group_linv 939 Now f ( |/ x) = h.inv (f x)) by group_homo_inv 940 = h.inv (h.id) by kernel_property 941 = h.id by group_inv_id 942 Hence |/ x IN kernel f g h by preimage_of_image 943*) 944val kernel_group_group = store_thm( 945 "kernel_group_group", 946 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> Group (kernel_group f g h)``, 947 rw_tac std_ss[GroupHomo_def] >> 948 rw_tac std_ss[group_def_alt, kernel_group_def] >| [ 949 `x IN G /\ y IN G` by metis_tac[kernel_property] >> 950 `x * y IN G` by rw[] >> 951 `f (x * y) = h.id` by metis_tac[kernel_property, group_id_id] >> 952 metis_tac[kernel_def, preimage_of_image], 953 `x IN G /\ y IN G /\ z IN G` by metis_tac[kernel_property] >> 954 rw[group_assoc], 955 `#e IN G` by rw[] >> 956 `f #e = h.id` by rw_tac std_ss[group_homo_id, GroupHomo_def] >> 957 metis_tac[kernel_def, preimage_of_image], 958 `x IN G` by metis_tac[kernel_property] >> 959 rw[], 960 `x IN G` by metis_tac[kernel_property] >> 961 qexists_tac `|/ x` >> 962 rw[] >> 963 `|/x IN G` by rw[] >> 964 `f ( |/ x) = h.inv (f x)` by rw_tac std_ss[group_homo_inv, GroupHomo_def] >> 965 `_ = h.inv h.id` by metis_tac[kernel_property] >> 966 `_ = h.id` by rw[] >> 967 metis_tac[kernel_def, preimage_of_image] 968 ]); 969 970(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> (kernel_group f g h) <= g *) 971(* Proof: by Subgroup_def. 972 (1) Group (kernel_group f g h) 973 True by kernel_group_group. 974 (2) (kernel_group f g h).carrier SUBSET G 975 True by kernel_group_def, kernel_def, preimage_subset_of_domain. 976 (3) x IN (kernel_group f g h).carrier /\ y IN (kernel_group f g h).carrier ==> (kernel_group f g h).op x y = x * y 977 True by kernel_group_def. 978*) 979val kernel_group_subgroup = store_thm( 980 "kernel_group_subgroup", 981 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> (kernel_group f g h) <= g``, 982 rw_tac std_ss[Subgroup_def] >| [ 983 rw_tac std_ss[kernel_group_group], 984 rw[kernel_group_def, kernel_def, preimage_subset_of_domain], 985 full_simp_tac (srw_ss()) [kernel_group_def] 986 ]); 987 988(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> (kernel_group f g h) << g *) 989(* Proof: by normal_subgroup_def. 990 With kernel_group_subgroup, it needs to show further: 991 a IN G /\ z IN kernel f g h ==> a * z * |/ a IN kernel f g h 992 By kernel_property, z IN G /\ f z = h.id 993 Hence a * z * |/ a IN G by group_op_element, group_inv_element. 994 f (a * z * |/ a) 995 = h.op (f (a * z)) f ( |/ a) by GroupHomo_def 996 = h.op (h.op (f a) (f z)) f ( |/ a) by GroupHomo_def 997 = h.op (h.op (f a) h.id) (h.inv f a) by group_homo_inv 998 = h.op (f a) (h.inv f a) by group_rid 999 = h.id by group_rinv 1000 Hence a * z * |/ a IN kernel f g h by preimage_of_image 1001*) 1002val kernel_group_normal = store_thm( 1003 "kernel_group_normal", 1004 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> (kernel_group f g h) << g``, 1005 rw_tac std_ss[normal_subgroup_def, kernel_group_subgroup, kernel_group_def] >> 1006 `z IN G /\ (f z = h.id)` by metis_tac[kernel_property] >> 1007 `|/ a IN G /\ a * z IN G /\ a * z * |/ a IN G` by rw[] >> 1008 `f (a * z * |/ a) = h.id` by metis_tac[group_rid, group_rinv, group_homo_inv, GroupHomo_def] >> 1009 metis_tac[kernel_property, group_div_def]); 1010 1011(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> Group (g / (kernel_group f g h)) *) 1012(* Proof: 1013 By kernel_group_normal, kernel_group f g h << g. 1014 By quotient_group_group, Group (g / (kernel_group f g h)) 1015*) 1016val kernel_quotient_group = store_thm( 1017 "kernel_quotient_group", 1018 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> Group (g / kernel_group f g h)``, 1019 rw[kernel_group_normal, quotient_group_group]); 1020 1021(* ------------------------------------------------------------------------- *) 1022(* Homomorphic Image and Kernel. *) 1023(* ------------------------------------------------------------------------- *) 1024 1025(* Proved in groupTheory, 1026- group_homo_group; 1027> val it = |- !g f. Group g /\ GroupHomo f g (homo_group g f) ==> Group (homo_group g f) : thm 1028- homo_monoid_def; 1029> val it = |- !g f. homo_group g f = <|carrier := IMAGE f G; op := image_op g f; id := f #e|> : thm 1030*) 1031 1032(* Define the homomorphic image of a group via homomorphism. *) 1033val homo_image_def = Define` 1034 homo_image f (g:'a group) (h:'b group) = 1035 <| carrier := IMAGE f G; 1036 op := h.op; 1037 id := h.id 1038 |> 1039`; 1040 1041(* Theorem: Monoid g /\ Monoid h /\ MonoidHomo f g h ==> Monoid (homo_image f g h) *) 1042(* Proof: by definition. 1043 (1) x IN IMAGE f G /\ y IN IMAGE f G ==> h.op x y IN IMAGE f G 1044 By IN_IMAGE, there are a IN G with f a = x, and b IN G with f b = y. 1045 Then h.op x y = h.op (f a) (f b) = f (a * b) by GroupHomo_def 1046 Since a * b IN G by group_op_element, hence f (a * b) IN IMAGE f G by IN_IMAGE. 1047 (2) x IN IMAGE f G /\ y IN IMAGE f G /\ z IN IMAGE f G ==> h.op (h.op x y) z = h.op x (h.op y z) 1048 By IN_IMAGE, there are a IN G with f a = x, b IN G with f b = y, and c IN G with f c = z. 1049 Hence x, y, z IN h.carrier by MonoidHomo_def, thus true by monoid_assoc. 1050 (3) h.id IN IMAGE f G 1051 Since #e IN G by monoid_id_element 1052 and f #e = h.id by MonoidHomo_def 1053 Hence h.id IN IMAGE f G by IN_IMAGE 1054 (4) h.op h.id x = x 1055 By IN_IMAGE, there are a IN G with f a = x. 1056 Hence x IN h.carrier by MonoidHomo_def 1057 Hence h.op h.id x = x by monoid_lid 1058 (5) h.op x h.id = x 1059 By IN_IMAGE, there are a IN G with f a = x. 1060 Hence x IN h.carrier by MonoidHomo_def 1061 Hence h.op x h.id = x by monoid_rid 1062*) 1063val homo_image_monoid = store_thm( 1064 "homo_image_monoid", 1065 ``!(g:'a monoid) (h:'b monoid). !f. Monoid g /\ Monoid h /\ MonoidHomo f g h ==> Monoid (homo_image f g h)``, 1066 rw_tac std_ss[MonoidHomo_def] >> 1067 `!x. x IN IMAGE f G ==> ?a. a IN G /\ (f a = x)` by metis_tac[IN_IMAGE] >> 1068 rw_tac std_ss[homo_image_def, Monoid_def] >| [ 1069 `?a. a IN G /\ (f a = x)` by rw_tac std_ss[] >> 1070 `?b. b IN G /\ (f b = y)` by rw_tac std_ss[] >> 1071 `a * b IN G` by rw[] >> 1072 `h.op x y = f (a * b)` by rw_tac std_ss[] >> 1073 metis_tac[IN_IMAGE], 1074 `x IN h.carrier` by metis_tac[] >> 1075 `y IN h.carrier` by metis_tac[] >> 1076 `z IN h.carrier` by metis_tac[] >> 1077 rw[monoid_assoc], 1078 metis_tac[monoid_id_element, IN_IMAGE], 1079 `x IN h.carrier` by metis_tac[] >> 1080 rw[], 1081 `x IN h.carrier` by metis_tac[] >> 1082 rw[] 1083 ]); 1084 1085(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> Group (homo_image f g h) *) 1086(* Proof: by definition. 1087 (1) x IN IMAGE f G /\ y IN IMAGE f G ==> h.op x y IN IMAGE f G 1088 By IN_IMAGE, there are a IN G with f a = x, and b IN G with f b = y. 1089 Then h.op x y = h.op (f a) (f b) = f (a * b) by GroupHomo_def 1090 Since a * b IN G by group_op_element, hence f (a * b) IN IMAGE f G by IN_IMAGE. 1091 (2) x IN IMAGE f G /\ y IN IMAGE f G /\ z IN IMAGE f G ==> h.op (h.op x y) z = h.op x (h.op y z) 1092 By IN_IMAGE, there are a IN G with f a = x, b IN G with f b = y, and c IN G with f c = z. 1093 Hence x, y, z IN h.carrier by GroupHomo_def, thus true by group_assoc. 1094 (3) h.id IN IMAGE f G 1095 Since #e IN G by group_id_element 1096 and f #e = h.id by group_homo_id 1097 Hence h.id IN IMAGE f G by IN_IMAGE 1098 (4) h.op h.id x = x 1099 By IN_IMAGE, there are a IN G with f a = x. 1100 Hence x IN h.carrier by GroupHomo_def 1101 Hence h.op h.id x = x by group_lid 1102 1103 Since GroupHomo f g h /\ by given 1104 f #e = h.id by group_homo_id 1105 ==> MonoidHomo h g h by GroupHomo_def, MonoidHomo_def 1106 Hence Monoid (homo_image f g h) by homo_image_monoid 1107 With Group_def and other definitions, this is to show: 1108 x IN IMAGE f G ==> ?y. y IN IMAGE f G /\ (h.op y x = h.id) 1109 By IN_IMAGE, there is a IN G with f a = x. 1110 Hence |/ a IN G by group_inv_element 1111 Let y = f ( |/ a), y IN IMAGE f G by IN_IMAGE 1112 h.op y x = h.op (f ( |/ a)) (f a) 1113 = f ( |/a * a) by GroupHomo_def 1114 = f #e by group_linv 1115 = h.id by group_homo_id 1116 h.op x y = h.op (f a) (f ( |/ a)) 1117 = f (a * |/a ) by GroupHomo_def 1118 = f #e by group_rinv 1119 = h.id by group_homo_id 1120*) 1121val homo_image_group = store_thm( 1122 "homo_image_group", 1123 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> Group (homo_image f g h)``, 1124 rpt strip_tac >> 1125 `f #e = h.id` by rw_tac std_ss[group_homo_id] >> 1126 `MonoidHomo f g h` by prove_tac[GroupHomo_def, MonoidHomo_def] >> 1127 `Monoid (homo_image f g h)` by rw[homo_image_monoid] >> 1128 rw_tac std_ss[Group_def, monoid_invertibles_def, homo_image_def, GSPECIFICATION, EXTENSION, EQ_IMP_THM] >> 1129 `?a. a IN G /\ (f a = x)` by metis_tac[IN_IMAGE] >> 1130 `|/ a IN G` by rw[] >> 1131 `( |/ a * a = #e) /\ (a * |/ a = #e)` by rw[] >> 1132 `f ( |/ a) IN IMAGE f G` by metis_tac[GroupHomo_def, IN_IMAGE] >> 1133 metis_tac[GroupHomo_def]); 1134 1135(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> (homo_image f g h) <= h *) 1136(* Proof: by Subgroup_def. 1137 (1) Group (homo_image f g h) 1138 True by homo_image_group. 1139 (2) (homo_image f g h).carrier SUBSET h.carrier 1140 (homo_image f g h).carrier = IMAGE f G by homo_image_def 1141 For all x IN IMAGE f G, ?a. a IN G /\ (f a = x)` by IN_IMAGE 1142 Hence x IN h.carrier by GroupHomo_def, hence true by SUBSET_DEF. 1143 (3) x IN (homo_image f g h).carrier /\ y IN (homo_image f g h).carrier ==> (homo_image f g h).op x y = h.op x y 1144 True by homo_image_def. 1145*) 1146val homo_image_subgroup = store_thm( 1147 "homo_image_subgroup", 1148 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> (homo_image f g h) <= h``, 1149 rw_tac std_ss[Subgroup_def] >| [ 1150 rw_tac std_ss[homo_image_group], 1151 rw[homo_image_def, SUBSET_DEF] >> 1152 metis_tac[GroupHomo_def], 1153 rw_tac std_ss[homo_image_def] 1154 ]); 1155 1156(* Theorem: Group g /\ Group h /\ SURJ f G h.carrier ==> GroupIso I h (homo_image f g h) *) 1157(* Proof: 1158 After expanding by GroupIso_def, GroupHomo_def, and homo_image_def, this is to show: 1159 (1) x IN h.carrier ==> x IN IMAGE f G 1160 Note x IN h.carrier ==> ?z. z IN G /\ f z = x by SURJ_DEF 1161 and z IN G ==> f z = x IN IMAGE f G by IN_IMAGE 1162 (2) x IN IMAGE f G ==> x IN h.carrier 1163 Note x IN IMAGE f G ==> ?z. z IN G /\ f z = x by IN_IMAGE 1164 and z IN G ==> f z = x IN h.carrier by SURJ_DEF 1165*) 1166val group_homo_image_surj_property = store_thm( 1167 "group_homo_image_surj_property", 1168 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ 1169 SURJ f G h.carrier ==> GroupIso I h (homo_image f g h)``, 1170 rw_tac std_ss[BIJ_DEF, SURJ_DEF, INJ_DEF, GroupIso_def, GroupHomo_def, homo_image_def] >> 1171 metis_tac[IN_IMAGE]); 1172 1173(* Theorem: Monoid g /\ MonoidHomo f g h ==> Monoid (homo_image f g h) *) 1174(* Proof: 1175 Note MonoidHomo f g h 1176 ==> !x. x IN G ==> f x IN h.carrier by MonoidHomo_def 1177 and !x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y)) by MonoidHomo_def 1178 and f #e = h.id by MonoidHomo_def 1179 Also !x. x IN IMAGE f G ==> ?a. a IN G /\ (f a = x) by IN_IMAGE 1180 1181 Expand by homo_image_def, Monoid_def, this is to show: 1182 (1) x IN IMAGE f G /\ y IN IMAGE f G ==> h.op x y IN IMAGE f G 1183 Note ?a. a IN G /\ (f a = x) by x IN IMAGE f G 1184 and ?b. b IN G /\ (f b = y) by y IN IMAGE f G 1185 also a * b IN G by monoid_op_element 1186 Now h.op x y = f (a * b) by above 1187 so h.op x y IN IMAGE f G by IN_IMAGE 1188 (2) x IN IMAGE f G /\ y IN IMAGE f G /\ z IN IMAGE f G ==> h.op (h.op x y) z = h.op x (h.op y z) 1189 Note ?a. a IN G /\ (f a = x) by x IN IMAGE f G 1190 and ?b. b IN G /\ (f b = y) by y IN IMAGE f G 1191 and ?c. c IN G /\ (f c = z) by z IN IMAGE f G 1192 Now h.op (h.op x y) z = f ((a * b) * c) by a * b IN G, and above 1193 and h.op x (h.op y z) = f (a * (b * c)) by b * c IN G, and above 1194 Since a * b * c = a * (b * c) by monoid_assoc 1195 thus h.op (h.op x y) z = h.op x (h.op y z) 1196 (3) h.id IN IMAGE f G 1197 Note h.id = f #e by above 1198 Now #e IN G by monoid_id_element 1199 so h.id IN IMAGE f G by IN_IMAGE 1200 (4) x IN IMAGE f G ==> h.op h.id x = x 1201 Note ?a. a IN G /\ (f a = x) by x IN IMAGE f G 1202 h.op h.id x 1203 = f (#e * a) by monoid_id_element, and above 1204 = f a by monoid_lid 1205 = x 1206 (5) x IN IMAGE f G ==> h.op x h.id = x 1207 Note ?a. a IN G /\ (f a = x) by x IN IMAGE f G 1208 h.op x h.id 1209 = f (a * #e) by monoid_id_element, and above 1210 = f a by monoid_rid 1211 = x 1212*) 1213val monoid_homo_homo_image_monoid = store_thm( 1214 "monoid_homo_homo_image_monoid", 1215 ``!(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidHomo f g h ==> Monoid (homo_image f g h)``, 1216 rw_tac std_ss[MonoidHomo_def] >> 1217 `!x. x IN IMAGE f G ==> ?a. a IN G /\ (f a = x)` by metis_tac[IN_IMAGE] >> 1218 rw_tac std_ss[homo_image_def, Monoid_def] >| [ 1219 `?a. a IN G /\ (f a = x)` by rw_tac std_ss[] >> 1220 `?b. b IN G /\ (f b = y)` by rw_tac std_ss[] >> 1221 `a * b IN G` by rw[] >> 1222 `h.op x y = f (a * b)` by rw_tac std_ss[] >> 1223 metis_tac[IN_IMAGE], 1224 `?a. a IN G /\ (f a = x)` by rw_tac std_ss[] >> 1225 `?b. b IN G /\ (f b = y)` by rw_tac std_ss[] >> 1226 `?c. c IN G /\ (f c = z)` by rw_tac std_ss[] >> 1227 `h.op x y = f (a * b)` by rw_tac std_ss[] >> 1228 `h.op y z = f (b * c)` by rw_tac std_ss[] >> 1229 `a * b IN G /\ b * c IN G` by rw[] >> 1230 `h.op (h.op x y) z = f ((a * b) * c)` by metis_tac[] >> 1231 `h.op x (h.op y z) = f (a * (b * c))` by metis_tac[] >> 1232 `a * b * c = a * (b * c)` by rw[monoid_assoc] >> 1233 metis_tac[], 1234 metis_tac[monoid_id_element, IN_IMAGE], 1235 `?a. a IN G /\ (f a = x)` by rw_tac std_ss[] >> 1236 `h.op h.id x = f (#e * a)` by rw_tac std_ss[monoid_id_element] >> 1237 metis_tac[monoid_lid], 1238 `x IN h.carrier` by metis_tac[] >> 1239 `?a. a IN G /\ (f a = x)` by rw_tac std_ss[] >> 1240 `h.op x h.id = f (a * #e)` by rw_tac std_ss[monoid_id_element] >> 1241 metis_tac[monoid_rid] 1242 ]); 1243 1244(* 1245GroupHomo_def is weaker than MonoidHomo_def. 1246May need to define GroupHomo = MonoidHomo, making f #e = h.id mandatory. 1247Better keep GroupHomo, just use MonoidHomo if necessary. 1248*) 1249 1250(* Theorem: Group g /\ MonoidHomo f g h ==> Group (homo_image f g h) *) 1251(* Proof: 1252 By Group_def, this is to show: 1253 (1) Monoid (homo_image f g h), true by monoid_homo_homo_image_monoid 1254 (2) monoid_invertibles (homo_image f g h) = (homo_image f g h).carrier 1255 By monoid_invertibles_def, homo_image_def, this is to show: 1256 x IN IMAGE f G ==> ?y. y IN IMAGE f G /\ (h.op x y = h.id) /\ (h.op y x = h.id) 1257 1258 Note ?a. a IN G /\ (f a = x) by x IN IMAGE f G 1259 Hence |/ a IN G by group_inv_element 1260 Let y = f ( |/ a). 1261 Then y IN IMAGE f G by IN_IMAGE 1262 h.op y x 1263 = h.op (f ( |/ a)) (f a) 1264 = f ( |/a * a) by MonoidHomo_def 1265 = f #e by group_linv 1266 = h.id by MonoidHomo_def 1267 h.op x y 1268 = h.op (f a) (f ( |/ a)) 1269 = f (a * |/a ) by MonoidHomo_def 1270 = f #e by group_rinv 1271 = h.id by MonoidHomo_def 1272*) 1273val group_homo_homo_image_group = store_thm( 1274 "group_homo_homo_image_group", 1275 ``!(g:'a group) (h:'b group) f. Group g /\ MonoidHomo f g h ==> Group (homo_image f g h)``, 1276 rpt strip_tac >> 1277 `Monoid (homo_image f g h)` by rw[monoid_homo_homo_image_monoid] >> 1278 rw_tac std_ss[Group_def, monoid_invertibles_def, homo_image_def, GSPECIFICATION, EXTENSION, EQ_IMP_THM] >> 1279 `?a. a IN G /\ (f a = x)` by metis_tac[IN_IMAGE] >> 1280 `|/ a IN G` by rw[] >> 1281 `( |/ a * a = #e) /\ (a * |/ a = #e)` by rw[] >> 1282 `f ( |/ a) IN IMAGE f G` by metis_tac[IN_IMAGE] >> 1283 metis_tac[MonoidHomo_def]); 1284 1285(* ------------------------------------------------------------------------- *) 1286(* First Isomorphic Theorem for Group. *) 1287(* ------------------------------------------------------------------------- *) 1288 1289(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> 1290 GroupHomo (\z. (CHOICE (preimage f G z)) * (kernel f g h) ) (homo_image f g h) (g / (kernel_group f g h)) *) 1291(* Proof: by GroupHomo_def, homo_image_def and quotient_group_def. 1292 This is to show: 1293 (1) !z. z IN IMAGE f G ==> CHOICE (preimage f G z) * kernel f g h IN CosetPartition g (kernel_group f g h) 1294 z IN IMAGE f G ==> CHOICE (preimage f G z) IN G by preimage_choice_property 1295 Since (kernel_group f g h) <= g by kernel_group_subgroup 1296 Hence CHOICE (preimage f G z) * kernel f g h IN CosetPartition g (kernel_group f g h) by coset_partition_element 1297 and 1298 (2) !z. z IN IMAGE f G /\ z' IN IMAGE f G ==> 1299 CHOICE (preimage f G (h.op z z')) * kernel f g h = 1300 coset_op g (kernel_group f g h) (CHOICE (preimage f G z) * kernel f g h) (CHOICE (preimage f G z') * kernel f g h) 1301 z IN IMAGE f G ==> CHOICE (preimage f G z) IN G by preimage_choice_property 1302 z IN IMAGE f G ==> CHOICE (preimage f G z) IN G by preimage_choice_property 1303 After expanding by coset_op_def, this is to show: 1304 CHOICE (preimage f G (h.op z z')) * kernel f g h = 1305 cogen g (kernel_group f g h) (CHOICE (preimage f G z) * kernel f g h) * 1306 cogen g (kernel_group f g h) (CHOICE (preimage f G z') * kernel f g h) * kernel f g h 1307 Now, (kernel_group f g h) << g by kernel_group_normal 1308 Let x = CHOICE (preimage f G z 1309 x' = CHOICE (preimage f G z' 1310 y = CHOICE (preimage f G (h.op z z')) 1311 k = kernel_group f g h 1312 s = kernel f g h 1313 This is to show: y * s = cogen g k (x * s) * cogen g k (x' * s) * s 1314 This can be done via normal_coset_property, but first: 1315 x IN G /\ x' IN G /\ (f x = z) /\ (f x' = z') by preimage_choice_property 1316 x * s IN CosetPartition g k by coset_partition_element 1317 x' * s IN CosetPartition g k by coset_partition_element 1318 Hence 1319 cogen g k (x * s) * cogen g k (x' * s) * s = x * x' * s by normal_coset_property 1320 It remains to show: y * s = x * x' * s 1321 i.e. to show: y / (x * x') IN s since k << g if we know y IN G and x * x' IN G 1322 But h.op z z' = f (x * x') by GroupHomo_def 1323 Hence x * x' IN G /\ f (x * x') IN IMAGE f G by group_op_element, IN_IMAGE 1324 and f y = h.op z z' = f (x * x') by preimage_choice_property 1325 Hence we just need to show: y / (x * x') IN s where s = kernel f g h 1326 An element is in kernel if it maps to h.id, so compute: 1327 f (y / (x * x')) 1328 = f (y * |/ (x * x')) by group_div_def 1329 = h.op (f y) f ( |/ (x * x')) by GroupHomo_def 1330 = h.op (f y) h.inv f (x * x') by group_homo_inv 1331 = h.op (f y) h.inv (f y) by above 1332 = h.id by group_rinv 1333*) 1334val homo_image_homo_quotient_kernel = store_thm( 1335 "homo_image_homo_quotient_kernel", 1336 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> 1337 GroupHomo (\z. (CHOICE (preimage f G z)) * (kernel f g h) ) 1338 (homo_image f g h) (g / (kernel_group f g h))``, 1339 rw_tac std_ss[homo_image_def, quotient_group_def] >> 1340 `(kernel_group f g h).carrier = kernel f g h` by rw_tac std_ss[kernel_group_def] >> 1341 rw_tac std_ss[GroupHomo_def] >| [ 1342 metis_tac[preimage_choice_property, kernel_group_subgroup, coset_partition_element], 1343 rw_tac std_ss[coset_op_def] >> 1344 `(kernel_group f g h) << g /\ (kernel_group f g h) <= g` by rw_tac std_ss[kernel_group_normal, normal_subgroup_subgroup] >> 1345 qabbrev_tac `x = CHOICE (preimage f G z)` >> 1346 qabbrev_tac `x' = CHOICE (preimage f G z')` >> 1347 qabbrev_tac `y = CHOICE (preimage f G (h.op z z'))` >> 1348 qabbrev_tac `k = kernel_group f g h` >> 1349 qabbrev_tac `s = kernel f g h` >> 1350 `x IN G /\ x' IN G /\ (f x = z) /\ (f x' = z')` by rw_tac std_ss[preimage_choice_property, Abbr`x`, Abbr`x'`] >> 1351 `x * s IN CosetPartition g k /\ x' * s IN CosetPartition g k` by metis_tac[coset_partition_element] >> 1352 `cogen g k (x * s) * cogen g k (x' * s) * s = x * x' * s` by rw_tac std_ss[normal_coset_property] >> 1353 full_simp_tac std_ss [] >> 1354 `h.op z z' = f (x * x')` by metis_tac[GroupHomo_def] >> 1355 `x * x' IN G /\ f (x * x') IN IMAGE f G` by rw[] >> 1356 `y IN G /\ (f y = h.op z z')` by metis_tac[preimage_choice_property] >> 1357 `y / (x * x') IN s` suffices_by rw_tac std_ss[normal_subgroup_coset_eq] >> 1358 `|/ (x * x') IN G` by rw[] >> 1359 `f y IN h.carrier` by metis_tac[GroupHomo_def] >> 1360 `f (y / (x * x')) = f (y * |/ (x * x'))` by rw_tac std_ss[group_div_def] >> 1361 `_ = h.op (f y) (f ( |/ (x * x')))` by metis_tac[GroupHomo_def] >> 1362 `_ = h.op (f y) (h.inv (h.op z z'))` by metis_tac[group_homo_inv] >> 1363 `_ = h.id` by metis_tac[group_rinv] >> 1364 metis_tac[kernel_property, group_div_element] 1365 ]); 1366 1367(* Theorem: BIJ (\z. CHOICE (preimage f G z) * kernel f g h) 1368 (homo_image f g h).carrier (g / kernel_group f g h).carrier *) 1369(* Proof: 1370 This is to prove: 1371 (1) z IN IMAGE f G ==> CHOICE (preimage f G z) * kernel f g h IN CosetPartition g (kernel_group f g h) 1372 z IN IMAGE f G ==> CHOICE (preimage f G z) IN G by preimage_choice_property 1373 Since (kernel_group f g h) <= g by kernel_group_subgroup 1374 Hence CHOICE (preimage f G z) * kernel f g h IN CosetPartition g (kernel_group f g h) by coset_partition_element 1375 (2) z IN IMAGE f G /\ z' IN IMAGE f G /\ CHOICE (preimage f G z) * kernel f g h = CHOICE (preimage f G z') * kernel f g h ==> z = z' 1376 Let x = CHOICE (preimage f G z) 1377 x' = CHOICE (preimage f G z'), then 1378 z IN IMAGE f G ==> x IN G /\ f x = z by preimage_choice_property 1379 z' IN IMAGE f G ==> x' IN G /\ f x' = z' by preimage_choice_property 1380 x IN G ==> z = f x IN H, x' IN G ==> z' = f x' IN H by GroupHomo_def 1381 Given x * kernel f g h = x' * kernel f g h 1382 Since (kernel_group f g h) << g by kernel_group_normal 1383 this gives x / x' IN kernel f g h by normal_subgroup_coset_eq 1384 Hence f (x / x') = h.id by kernel_property 1385 i.e. h.id = f (x / x') 1386 = f (x * |/ x') by group_div_def 1387 = h.op (f x) (f ( |/ x')) by GroupHomo_def 1388 = h.op (f x) h.inv (f x') by group_homo_inv 1389 = h.op z h.inv z' by above 1390 Hence z = z' by group_linv_unique, group_inv_inv 1391 (3) same as (1). 1392 (4) x IN CosetPartition g (kernel_group f g h) ==> ?z. z IN IMAGE f G /\ (CHOICE (preimage f G z) * kernel f g h = x) 1393 Note (kernel_group f g h) << g by kernel_group_normal 1394 and (kernel_group f g h) <= g by normal_subgroup_subgroup 1395 Since x IN CosetPartition g (kernel_group f g h), 1396 ?a. a IN G /\ (x = a * kernel f g h) by coset_partition_element 1397 Let z = f a, then z IN IMAGE f G by IN_IMAGE, 1398 and CHOICE (preimage f G z) IN G /\ (f (CHOICE (preimage f G z)) = z) by preimage_choice_property 1399 Thus, this is to prove: 1400 CHOICE (preimage f G z) * kernel f g h = x = a * kernel f g h 1401 Since kernel f g h << g, this is true if CHOICE (preimage f G z) / a IN kernel f g h 1402 or need to show: f (CHOICE (preimage f G z) / a) = h.id by normal_subgroup_coset_eq 1403 By computation, 1404 f (CHOICE (preimage f G z) / a) 1405 = f (CHOICE (preimage f G z) * |/ a) by group_div_def 1406 = h.op (f (CHOICE (preimage f G z)) (f ( |/ a)) by GroupHomo_def 1407 = h.op z (h.inv z) by group_homo_inv 1408 = h.id by group_linv 1409*) 1410val homo_image_to_quotient_kernel_bij = store_thm( 1411 "homo_image_to_quotient_kernel_bij", 1412 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> 1413 BIJ (\z. (CHOICE (preimage f G z)) * (kernel f g h) ) 1414 (homo_image f g h).carrier (g / (kernel_group f g h)).carrier``, 1415 rw_tac std_ss[homo_image_def, quotient_group_def] >> 1416 `(kernel_group f g h).carrier = kernel f g h` by rw_tac std_ss[kernel_group_def] >> 1417 rw_tac std_ss[BIJ_DEF, SURJ_DEF, INJ_DEF] >| [ 1418 metis_tac[preimage_choice_property, kernel_group_subgroup, coset_partition_element], 1419 `CHOICE (preimage f G z) IN G /\ (f (CHOICE (preimage f G z)) = z)` by rw_tac std_ss[preimage_choice_property] >> 1420 `CHOICE (preimage f G z') IN G /\ (f (CHOICE (preimage f G z')) = z')` by rw_tac std_ss[preimage_choice_property] >> 1421 `(kernel_group f g h) << g` by rw_tac std_ss[kernel_group_normal] >> 1422 qabbrev_tac `x = CHOICE (preimage f G z)` >> 1423 qabbrev_tac `x' = CHOICE (preimage f G z')` >> 1424 qabbrev_tac `k = kernel_group f g h` >> 1425 qabbrev_tac `s = kernel f g h` >> 1426 `|/ x' IN G` by rw[] >> 1427 `f ( |/ x') = h.inv z'` by rw_tac std_ss[group_homo_inv] >> 1428 `z IN h.carrier /\ z' IN h.carrier /\ h.inv z' IN h.carrier` by metis_tac[GroupHomo_def] >> 1429 `x / x' IN s` by metis_tac[normal_subgroup_coset_eq] >> 1430 `h.id = f (x / x')` by metis_tac[kernel_property] >> 1431 `_ = f (x * |/ x')` by rw_tac std_ss[group_div_def] >> 1432 `_ = h.op (f x) (h.inv (f x'))` by metis_tac[GroupHomo_def] >> 1433 metis_tac[group_linv_unique, group_inv_inv], 1434 metis_tac[preimage_choice_property, kernel_group_subgroup, coset_partition_element], 1435 `(kernel_group f g h) << g /\ (kernel_group f g h) <= g` by rw_tac std_ss[kernel_group_normal, normal_subgroup_subgroup] >> 1436 `?a. a IN G /\ (x = a * kernel f g h)` by metis_tac[coset_partition_element] >> 1437 qexists_tac `f a` >> 1438 rw[] >> 1439 qabbrev_tac `z = f a` >> 1440 qabbrev_tac `x = CHOICE (preimage f G z)` >> 1441 qabbrev_tac `k = kernel_group f g h` >> 1442 qabbrev_tac `s = kernel f g h` >> 1443 `x IN G /\ (f x = z) /\ z IN h.carrier` by metis_tac[preimage_choice_property, IN_IMAGE, GroupHomo_def] >> 1444 `x / a IN s` suffices_by metis_tac[normal_subgroup_coset_eq] >> 1445 `|/a IN G` by rw[] >> 1446 `f (x * |/ a) = h.op (f x) (f ( |/ a))` by metis_tac[GroupHomo_def] >> 1447 `_ = h.op z (h.inv z)` by metis_tac[group_homo_inv] >> 1448 `_ = h.id` by metis_tac[group_rinv] >> 1449 metis_tac[kernel_property, group_div_def, group_div_element] 1450 ]); 1451 1452(* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> 1453 GroupIso (\z. (CHOICE (preimage f G z)) * (kernel f g h) ) (homo_image f g h) (g / (kernel_group f g h)) *) 1454(* Proof: by GroupIso_def. 1455 (1) GroupHomo (\z. CHOICE (preimage f G z) * kernel f g h) (homo_image f g h) (g / kernel_group f g h) 1456 True by homo_image_homo_quotient_kernel. 1457 (2) BIJ (\z. CHOICE (preimage f G z) * kernel f g h) (homo_image f g h).carrier (g / kernel_group f g h).carrier 1458 True by homo_image_to_quotient_kernel_bij. 1459*) 1460val homo_image_iso_quotient_kernel = store_thm( 1461 "homo_image_iso_quotient_kernel", 1462 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> 1463 GroupIso (\z. (CHOICE (preimage f G z)) * (kernel f g h) ) 1464 (homo_image f g h) (g / (kernel_group f g h))``, 1465 rw[GroupIso_def, homo_image_homo_quotient_kernel, homo_image_to_quotient_kernel_bij]); 1466 1467(* Theorem [First Isomorphism Theorem for Groups] 1468 Let G and H be groups, and let f: G -> H be a homomorphism. Then: 1469 (a) The kernel of f is a normal subgroup of G, 1470 (b) The image of f is a subgroup of H, and 1471 (c) The image of f is isomorphic to the quotient group G / ker(f). 1472 In particular, (d) if f is surjective then H is isomorphic to G / ker(f). 1473*) 1474(* Proof: 1475 (a) by kernel_group_normal 1476 (b) by homo_image_subgroup 1477 (c) by homo_image_iso_quotient_kernel 1478 (d) by group_homo_image_surj_property 1479*) 1480val group_first_isomorphism_thm = store_thm( 1481 "group_first_isomorphism_thm", 1482 ``!(g:'a group) (h:'b group). !f. Group g /\ Group h /\ GroupHomo f g h ==> 1483 (kernel_group f g h) << g /\ 1484 (homo_image f g h) <= h /\ 1485 GroupIso (\z. (CHOICE (preimage f G z)) * (kernel f g h) ) 1486 (homo_image f g h) (g / (kernel_group f g h)) /\ 1487 (SURJ f G h.carrier ==> GroupIso I h (homo_image f g h))``, 1488 rw[kernel_group_normal, homo_image_subgroup, homo_image_iso_quotient_kernel, group_homo_image_surj_property]); 1489 1490(* ------------------------------------------------------------------------- *) 1491 1492(* export theory at end *) 1493val _ = export_theory(); 1494 1495(*===========================================================================*) 1496