1(* ------------------------------------------------------------------------- *) 2(* Field Symmetry Group *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "symmetryField"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* Get dependent theories local *) 21(* val _ = load "fieldMapTheory"; *) 22open monoidTheory groupTheory ringTheory fieldTheory; 23open monoidOrderTheory groupOrderTheory; 24open monoidMapTheory groupMapTheory ringMapTheory fieldMapTheory; 25open subgroupTheory; 26 27(* val _ = load "symmetryGroupTheory"; *) 28open symmetryGroupTheory; 29 30(* open dependent theories *) 31(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 32(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 33open pred_setTheory arithmeticTheory dividesTheory gcdTheory; 34 35(* Get dependent theories in lib *) 36(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 37open helperNumTheory helperSetTheory; 38 39 40(* ------------------------------------------------------------------------- *) 41(* Field Symmetry Group Documentation *) 42(* ------------------------------------------------------------------------- *) 43(* Overload: 44*) 45(* Definitions and Theorems (# are exported): 46 47 Helper Theorems: 48 49 Maps restricted on a Set: 50 ring_homo_on_homo |- !r r_ f. Ring r /\ RingHomo f r r_ ==> RingHomo (f on R) r r_ 51 ring_iso_on_iso |- !r r_ f. Ring r /\ RingIso f r r_ ==> RingIso (f on R) r r_ 52 ring_auto_on_auto |- !r f. Ring r /\ RingAuto f r ==> RingAuto (f on R) r 53 ring_auto_on_id |- !r. Ring r ==> RingAuto (I on R) r 54 field_homo_on_homo |- !r r_ f. Field r /\ FieldHomo f r r_ ==> FieldHomo (f on R) r r_ 55 field_iso_on_iso |- !r r_ f. Field r /\ FieldIso f r r_ ==> FieldIso (f on R) r r_ 56 field_auto_on_auto |- !r f. Field r /\ FieldAuto f r ==> FieldAuto (f on R) r 57 field_auto_on_id |- !r. Field r ==> FieldAuto (I on R) r 58 59 Symmetric Group of a Field: 60 field_symmetric_group_group |- !r. Group (symmetric_group R) 61 field_nonzero_symmetric_group_group |- !r. Group (symmetric_group R+) 62 63 Automorphism Group of a Field: 64 field_automorphism_group_group |- !r. Field r ==> Group (automorphism_group f* ) 65 automorphism_field_def |- !r. automorphism_field r = 66 <|carrier := {f on R | f | FieldAuto f r}; 67 op := (\f1 f2. f1 o f2 on R); 68 id := (I on R)|> 69 automorphism_field_group |- !r. Field r ==> Group (automorphism_field r) 70 71 Map Fixing a Set: 72 fixes_def |- !f s. f fixes s <=> !x. x IN s ==> (f x = x) 73 fixes_compose |- !s f g. f fixes s /\ g fixes s ==> f o g fixes s 74 fixes_I |- !s. I fixes s 75 fixes_inj_linv |- !s t f. f fixes s /\ INJ f s t ==> LINV f s fixes s 76 fixes_bij_linv |- !s f. f fixes s /\ f PERMUTES s ==> LINV f s fixes s 77 fixes_on_subset |- !s t f. f fixes s /\ s SUBSET t ==> (f on t) fixes s 78 fixes_on_linv |- !s t f. f fixes s /\ s SUBSET t /\ INJ f t t ==> LINV f t fixes s 79 80 Field Automorphism fixing subfield: 81 subfield_auto_def |- !f r s. subfield_auto f r s <=> FieldAuto f r /\ f fixes B 82 subfield_auto_field_auto |- !r s f. subfield_auto f r s ==> FieldAuto f r 83 subfield_auto_fixes |- !r s f. subfield_auto f r s ==> f fixes B 84 subfield_auto_element |- !r s f x. subfield_auto f r s /\ x IN R ==> f x IN R 85 subfield_auto_bij |- !r s f. Field r /\ subfield_auto f r s ==> f PERMUTES R 86 subfield_auto_compose |- !r s f1 f2. subfield_auto f1 r s /\ subfield_auto f2 r s ==> 87 subfield_auto (f1 o f2) r s 88 subfield_auto_I |- !r s. subfield_auto I r s 89 subfield_auto_on_compose |- !r s f1 f2. Field r /\ B SUBSET R /\ subfield_auto f1 r s /\ 90 subfield_auto f2 r s ==> subfield_auto (f1 o f2 on R) r s 91 subfield_auto_on_id |- !r s. Field r /\ B SUBSET R ==> subfield_auto (I on R) r s 92 subfield_auto_on_linv |- !r s f. Field r /\ B SUBSET R /\ subfield_auto f r s ==> 93 subfield_auto (LINV f R) r s /\ (LINV f R o f on R) = (I on R) 94 95 Subfield Fixing Automorphism Group: 96 subfield_auto_group_def |- !r s. subfield_auto_group r s = 97 <|carrier := {f on R | f | subfield_auto f r s}; 98 op := (\f1 f2. f1 o f2 on R); id := (I on R)|> 99 subfield_auto_group_group |- !r s. Field r /\ B SUBSET R ==> Group (subfield_auto_group r s) 100 subfield_auto_group_group_1 |- !r s. Field r /\ subfield s r ==> Group (subfield_auto_group r s) 101 subfield_auto_group_group_2 |- !r s. s <<= r ==> Group (subfield_auto_group r s) 102*) 103 104(* ------------------------------------------------------------------------- *) 105(* Field Symmetry Group *) 106(* ------------------------------------------------------------------------- *) 107 108(* ------------------------------------------------------------------------- *) 109(* Helper Theorems *) 110(* ------------------------------------------------------------------------- *) 111 112(* ------------------------------------------------------------------------- *) 113(* Maps restricted on a Set *) 114(* ------------------------------------------------------------------------- *) 115 116(* Theorem: Ring r /\ RingHomo f r r_ ==> RingHomo (f on R) r r_ *) 117(* Proof: 118 By RingHomo_def, this is to show: 119 (1) x IN R ==> (f on R) x IN R_, true by fun_on_element 120 (2) GroupHomo f r.sum r_.sum ==> GroupHomo (f on R) r.sum r_.sum 121 Note Group r.sum by ring_add_group 122 Thus GroupHomo (f on R) r.sum r_.sum by group_homo_on_homo 123 (2) MonoidHomo f r.prod r_.prod ==> MonoidHomo (f on R) r.prod r_.prod 124 Note Monoid r.prod by ring_mult_monoid 125 Thus GroupHomo (f on R) r.sum r_.sum by monoid_homo_on_homo 126*) 127val ring_homo_on_homo = store_thm( 128 "ring_homo_on_homo", 129 ``!(r:'a ring) (r_:'b ring) f. Ring r /\ RingHomo f r r_ ==> RingHomo (f on R) r r_``, 130 rw_tac std_ss[RingHomo_def] >- 131 rw_tac std_ss[fun_on_element] >- 132 metis_tac[ring_add_group, group_homo_on_homo] >> 133 metis_tac[ring_mult_monoid, monoid_homo_on_homo]); 134 135(* Theorem: Ring r /\ RingIso f r r_ ==> RingIso (f on R) r r_ *) 136(* Proof: 137 RingIso f r r_ 138 = RingHomo f r r_ /\ BIJ f R R_ by RingIso_def 139 ==> RingHomo (f on R) r r_ /\ BIJ f R R_ by ring_homo_on_homo 140 ==> RingHomo (f on R) r r_ /\ BIJ (f on R) R R_ by bij_on_bij 141 = RingIso (f on R) r r_ by RingIso_def 142*) 143val ring_iso_on_iso = store_thm( 144 "ring_iso_on_iso", 145 ``!(r:'a ring) (r_:'b ring) f. Ring r /\ RingIso f r r_ ==> RingIso (f on R) r r_``, 146 rw_tac std_ss[RingIso_def, ring_homo_on_homo, bij_on_bij]); 147 148(* Theorem: Ring r /\ RingAuto f r ==> RingAuto (f on R) r *) 149(* Proof: 150 RingAuto f r 151 = RingIso f r r by RingAuto_def 152 ==> RingIso (f on R) r r_ by ring_iso_on_iso 153 = RingAuto (f on R) r r_ by RingAuto_def 154*) 155val ring_auto_on_auto = store_thm( 156 "ring_auto_on_auto", 157 ``!(r:'a ring) f. Ring r /\ RingAuto f r ==> RingAuto (f on R) r ``, 158 rw_tac std_ss[RingAuto_def, ring_iso_on_iso]); 159 160(* Theorem: Ring r ==> RingAuto (I on R) r *) 161(* Proof: 162 Ring r 163 ==> RingAuto I r by ring_auto_I 164 ==> RingAuto (I on R) r by ring_auto_on_auto 165*) 166val ring_auto_on_id = store_thm( 167 "ring_auto_on_id", 168 ``!(r:'a ring). Ring r ==> RingAuto (I on R) r``, 169 rw_tac std_ss[ring_auto_I, ring_auto_on_auto]); 170 171(* Theorem: Field r /\ FieldHomo f r r_ ==> FieldHomo (f on R) r r_ *) 172(* Proof: 173 Note Ring r by field_is_ring 174 FieldHomo f r r_ 175 = RingHomo f r r_ by field_homo_eq_ring_homo 176 ==> RingHomo (f on R) r r_ by ring_homo_on_homo 177 = FieldHomo (f on R) r r_ by field_homo_eq_ring_homo 178*) 179val field_homo_on_homo = store_thm( 180 "field_homo_on_homo", 181 ``!(r:'a field) (r_:'b field) f. Field r /\ FieldHomo f r r_ ==> FieldHomo (f on R) r r_``, 182 rw_tac std_ss[field_homo_eq_ring_homo, field_is_ring, ring_homo_on_homo]); 183 184(* Theorem: Field r /\ FieldIso f r r_ ==> FieldIso (f on R) r r_ *) 185(* Proof: 186 Note Ring r by field_is_ring 187 FieldIso f r r_ 188 = RingIso f r r_ by field_iso_eq_ring_iso 189 ==> RingIso (f on R) r r_ by ring_iso_on_iso 190 = FieldIso (f on R) r r_ by field_iso_eq_ring_iso 191*) 192val field_iso_on_iso = store_thm( 193 "field_iso_on_iso", 194 ``!(r:'a field) (r_:'b field) f. Field r /\ FieldIso f r r_ ==> FieldIso (f on R) r r_``, 195 rw_tac std_ss[field_iso_eq_ring_iso, field_is_ring, ring_iso_on_iso]); 196 197(* Theorem: Field r /\ FieldAuto f r ==> FieldAuto (f on R) r *) 198(* Proof: 199 Note Ring r by field_is_ring 200 FieldAuto f r 201 = RingAuto f r by field_auto_eq_ring_auto 202 ==> RingAuto (f on R) r by ring_auto_on_auto 203 ==> FieldAuto (f on R) r by field_auto_eq_ring_auto 204 or 205 FieldAuto f r 206 = FieldIso f r r by FieldAuto_def 207 ==> FieldIso (f on R) r r_ by field_iso_on_iso 208 = FieldAuto (f on R) r r_ by FieldAuto_def 209*) 210val field_auto_on_auto = store_thm( 211 "field_auto_on_auto", 212 ``!(r:'a field) f. Field r /\ FieldAuto f r ==> FieldAuto (f on R) r ``, 213 rw_tac std_ss[FieldAuto_def, field_iso_on_iso]); 214 215(* Theorem: Field r ==> FieldAuto (I on R) r *) 216(* Proof: 217 Field r 218 ==> FieldAuto I r by field_auto_I 219 ==> FieldAuto (I on R) r by field_auto_on_auto 220*) 221val field_auto_on_id = store_thm( 222 "field_auto_on_id", 223 ``!(r:'a field). Field r ==> FieldAuto (I on R) r``, 224 rw_tac std_ss[field_auto_I, field_auto_on_auto]); 225 226(* ------------------------------------------------------------------------- *) 227(* Symmetric Group of a Field *) 228(* ------------------------------------------------------------------------- *) 229 230(* All permutations of a field form the Symmetric Group. *) 231 232(* Theorem: Group (symmetric_group R) *) 233(* Proof: by symmetric_group_group *) 234val field_symmetric_group_group = store_thm( 235 "field_symmetric_group_group", 236 ``!r:'a field. Group (symmetric_group R)``, 237 rw_tac std_ss[symmetric_group_group]); 238 239(* Theorem: Group (symmetric_group R+) *) 240(* Proof: by symmetric_group_group. 241 Both Group (symmetric_group R) 242 and Group (symmetric_group R+) are true 243 due to BIJ f R R must map #0 to #0 uniquely, 244 and a bijection taking out #0 <-> #0 is still a bijection. 245*) 246val field_nonzero_symmetric_group_group = store_thm( 247 "field_nonzero_symmetric_group_group", 248 ``!r:'a field. Group (symmetric_group R+)``, 249 rw_tac std_ss[symmetric_group_group]); 250 251(* ------------------------------------------------------------------------- *) 252(* Automorphism Group of a Field *) 253(* ------------------------------------------------------------------------- *) 254 255(* All automorphisms of a field form the Automorphism Group. *) 256 257(* Theorem: Field r ==> Group (automorphism_group f* ) *) 258(* Proof: 259 Note Group f* by field_mult_group 260 Thus Group (automorphism_group f* ) by automorphism_group_group 261*) 262val field_automorphism_group_group = store_thm( 263 "field_automorphism_group_group", 264 ``!r:'a field. Field r ==> Group (automorphism_group f* )``, 265 rw_tac std_ss[field_mult_group, automorphism_group_group]); 266 267(* This is true, but this is not the aim. *) 268 269(* All automorphisms of a Field form a Group. *) 270val automorphism_field_def = Define` 271 automorphism_field (r:'a field) = 272 <| carrier := {f on R | f | FieldAuto f r}; 273 op := \f1 f2. (f1 o f2) on R; 274 id := (I on R) 275 |> 276`; 277 278(* Theorem: Field r ==> Group (automorphism_field r) *) 279(* Proof: 280 By group_def_alt, automorphism_field_def, this is to show: 281 (1) FieldAuto f r /\ FieldAuto f' r ==> ?f''. ((f on R) o (f' on R) on R) = (f'' on R) /\ FieldAuto f'' r 282 Let f'' = f o f' on R. 283 Note f PERMUTES R /\ f' PERMUTES R by field_auto_bij 284 Then (f on R) o (f' on R) on R = (f o f' on R) on R by bij_on_compose, fun_on_on 285 and FieldAuto (f o f' on R) r by field_auto_compose, field_auto_on_auto 286 (2) FieldAuto f r /\ FieldAuto f' r /\ FieldAuto f'' r ==> 287 (((f on R) o (f' on R) on R) o (f'' on R) on R) = ((f on R) o ((f' on R) o (f'' on R) on R) on R) 288 Note f PERMUTES R /\ f' PERMUTES R /\ f'' PERMUTES R by field_auto_bij 289 The result follows by bij_on_compose_assoc, bij_on_bij 290 (3) ?f. (I on R) = (f on R) /\ FieldAuto f r 291 Let f = I, then FieldAuto I g by field_auto_I 292 (4) ((I on R) o (f on R) on R) = (f on R) 293 Note !x. x IN R ==> f x IN R by field_auto_bij, BIJ_ELEMENT 294 (I on R) o (f on R) on R 295 = (I o f) on R by fun_on_compose 296 = f on R by I_o_ID 297 (5) FieldAuto f r ==> ?y. (?f. y = (f on R) /\ FieldAuto f r) /\ (y o (f on R) on R) = (I on R) 298 Let y = (LINV f R) on R, Then 299 (1) Let f = LINV f R, then FieldAuto f g by field_auto_linv_auto 300 (2) FieldAuto f r ==> (LINV f R on R) o (f on R) on R = I on R 301 Note f PERMUTES R by field_auto_bij 302 (LINV f R on R) o (f on R) on R 303 = (LINV f R o f) on R by bij_on_compose 304 = I on R by bij_on_inv 305*) 306 307Theorem automorphism_field_group: 308 !r:'a field. Field r ==> Group (automorphism_field r) 309Proof 310 rpt strip_tac >> 311 rw_tac std_ss[group_def_alt, automorphism_field_def, GSPECIFICATION] >| [ 312 rename [���(f on R) o (f' on R) on R���] >> qexists_tac `f o f' on R` >> 313 rpt strip_tac >- 314 metis_tac[bij_on_compose, fun_on_on, field_auto_bij] >> 315 metis_tac[field_auto_compose, field_auto_on_auto], 316 rename [���((f on R) o (f' on R) on R) o (f'' on R) on R���] >> 317 `f PERMUTES R /\ f' PERMUTES R /\ f'' PERMUTES R` by rw[field_auto_bij] >> 318 metis_tac[bij_on_bij, bij_on_compose_assoc, field_auto_bij], 319 metis_tac[field_auto_I], 320 rename [���FieldAuto f r���] >> 321 `!x. x IN R ==> f x IN R` by metis_tac[field_auto_bij, BIJ_ELEMENT] >> 322 rw[fun_on_compose], 323 rename [���FieldAuto f r���] >> 324 qexists_tac `(LINV f R) on R` >> 325 rpt strip_tac >- metis_tac[field_auto_linv_auto] >> 326 metis_tac[bij_on_compose, bij_on_inv, field_auto_bij] 327 ] 328QED 329 330(* ------------------------------------------------------------------------- *) 331(* Map Fixing a Set *) 332(* ------------------------------------------------------------------------- *) 333 334(* Define a map fixing a set *) 335(* Overload a map fixing a set -- but hard to control: 336val _ = overload_on("fixes", ``\f s. !x. x IN s ==> (f x = x)``); 337*) 338val fixes_def = Define` 339 fixes f s <=> (!x. x IN s ==> (f x = x)) 340`; 341val _ = set_fixity "fixes" (Infix(NONASSOC, 450)); (* same as relation *) 342 343(* Theorem: (f fixes s) /\ (g fixes s) ==> (f o g) fixes s *) 344(* Proof: 345 Let x IN s, then 346 (f o g) x 347 = f (g x) by composition 348 = f x by fixes_def, g fixes s 349 = x by fixes_def, f fixes s 350*) 351val fixes_compose = store_thm( 352 "fixes_compose", 353 ``!(s:'a -> bool) f g. (f fixes s) /\ (g fixes s) ==> (f o g) fixes s``, 354 rw_tac std_ss[fixes_def]); 355 356(* Theorem: I fixes s *) 357(* Proof: 358 Let x IN s, then I x = x by I_THM 359 Thus I fixes s by fixes_def 360*) 361val fixes_I = store_thm( 362 "fixes_I", 363 ``!(s:'a -> bool). I fixes s``, 364 rw_tac std_ss[fixes_def]); 365 366(* Theorem: f fixes s /\ INJ f s t ==> (LINV f s) fixes s *) 367(* Proof: 368 Let x IN s. 369 (LINV f s) x 370 = (LINV f s) (f x) by fixes_def, f fixes s 371 = x by LINV_DEF 372 Thus (LINV f s) fixes s by fixes_def 373*) 374val fixes_inj_linv = store_thm( 375 "fixes_inj_linv", 376 ``!(s:'a -> bool) t f. f fixes s /\ INJ f s t ==> (LINV f s) fixes s``, 377 metis_tac[fixes_def, LINV_DEF]); 378 379(* Theorem: f fixes s /\ f PERMUTES s ==> (LINV f s) fixes s *) 380(* Proof: 381 Note INJ f s s by BIJ_DEF 382 Thus (LINV f s) fixes s by fixes_inj_linv 383*) 384val fixes_bij_linv = store_thm( 385 "fixes_bij_linv", 386 ``!(s:'a -> bool) f. f fixes s /\ f PERMUTES s ==> (LINV f s) fixes s``, 387 metis_tac[BIJ_DEF, fixes_inj_linv]); 388 389(* Theorem: f fixes s /\ s SUBSET t ==> (f on t) fixes s *) 390(* Proof: by on_def, fixes_def, SUBSET_DEF *) 391val fixes_on_subset = store_thm( 392 "fixes_on_subset", 393 ``!(s:'a -> bool) t f. f fixes s /\ s SUBSET t ==> (f on t) fixes s``, 394 rw_tac std_ss[on_def, fixes_def, SUBSET_DEF]); 395 396 397(* Theorem: f fixes s /\ s SUBSET t /\ INJ f t t ==> LINV f t fixes s *) 398(* Proof: by fixes_def, LINV_SUBSET *) 399val fixes_on_linv = store_thm( 400 "fixes_on_linv", 401 ``!(s:'a -> bool) t f. f fixes s /\ s SUBSET t /\ INJ f t t ==> LINV f t fixes s``, 402 metis_tac[fixes_def, LINV_SUBSET]); 403 404(* ------------------------------------------------------------------------- *) 405(* Field Automorphism fixing subfield. *) 406(* ------------------------------------------------------------------------- *) 407 408(* Define the subfield-fixing automorphism *) 409val subfield_auto_def = Define` 410 subfield_auto f (r:'a field) (s:'a field) <=> FieldAuto f r /\ (f fixes B) 411`; 412(* Note: no subfield or SUBSET relating r and s here. *) 413(* Note: including B SUBSET R only simplifies some theorems with subfield_auto f r s in premise, 414 but then subfield_auto_I needs explicity B SUBSET R, 415 so finally subfield_auto_group_group still requires B SUBSET R for qualification. *) 416 417(* Theorem: subfield_auto f r s ==> FieldAuto f r *) 418(* Proof: by subfield_auto_def. *) 419val subfield_auto_field_auto = store_thm( 420 "subfield_auto_field_auto", 421 ``!(r s):'a field. !f. subfield_auto f r s ==> FieldAuto f r``, 422 rw_tac std_ss[subfield_auto_def]); 423 424(* Theorem: subfield_auto f r s ==> f fixes B *) 425(* Proof: by subfield_auto_def. *) 426val subfield_auto_fixes = store_thm( 427 "subfield_auto_fixes", 428 ``!(r s):'a field. !f. subfield_auto f r s ==> f fixes B``, 429 rw_tac std_ss[subfield_auto_def]); 430 431(* Theorem: subfield_auto f r s /\ x IN R ==> f x IN R *) 432(* Proof: by subfield_auto_field_auto, field_auto_element *) 433val subfield_auto_element = store_thm( 434 "subfield_auto_element", 435 ``!(r s):'a field. !f x. subfield_auto f r s /\ x IN R ==> f x IN R``, 436 metis_tac[subfield_auto_field_auto, field_auto_element]); 437 438(* Theorem: Field r /\ subfield_auto f r s ==> f PERMUTES R *) 439(* Proof: by subfield_auto_field_auto, field_auto_bij *) 440val subfield_auto_bij = store_thm( 441 "subfield_auto_bij", 442 ``!(r s):'a field. !f. Field r /\ subfield_auto f r s ==> f PERMUTES R``, 443 metis_tac[subfield_auto_field_auto, field_auto_bij]); 444 445(* Theorem: subfield_auto f1 r s /\ subfield_auto f2 r s ==> subfield_auto (f1 o f2) r s *) 446(* Proof: 447 By subfield_auto_def, this is to show: 448 (1) FieldAuto f1 r /\ FieldAuto f2 r ==> FieldAuto (f1 o f2) r, true by field_auto_compose 449 True by field_auto_on_compose 450 (2) f1 fixes B /\ f2 fixes B ==> f1 o f2 fixes B 451 True by fixes_compose 452*) 453val subfield_auto_compose = store_thm( 454 "subfield_auto_compose", 455 ``!(r s):'a field. !f1 f2. subfield_auto f1 r s /\ subfield_auto f2 r s ==> subfield_auto (f1 o f2) r s``, 456 rw_tac std_ss[subfield_auto_def, field_auto_compose, fixes_compose]); 457 458(* Theorem: subfield_auto I r s *) 459(* Proof: 460 By subfield_auto_def, this is to show: 461 (1) FieldAuto I r, true by field_auto_I 462 (2) I fixes B, true by fixes_I 463*) 464val subfield_auto_I = store_thm( 465 "subfield_auto_I", 466 ``!(r s):'a field. subfield_auto I r s``, 467 rw_tac std_ss[subfield_auto_def, field_auto_I, fixes_I]); 468 469(* Theorem: Field r /\ B SUBSET R /\ 470 subfield_auto f r s1 /\ subfield_auto f r s2 ==> subfield_auto r s ((f1 oo f2) R) *) 471(* Proof: 472 By subfield_auto_def, this is to show: 473 (1) FieldAuto f1 r /\ FieldAuto f2 r ==> FieldAuto (f1 o f2 on R) r 474 Note FieldAuto (f1 o f2) r by field_auto_compose 475 Thus FieldAuto (f1 o f2 on R) r by field_auto_on_auto, Field r 476 (2) f1 fixes B /\ f2 fixes B ==> (f1 o f2 on R) fixes B 477 Note (f1 o f2) fixes B by fixes_compose 478 Thus ((f1 o f2) on R) fixes B by fixes_on_subset, B SUBSET R 479*) 480val subfield_auto_on_compose = store_thm( 481 "subfield_auto_on_compose", 482 ``!(r s):'a field. !f1 f2. Field r /\ B SUBSET R /\ 483 subfield_auto f1 r s /\ subfield_auto f2 r s ==> subfield_auto ((f1 o f2) on R) r s``, 484 rw_tac std_ss[subfield_auto_def] >- 485 rw_tac std_ss[field_auto_compose, field_auto_on_auto] >> 486 rw_tac std_ss[fixes_compose, fixes_on_subset]); 487 488(* Theorem: Field r /\ B SUBSET R ==> subfield_auto (I on R) r s *) 489(* Proof: 490 By subfield_auto_def, this is to show: 491 (1) FieldAuto (I on R) r, true by field_auto_on_id 492 (2) B SUBSET R ==> (I on R) fixes B 493 Note I fixes B by fixes_I 494 so (I on R) fixes B by fixes_on_subset, B SUBSET R 495*) 496val subfield_auto_on_id = store_thm( 497 "subfield_auto_on_id", 498 ``!(r s):'a field. Field r /\ B SUBSET R ==> subfield_auto (I on R) r s``, 499 rw_tac std_ss[subfield_auto_def] >- 500 rw_tac std_ss[field_auto_on_id] >> 501 rw_tac std_ss[fixes_I, fixes_on_subset]); 502 503(* Theorem: Field r /\ B SUBSET R /\ subfield_auto f r s ==> 504 subfield_auto (LINV f R) r s /\ (((LINV f R) o f) on R) = (I on R) *) 505(* Proof: 506 By subfield_auto_def, this is to show: 507 (1) FieldAuto f r ==> FieldAuto (LINV f R) r, 508 This is true by field_auto_linv_auto 509 (2) f fixes B ==> LINV f R fixes B 510 Note BIJ f R R by FieldAuto_def, FieldIso_def 511 so INJ f R R by BIJ_DEF 512 Thus LINV f R fixes B by fixes_on_linv, B SUBSET R 513 (3) LINV f R o f on R = I on R 514 By on_def, FUN_EQ_THM, this is to show: 515 (if x IN R then LINV f R (f x) else ARB) = if x IN R then x else ARB 516 Note BIJ f R R by FieldAuto_def, FieldIso_def 517 so INJ f R R by BIJ_DEF 518 Thus x IN R ==> LINV f R (f x) = x by LINV_DEF 519*) 520val subfield_auto_on_linv = store_thm( 521 "subfield_auto_on_linv", 522 ``!(r s):'a field. !f. Field r /\ B SUBSET R /\ subfield_auto f r s ==> 523 subfield_auto (LINV f R) r s /\ (((LINV f R) o f) on R) = (I on R)``, 524 rw_tac std_ss[subfield_auto_def] >- 525 rw_tac std_ss[field_auto_linv_auto] >- 526 (`INJ f R R` by metis_tac[FieldAuto_def, FieldIso_def, BIJ_DEF] >> 527 rw_tac std_ss[fixes_on_linv]) >> 528 rw[on_def, FUN_EQ_THM] >> 529 `INJ f R R` by metis_tac[FieldAuto_def, FieldIso_def, BIJ_DEF] >> 530 metis_tac[LINV_DEF]); 531 532(* ------------------------------------------------------------------------- *) 533(* Subfield Fixing Automorphism Group *) 534(* ------------------------------------------------------------------------- *) 535 536(* 537Given a field/subfield pair: s <<= r, 538an automorphism f:'a -> 'a is FieldAuto f r. 539Those automorphisms that keep the subfield s fixed: f fixes B, 540will form a group, the automorphism subfield group: Auto r s, or Galois group. 541*) 542 543(* Define the subfield-fixing automorphism group *) 544val subfield_auto_group_def = Define` 545 subfield_auto_group (r:'a field) (s:'a field) = 546 <| carrier := {f on R | f | subfield_auto f r s}; 547 op := (\f1 f2. (f1 o f2) on R); 548 id := (I on R) 549 |> 550`; 551 552(* Theorem: The subfield-fixing automorphism group is a group. 553 Field r /\ B SUBSET R ==> Group (subfield_auto_group r s) *) 554(* Proof: 555 By group_def_alt, subfield_auto_group_def, this is to show: 556 (1) subfield_auto f r s /\ subfield_auto f' r s ==> 557 ?f''. ((f on R) o (f' on R) on R = f'' on R) /\ subfield_auto f'' r s 558 Let f'' = (f o f') on R. 559 Then (f on R) o (f' on R) on R = f'' on R by bij_on_compose, bij_on_bij 560 and subfield_auto (f o f' on R) r s by subfield_auto_on_compose 561 (2) ((f on R) o (f' on R) on R) o (f'' on R) on R = (f on R) o ((f' on R) o (f'' on R) on R) on R 562 Note BIJ f R B /\ BIJ f' R B /\ BIJ f'' R B by subfield_auto_bij 563 True by bij_on_bij, bij_on_compose_assoc. 564 (3) ?f. (I on R = f on R) /\ subfield_auto f r s 565 Let f = I, 566 Then subfield_auto r s I by subfield_auto_I, B SUBSET R 567 (4) subfield_auto f r s /\ B SUBSET R ==> (I on R) o (f on R) on R = f on R 568 Note !x. x IN R ==> f x IN R by subfield_auto_bij, BIJ_ELEMENT 569 True by fun_on_compose, I_o_ID 570 (5) subfield_auto f r s ==> ?y. (?f. (y = f on R) /\ subfield_auto f r s) /\ (y o (f on R) on R = I on R) 571 Let y = (LINV f R) on R. 572 Then subfield (LINV f r) r s by subfield_auto_on_linv 573 Note BIJ f R B by subfield_auto_bij 574 y o (f on R) on R 575 = ((LINV f R) on R) o (f on R) on R by notation 576 = ((LINV f R) o f) on R by bij_on_compose 577 = I o R by subfield_auto_on_linv 578*) 579 580Theorem subfield_auto_group_group: 581 !(r s):'a field. Field r /\ B SUBSET R ==> Group (subfield_auto_group r s) 582Proof 583 rw_tac std_ss[group_def_alt, subfield_auto_group_def, GSPECIFICATION] >| [ 584 rename [���(f on R) o (f' on R) on R���] >> 585 qexists_tac `f o f' on R` >> 586 rpt strip_tac >- 587 metis_tac[bij_on_compose, fun_on_on, subfield_auto_bij] >> 588 rw_tac std_ss[subfield_auto_on_compose], 589 prove_tac[subfield_auto_bij, bij_on_bij, bij_on_compose_assoc], 590 metis_tac[subfield_auto_I], 591 rename [���subfield_auto f r s���] >> 592 `!x. x IN R ==> f x IN R` by metis_tac[subfield_auto_bij, BIJ_ELEMENT] >> 593 rw[fun_on_compose], 594 metis_tac[subfield_auto_on_linv, subfield_auto_bij, bij_on_compose] 595 ] 596QED 597 598(* This is a milestone theorem. *) 599 600(* Theorem: Field r /\ subfield s r ==> Group (subfield_auto_group r s) *) 601(* Proof: by subfield_auto_group_group, subfield_carrier_subset *) 602val subfield_auto_group_group_1 = store_thm( 603 "subfield_auto_group_group_1", 604 ``!(r s):'a field. Field r /\ subfield s r ==> Group (subfield_auto_group r s)``, 605 rw[subfield_auto_group_group, subfield_carrier_subset]); 606 607(* Theorem: s <<= r ==> Group (subfield_auto_group r s) *) 608(* Proof: by subfield_auto_group_group_1 *) 609val subfield_auto_group_group_2 = store_thm( 610 "subfield_auto_group_group_2", 611 ``!(r s):'a field. s <<= r ==> Group (subfield_auto_group r s)``, 612 rw[subfield_auto_group_group_1]); 613 614(* ------------------------------------------------------------------------- *) 615 616(* export theory at end *) 617val _ = export_theory(); 618 619(*===========================================================================*) 620