1(* ------------------------------------------------------------------------- *) 2(* Finite Field: Master Polynomial *) 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 "ffMaster"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Loading theories *) 23(* (* val _ = load "ffCycloTheory"; *) *) 24(* val _ = load "ffPolyTheory"; *) 25open ffBasicTheory; 26open ffAdvancedTheory; 27open ffPolyTheory; 28 29(* Open theories in order *) 30 31(* open dependent theories *) 32open arithmeticTheory pred_setTheory listTheory; 33(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 34(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 35open dividesTheory gcdTheory; 36 37(* Get dependent theories in lib *) 38(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 39(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 40(* (* val _ = load "helperFunctionTheory"; -- in ringTheory *) *) 41(* (* val _ = load "helperListTheory"; -- in polyRingTheory *) *) 42open helperNumTheory helperSetTheory helperListTheory helperFunctionTheory; 43 44(* Get dependent theories local *) 45(* (* val _ = load "groupInstancesTheory"; -- in ringInstancesTheory *) *) 46(* (* val _ = load "ringInstancesTheory"; *) *) 47(* (* val _ = load "fieldInstancesTheory"; *) *) 48open monoidTheory groupTheory ringTheory fieldTheory; 49open monoidOrderTheory groupOrderTheory; 50open subgroupTheory; 51 52open groupInstancesTheory ringInstancesTheory fieldInstancesTheory; 53open groupCyclicTheory; 54 55open ringBinomialTheory; 56open ringDividesTheory; 57open ringIdealTheory; 58open ringUnitTheory; 59 60(* Get polynomial theory of Ring *) 61open polynomialTheory polyWeakTheory polyRingTheory polyDivisionTheory polyBinomialTheory; 62 63open polyFieldTheory; 64open polyFieldDivisionTheory; 65open polyFieldModuloTheory; 66open polyModuloRingTheory; 67 68open polyMonicTheory; 69open polyProductTheory; 70open polyDividesTheory; 71open polyGCDTheory; 72open polyIrreducibleTheory; 73 74(* (* val _ = load "polyMapTheory"; *) *) 75open monoidMapTheory groupMapTheory ringMapTheory fieldMapTheory; 76open polyMapTheory; 77 78open polyDerivativeTheory; 79open polyEvalTheory; 80open polyRootTheory; 81open binomialTheory; 82 83open GaussTheory; 84open EulerTheory; 85 86(* val _ = load "fieldBinomialTheory"; *) 87open fieldBinomialTheory; (* for finite_field_freshman_all *) 88 89(* (* val _ = load "MobiusTheory"; *) *) 90 91 92(* ------------------------------------------------------------------------- *) 93(* Finite Field Master Polynomial Documentation *) 94(* ------------------------------------------------------------------------- *) 95(* Overload: 96 poly_psi r n = PPROD (monic_irreducibles_degree r n) 97 Psi n = poly_psi r n 98*) 99(* Definitions and Theorems (# are exported): 100 101 Master Polynomial and its roots: 102 poly_master_root_all |- !r. FiniteField r ==> !x. x IN R ==> root (master (CARD R)) x 103 poly_master_roots_all |- !r. FiniteField r ==> (roots (master (CARD R)) = R) 104 poly_master_subfield_root |- !r s. s <<= r ==> !x. x IN B ==> 105 !n. poly_root s (Master s n) x <=> root (master n) x 106 poly_master_coprime_diff |- !r. FiniteField r ==> !n. 0 < n ==> 107 pgcd (master (CARD R ** n)) (diff (master (CARD R ** n))) ~~ |1| 108 poly_master_prod_set_over_natural_monic |- !r. FiniteField r ==> 109 !n. monic (PPIMAGE (\k. master (CARD R ** k)) (natural n)) 110 poly_master_prod_set_over_natural_poly |- !r. FiniteField r ==> 111 !n. poly (PPIMAGE (\k. master (CARD R ** k)) (natural n)) 112 poly_master_prod_set_over_natural_nonzero |- !r. FiniteField r ==> 113 !n. PPIMAGE (\k. master (CARD R ** k)) (natural n) <> |0| 114 poly_master_prod_set_over_natural_deg |- !r. FiniteField r ==> (let m = CARD R in 115 !n. deg (PPIMAGE (\k. master (m ** k)) (natural n)) = 116 m * (m ** n - 1) DIV (m - 1)) 117 118 Irreducible Factors of Master Polynomial: 119 poly_ulead_divides_master_condition 120 |- !r. Ring r ==> !p. ulead p ==> 121 !n. p pdivides master n <=> (X ** n == X) (pm p) 122 poly_irreducible_divides_master |- !r. FiniteField r ==> !p. monic p /\ ipoly p ==> 123 p pdivides master (CARD R ** deg p) 124 poly_mod_master_root_condition |- !r. Field r ==> !p. monic p /\ ipoly p ==> 125 !x. x IN (PolyModRing r p).carrier ==> 126 !n. poly_root (PolyModRing r p) (Master (PolyModRing r p) n) x <=> (x ** n == x) (pm p) 127 poly_mod_poly_sum_gen |- !r. Ring r ==>!p. pmonic p ==> !f. poly_fun f ==> 128 !n. poly_sum (GENLIST f n) % p = poly_sum (GENLIST (\k. f k % p) n) % p 129 poly_irreducible_master_factor_all_roots 130 |- !r. FiniteField r ==> !p. monic p /\ ipoly p ==> 131 !n. p pdivides master (CARD R ** n) ==> 132 (PolyModRing r p).carrier SUBSET 133 poly_roots (PolyModRing r p) (Master (PolyModRing r p) (CARD R ** n)) 134 poly_irreducible_master_factor_deg 135 |- !r. FiniteField r ==> !p. monic p /\ ipoly p ==> 136 !n. 0 < n /\ p pdivides master (CARD R ** n) ==> deg p <= n 137 poly_irreducible_master_divisibility 138 |- !r. FiniteField r ==> !p. monic p /\ ipoly p ==> 139 !n. p pdivides master (CARD R ** n) <=> deg p divides n 140 poly_irreducible_master_subfield_divisibility 141 |- !r s. FiniteField r /\ s <<= r ==> !p. monic p /\ IPoly s p ==> 142 (p pdivides master (CARD R) <=> deg p divides (r <:> s)) 143 144 Master as Product of Factors: 145 poly_master_eq_root_factor_product 146 |- !r. FiniteField r ==> (master (CARD R) = PPROD (IMAGE factor R)) 147 poly_master_eq_root_factor_product_alt 148 |- !r. FiniteField r ==> (master (CARD R) = PPROD {X - c * |1| | c | c IN R}) 149 150 Subfield Conditions: 151 subfield_element_condition |- !r. FiniteField r ==> !s. s <<= r ==> 152 !x. x IN R ==> (x IN B <=> (x ** CARD B = x)) 153 subfield_poly_condition |- !r. FiniteField r ==> !s. s <<= r ==> 154 !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B))) 155 156 Sets of Monic Irreducible Polynomials: 157 monic_irreducibles_degree_def |- !r n. monic_irreducibles_degree r n = 158 {p | monic p /\ ipoly p /\ (deg p = n)} 159 monic_irreducibles_bounded_def |- !r n. monic_irreducibles_bounded r n = 160 BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n)) 161 monic_irreducibles_degree_member |- !r n p. p IN monic_irreducibles_degree r n <=> 162 monic p /\ ipoly p /\ (deg p = n) 163 monic_irreducibles_bounded_member |- !r n p. p IN monic_irreducibles_bounded r n <=> 164 monic p /\ ipoly p /\ deg p <= n /\ deg p divides n 165 monic_irreducibles_degree_finite |- !r. FINITE R /\ #0 IN R ==> 166 !n. FINITE (monic_irreducibles_degree r n) 167 monic_irreducibles_bounded_finite |- !r. FINITE R /\ #0 IN R ==> 168 !n. FINITE (monic_irreducibles_bounded r n) 169 monic_irreducibles_degree_0 |- !r. Field r ==> (monic_irreducibles_degree r 0 = {} 170 monic_irreducibles_degree_1 |- !r. Field r ==> (monic_irreducibles_degree r 1 = IMAGE factor R) 171 monic_irreducibles_bounded_0 |- !r. Field r ==> (monic_irreducibles_bounded r 0 = {}) 172 monic_irreducibles_bounded_1 |- !r. Field r ==> (monic_irreducibles_bounded r 1 = IMAGE factor R) 173 monic_irreducibles_degree_monic_irreducible_set 174 |- !r n. miset (monic_irreducibles_degree r n) 175 monic_irreducibles_degree_monic_set |- !r n. mset (monic_irreducibles_degree r n) 176 monic_irreducibles_degree_poly_set |- !r n. pset (monic_irreducibles_degree r n) 177 monic_irreducibles_degree_coprime_set |- !r. Field r ==> !n. pcoprime_set (monic_irreducibles_degree r n) 178 monic_irreducibles_bounded_coprime_set |- !r. Field r ==> !n. pcoprime_set (monic_irreducibles_bounded r n) 179 180 Product of Monic Irreducibles of the same degree: 181 monic_irreducibles_degree_prod_set_monic |- !r. FiniteRing r ==> !n. monic (Psi n) 182 monic_irreducibles_degree_prod_set_poly |- !r. FiniteRing r ==> !n. poly (Psi n) 183 monic_irreducibles_degree_prod_set_nonzero |- !r. FiniteRing r /\ #1 <> #0 ==> !n. Psi n <> |0| 184 185 Master Polynomial as Product of Monic Irreducibles: 186 poly_master_subfield_factors |- !r. FiniteField r ==> !s. s <<= r ==> !n. 0 < n ==> 187 (Master s (CARD B ** n) = poly_prod_set s (monic_irreducibles_bounded s n)) 188 poly_master_subfield_factors_alt |- !r s n. FiniteField r /\ s <<= r /\ 0 < n ==> 189 (master (CARD B ** n) = poly_prod_set s (monic_irreducibles_bounded s n)) 190 poly_master_monic_irreducible_factors |- !r. FiniteField r ==> !n. 0 < n ==> 191 (master (CARD R ** n) = PPROD (monic_irreducibles_bounded r n)) 192 poly_master_eq_irreducibles_product |- !r. FiniteField r ==> !s. s <<= r ==> 193 (master (CARD R) = poly_prod_set s (monic_irreducibles_bounded s (r <:> s))) 194 195 Counting Monic Irreducible Polynomials: 196 monic_irreducibles_count_def |- !r n. monic_irreducibles_count r n = CARD (monic_irreducibles_degree r n) 197 monic_irreducibles_degree_prod_set_deg 198 |- !r. FiniteRing r ==> !n. deg (Psi n) = n * monic_irreducibles_count r n 199 monic_irreducibles_degree_prod_set_deg_fun |- !r. FiniteRing r ==> 200 (deg o PPROD o monic_irreducibles_degree r = (\d. d * monic_irreducibles_count r d)) 201 monic_irreducibles_degree_disjoint 202 |- !r n m. n <> m ==> DISJOINT (monic_irreducibles_degree r n) (monic_irreducibles_degree r m) 203 monic_irreducibles_degree_pair_disjoint 204 |- !r n. PAIR_DISJOINT (IMAGE (monic_irreducibles_degree r) (divisors n)) 205 monic_irreducibles_degree_prod_set_divisor |- !r. FiniteField r ==> !p. monic p /\ ipoly p ==> 206 !n. p pdivides Psi n <=> p IN monic_irreducibles_degree r n 207 monic_irreducibles_degree_poly_prod_inj |- !r. FiniteField r ==> 208 !n. INJ PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) univ(:'a poly) 209 monic_irreducibles_degree_nonempty_inj |- !r s. FINITE s /\ 210 (!d. d IN s ==> monic_irreducibles_degree r d <> {}) ==> 211 INJ (monic_irreducibles_degree r) s univ(:'a poly -> bool) 212 monic_irreducibles_bounded_prod_set |- !r. FiniteField r ==> !n. PPROD (monic_irreducibles_bounded r n) = 213 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) 214 monic_irreducibles_bounded_prod_set_deg |- !r. FiniteField r ==> 215 !n. deg (PPROD (monic_irreducibles_bounded r n)) = 216 SIGMA (\d. d * monic_irreducibles_count r d) (divisors n) 217 218 Finite Field and Subfield Order: 219 finite_subfield_card_exp_eqn |- !r. FiniteField r ==> !s. s <<= r ==> !n. 0 < n ==> 220 (CARD B ** n = SIGMA (\d. d * monic_irreducibles_count s d) (divisors n)) 221 finite_field_card_exp_eqn |- !r. FiniteField r ==> !n. 0 < n ==> 222 (CARD R ** n = SIGMA (\d. d * monic_irreducibles_count r d) (divisors n)) 223 224 Roots of Master is a Subfield: 225 poly_master_roots_char_n_zero |- !r. FiniteField r ==> !n. #0 IN roots (master (char r ** n)) 226 poly_master_roots_add_root |- !r. FiniteField r ==> !n. (let p = master (char r ** n) in 227 !x y. x IN roots p /\ y IN roots p ==> x + y IN roots p) 228 poly_master_roots_sub_root |- !r. FiniteField r ==> !n. (let p = master (char r ** n) in 229 !x y. x IN roots p /\ y IN roots p ==> x - y IN roots p) 230 poly_master_roots_neg_root |- !r. FiniteField r ==> !n. (let p = master (char r ** n) in 231 !x. x IN roots p ==> -x IN roots p) 232 poly_master_roots_mult_root |- !r. Field r ==> !n. (let p = master (char r ** n) in 233 !x y. x IN roots p /\ y IN roots p ==> x * y IN roots p) 234 poly_master_roots_inv_root |- !r. Field r ==> !n. (let p = master (char r ** n) in 235 !x. x IN roots p /\ x <> #0 ==> |/ x IN roots p) 236 poly_master_roots_div_root |- !r. Field r ==> !n. (let p = master (char r ** n) in 237 !x y. x IN roots p /\ y IN roots p /\ y <> #0 ==> x * |/ y IN roots p) 238 poly_master_roots_sum_abelian_group 239 |- !r. FiniteField r ==> 240 !n. AbelianGroup (subset_field r (roots (master (char r ** n)))).sum 241 poly_master_roots_prod_abelian_group 242 |- !r. FiniteField r ==> !n. (let p = master (char r ** n) in 243 AbelianGroup ((subset_field r (roots p)).prod excluding (subset_field r (roots p)).sum.id)) 244 poly_master_roots_field |- !r. FiniteField r ==> 245 !n. Field (subset_field r (roots (master (char r ** n)))) 246 poly_master_roots_finite_field |- !r. FiniteField r ==> 247 !n. FiniteField (subset_field r (roots (master (char r ** n)))) 248 poly_master_roots_subfield |- !r. FiniteField r ==> 249 !n. subset_field r (roots (master (char r ** n))) <<= r 250 poly_master_roots_subfield_iso_field 251 |- !r. FiniteField r ==> 252 FieldIso I (subset_field r (roots (master (char r ** fdim r)))) r 253 poly_master_roots_subfield_isomorphism 254 |- !r. FiniteField r ==> 255 r =ff= subset_field r (roots (master (char r ** fdim r))) 256 257 Useful Results: 258 poly_master_subfield_eq_monic_irreducibles_prod_image 259 |- !r s n. FiniteField r /\ s <<= r /\ 0 < n ==> (master (CARD B ** n) = 260 poly_prod_image s (poly_prod_set s) (IMAGE (monic_irreducibles_degree s) (divisors n))) 261 poly_master_subfield_eq_monic_irreducibles_prod_image_alt_1 262 |- !r s n. FiniteField r /\ s <<= r /\ 0 < n ==> 263 (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d IN divisors n}) 264 poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2 265 |- !r s n. FiniteField r /\ s <<= r /\ 0 < n ==> 266 (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d divides n}) 267 poly_master_eq_monic_irreducibles_prod_image 268 |- !r. FiniteField r ==> !n. 0 < n ==> 269 (master (CARD R ** n) = PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n))) 270 poly_master_eq_monic_irreducibles_prod_image_alt_1 271 |- !r n. FiniteField r /\ 0 < n ==> 272 (master (CARD R ** n) = PPROD {Psi d | d IN divisors n}) 273 poly_master_eq_monic_irreducibles_prod_image_alt_2 274 |- !r n. FiniteField r /\ 0 < n ==> 275 (master (CARD R ** n) = PPROD {Psi d | d divides n}) 276 277 Monic Irreducible Products: 278 monic_irreducibles_degree_prod_set_image_monic_set 279 |- !r. FiniteRing r ==> 280 !n. mset (IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))) 281 monic_irreducibles_degree_prod_set_image_monic 282 |- !r. FiniteRing r ==> 283 !n. monic (PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))) 284 monic_irreducibles_degree_prod_set_image_poly 285 |- !r. FiniteRing r ==> 286 !n. poly (PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))) 287 monic_irreducibles_degree_prod_set_image_nonzero 288 |- !r. FiniteRing r /\ #1 <> #0 ==> 289 !n. PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)) <> |0| 290 291 Existence of Monic Irreducible by Master Polynomial: 292 monic_irreducibles_degree_prod_set_divides_master 293 |- !r. FiniteField r ==> !n. Psi n pdivides master (CARD R ** n) 294 poly_master_divides_monic_irreducibles_degree_prod_set_image 295 |- !r. FiniteField r ==> !n. 0 < n ==> 296 master (CARD R ** n) pdivides 297 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)) 298 monic_irreducibles_degree_prod_set_image_divides_master_image 299 |- !r. FiniteField r ==> !s. FINITE s ==> 300 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) s) pdivides 301 PPIMAGE (\n. master (CARD R ** n)) s 302 poly_monic_irreducible_exists_alt 303 |- !r. FiniteField r ==> !n. 0 < n ==> ?p. monic p /\ ipoly p /\ (deg p = n) 304 305 Finite Field Subgroup and Master Polynomial: 306 field_subgroup_master_roots |- !r g. FiniteField r /\ g <= f* ==> (roots (master (CARD G + 1)) = G UNION {#0}) 307 308 Finite Field Subgroup Field: 309 subgroup_field_def |- !r g. subgroup_field r g = 310 <|carrier := G UNION {#0}; 311 sum := <|carrier := G UNION {#0}; op := $+; id := #0|>; 312 prod := g including #0 313 |> 314 subgroup_field_property |- !r g. ((subgroup_field r g).carrier = G UNION {#0}) /\ 315 ((subgroup_field r g).sum.carrier = G UNION {#0}) /\ 316 ((subgroup_field r g).prod.carrier = G UNION {#0}) /\ 317 ((subgroup_field r g).sum.op = $+) /\ 318 ((subgroup_field r g).sum.id = #0) 319 subgroup_field_sum_property |- !r g. ((subgroup_field r g).sum.op = $+) /\ 320 ((subgroup_field r g).sum.id = #0) 321 subgroup_field_prod_property |- !r g. Field r /\ g <= f* ==> 322 ((subgroup_field r g).prod.op = $* ) /\ 323 ((subgroup_field r g).prod.id = #1) 324 subgroup_field_ids |- !r g. Field r /\ g <= f* ==> 325 ((subgroup_field r g).sum.id = #0) /\ 326 ((subgroup_field r g).prod.id = #1) 327 subgroup_field_card |- !r g. FiniteGroup g /\ #0 NOTIN G ==> 328 (CARD (subgroup_field r g).carrier = CARD G + 1) 329 subgroup_field_has_ids |- !r g. Field r /\ g <= f* ==> #0 IN G UNION {#0} /\ #1 IN G UNION {#0} 330 subgroup_field_element |- !r g. Field r /\ g <= f* ==> !x. x IN G UNION {#0} ==> x IN R 331 subgroup_field_mult_element |- !r g. Field r /\ g <= f* ==> 332 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x * y IN G UNION {#0} 333 subgroup_field_exp_element |- !r g. Field r /\ g <= f* ==> 334 !x. x IN G UNION {#0} ==> !n. x ** n IN G UNION {#0} 335 subgroup_field_inv_element |- !r g. Field r /\ g <= f* ==> !x. x IN G ==> |/ x IN G 336 337 Subgroup Field Additive Closure: 338 subgroup_field_element_iff_master_root |- !r g. FiniteField r /\ g <= f* ==> 339 !x. x IN G UNION {#0} <=> x IN R /\ (x ** (CARD G + 1) = x) 340 subgroup_field_add_element |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 341 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x + y IN G UNION {#0} 342 subgroup_field_sub_element |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 343 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x - y IN G UNION {#0} 344 subgroup_field_neg_element |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 345 !x. x IN G UNION {#0} ==> -x IN G UNION {#0} 346 347 Subgroup Field Properties: 348 subgroup_field_prod_abelian_monoid |- !r g. Field r /\ g <= f* ==> AbelianMonoid (subgroup_field r g).prod 349 subgroup_field_prod_monoid |- !r g. Field r /\ g <= f* ==> Monoid (subgroup_field r g).prod 350 subgroup_field_sum_abelian_group |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 351 AbelianGroup (subgroup_field r g).sum 352 subgroup_field_sum_group |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 353 Group (subgroup_field r g).sum 354 subgroup_field_ring |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 355 Ring (subgroup_field r g) 356 subgroup_field_field |- !r g. FiniteField r /\ g <= f* ==> !n. (CARD G = char r ** n - 1) ==> 357 Field (subgroup_field r g) 358 subgroup_field_subfield |- !r g. Field r /\ g <= f* ==> subfield (subgroup_field r g) r 359 360 Subfield Classification: 361 finite_field_subfield_gives_subgroup 362 |- !r s. FiniteField r /\ s <<= r ==> ?g. g <= f* /\ (CARD G = char r ** fdim s - 1) 363 finite_field_subgroup_gives_subfield 364 |- !r. FiniteField r ==> !g n. g <= f* /\ (CARD G = char r ** n - 1) ==> 365 ?s. s <<= r /\ (fdim s = n) 366 finite_field_subfield_exists_iff_subgroup_exists 367 |- !r. FiniteField r ==> !n. (?s. s <<= r /\ (fdim s = n)) <=> 368 ?g. g <= f* /\ (CARD G = char r ** n - 1) 369 finite_field_subfield_exists_condition 370 |- !r. FiniteField r ==> !n. (?s. s <<= r /\ (fdim s = n)) <=> n divides fdim r 371 372*) 373 374(* ------------------------------------------------------------------------- *) 375(* Helper Theorems *) 376(* ------------------------------------------------------------------------- *) 377 378(* ------------------------------------------------------------------------- *) 379(* Master Polynomial: X ** (CARD R) - X and its roots. *) 380(* ------------------------------------------------------------------------- *) 381 382(* Theorem: FiniteField r ==> !x. x IN R ==> root (master (CARD R)) x *) 383(* Proof: 384 FiniteField r ==> Field r by FiniteField_def 385 root (master (CARD R)) x 386 <=> x ** (CARD R) = x by poly_master_root 387 <=> T by finite_field_fermat_thm 388*) 389val poly_master_root_all = store_thm( 390 "poly_master_root_all", 391 ``!r:'a field. FiniteField r ==> !x. x IN R ==> root (master (CARD R)) x``, 392 rw[FiniteField_def, poly_master_root, finite_field_fermat_thm]); 393 394(* Theorem: FiniteField r ==> (roots (master (CARD R)) = R) *) 395(* Proof: 396 By poly_roots_def, this is to show: 397 {x | x IN R /\ root (X ** CARD R - X) x} = R 398 which is true by poly_master_root_all. 399*) 400val poly_master_roots_all = store_thm( 401 "poly_master_roots_all", 402 ``!r:'a field. FiniteField r ==> (roots (master (CARD R)) = R)``, 403 rw_tac std_ss[poly_roots_def, GSPECIFICATION, EXTENSION] >> 404 metis_tac[poly_master_root_all]); 405 406(* Theorem: s <<= r ==> !x. x IN B ==> !n. poly_root s (Master s n) x <=> root (master n) x *) 407(* Proof: 408 Note x IN B == x IN R by subfield_element 409 Given poly_root s (Master s n) x 410 <=> s.prod.exp x n = x by poly_master_root 411 <=> x ** n = x by subfield_exp 412 <=> root (master n) x by poly_master_root 413*) 414val poly_master_subfield_root = store_thm( 415 "poly_master_subfield_root", 416 ``!(r s):'a field. s <<= r ==> !x. x IN B ==> !n. poly_root s (Master s n) x <=> root (master n) x``, 417 metis_tac[subfield_element, poly_master_root, subfield_exp, field_is_ring]); 418 419(* Theorem: FiniteField r ==> 420 !n. 0 < n ==> pgcd (master (CARD R ** n)) (diff (master (CARD R ** n))) ~~ |1| *) 421(* Proof: 422 Let b = CARD R ** n, p = master b, c = char r. 423 Then poly p by poly_master_poly 424 and prime c by finite_field_char 425 and 1 < c by ONE_LT_PRIME, 426 also ?m. 0 < m /\ (CARD R = c ** m by finite_field_card 427 thus b = (c ** m) ** n 428 = c ** (m * n) by EXP_EXP_MULT 429 Note m * n <> 0 by MULT_EQ_0, m <> 0 430 Thus diff p = -|1| by poly_diff_master_char_exp, m * n <> 0 431 Now upoly |1| by poly_unit_one 432 and upoly (-|1|) by poly_unit_neg 433 Hence pgcd p (diff p) 434 = pgcd p (-|1|) ~~ |1| by poly_gcd_unit 435*) 436val poly_master_coprime_diff = store_thm( 437 "poly_master_coprime_diff", 438 ``!r:'a field. FiniteField r ==> 439 !n. 0 < n ==> pgcd (master (CARD R ** n)) (diff (master (CARD R ** n))) ~~ |1|``, 440 rpt (stripDup[FiniteField_def]) >> 441 `Ring r /\ #1 <> #0` by rw[] >> 442 qabbrev_tac `b = CARD R ** n` >> 443 qabbrev_tac `p = master b` >> 444 qabbrev_tac `c = char r` >> 445 `1 < c` by rw[finite_field_char, ONE_LT_PRIME, Abbr`c`] >> 446 `?m. 0 < m /\ (CARD R = c ** m)` by rw[finite_field_card, Abbr`c`] >> 447 `b = c ** (m * n)` by rw[EXP_EXP_MULT, Abbr`b`] >> 448 `m * n <> 0` by metis_tac[MULT_EQ_0, NOT_ZERO_LT_ZERO] >> 449 `diff p = -|1|` by rw[poly_diff_master_char_exp, Abbr`p`, Abbr`c`] >> 450 `upoly |1|` by rw[poly_unit_one] >> 451 `upoly (-|1|)` by rw[poly_unit_neg] >> 452 rw[poly_gcd_unit, Abbr`p`]); 453 454(* Theorem: FiniteField r ==> !n. monic (PPIMAGE (\k. master (CARD R ** k)) (natural n)) *) 455(* Proof: 456 Let m = CARD R. 457 Then 1 < m by finite_field_card_gt_1 458 Let f = \k. master (m ** k), s = IMAGE f (natural n). 459 Note FINITE (natural n) by natural_finite 460 so FINITE s by IMAGE_FINITE 461 Note !k. k IN (natural n) 462 ==> 0 < k by natural_element 463 ==> 1 < m ** k by ONE_LT_EXP, 1 < m 464 so mset s by IN_IMAGE, poly_master_monic, 1 < m ** k for k IN (natural n) 465 Thus monic (PPROD s) by poly_monic_prod_set_monic 466*) 467val poly_master_prod_set_over_natural_monic = store_thm( 468 "poly_master_prod_set_over_natural_monic", 469 ``!r:'a field. FiniteField r ==> !n. monic (PPIMAGE (\k. master (CARD R ** k)) (natural n))``, 470 rpt (stripDup[FiniteField_def]) >> 471 `Ring r /\ #1 <> #0` by rw[] >> 472 qabbrev_tac `m = CARD R` >> 473 `1 < m` by rw[finite_field_card_gt_1, Abbr`m`] >> 474 qabbrev_tac `f = \k. master (m ** k)` >> 475 qabbrev_tac `s = IMAGE f (natural n)` >> 476 `FINITE (natural n)` by rw[natural_finite] >> 477 `FINITE s` by rw[Abbr`s`] >> 478 `mset s` by metis_tac[IN_IMAGE, poly_master_monic, natural_element, ONE_LT_EXP] >> 479 rw[poly_monic_prod_set_monic]); 480 481(* Theorem: FiniteField r ==> !n. poly (PPIMAGE (\k. master (CARD R ** k)) (natural n)) *) 482(* Proof: by poly_master_prod_set_over_natural_monic, poly_monic_poly *) 483val poly_master_prod_set_over_natural_poly = store_thm( 484 "poly_master_prod_set_over_natural_poly", 485 ``!r:'a field. FiniteField r ==> !n. poly (PPIMAGE (\k. master (CARD R ** k)) (natural n))``, 486 rw_tac std_ss[poly_master_prod_set_over_natural_monic, poly_monic_poly]); 487 488(* Theorem: FiniteField r ==> !n. PPIMAGE (\k. master (CARD R ** k)) (natural n) <> |0| *) 489(* Proof: by poly_master_prod_set_over_natural_monic, poly_monic_nonzero *) 490val poly_master_prod_set_over_natural_nonzero = store_thm( 491 "poly_master_prod_set_over_natural_nonzero", 492 ``!r:'a field. FiniteField r ==> !n. PPIMAGE (\k. master (CARD R ** k)) (natural n) <> |0|``, 493 rw_tac std_ss[poly_master_prod_set_over_natural_monic, poly_monic_nonzero, finite_field_is_field, field_one_ne_zero]); 494 495(* Theorem: FiniteField r ==> let m = CARD R in 496 !n. deg (PPIMAGE (\k. master (m ** k)) (natural n)) = m * (m ** n - 1) DIV (m - 1) *) 497(* Proof: 498 Let m = CARD R. 499 Then 1 < m by finite_field_card_gt_1 500 Let f = \k. master (m ** k), s = IMAGE f (natural n). 501 Note FINITE (natural n) by natural_finite 502 so FINITE s by IMAGE_FINITE 503 also mset s by IN_IMAGE, poly_master_monic, natural_element, ONE_LT_EXP 504 505 Claim: INJ f (natural n) UNIV 506 Proof: by INJ_DEF, this is to show: 507 (1) k IN natural n ==> master (m ** k) IN univ(:'a poly) 508 True by poly_master_poly, IN_UNIV 509 (2) k IN natural n /\ k' IN natural n /\ master (m ** k) = master (m ** k') ==> k = k' 510 Note m ** k = m ** k' by poly_master_eq 511 ==> k = k' by EXP_BASE_INJECTIVE, 1 < m 512 513 Claim: !k. k IN (natural n) ==> ((deg o f) k = (\k. m ** k) k) 514 Proof: By FUN_EQ_THM, this is to show: 515 k IN natural n ==> deg (master (m ** k)) = m ** k 516 Note 0 < k by natural_element 517 so 1 < m ** k by ONE_LT_EXP, 1 < m 518 Thus true by poly_master_deg, 1 < m ** k 519 520 deg (PPROD s) 521 = SIGMA deg s by poly_monic_prod_set_deg, mset s 522 = SIGMA deg (IMAGE f (natural n)) by notation 523 = SIGMA (deg o f) (natural n) by sum_image_by_composition 524 = SIGMA (\k. m ** k) (natural n) by SIGMA_CONG 525 = m * (m ** n - 1) DIV (m - 1) by sigma_geometric_natural, 1 < m 526*) 527val poly_master_prod_set_over_natural_deg = store_thm( 528 "poly_master_prod_set_over_natural_deg", 529 ``!r:'a field. FiniteField r ==> let m = CARD R in 530 !n. deg (PPIMAGE (\k. master (m ** k)) (natural n)) = m * (m ** n - 1) DIV (m - 1)``, 531 rpt (stripDup[FiniteField_def]) >> 532 `Ring r /\ #1 <> #0` by rw[] >> 533 rw_tac std_ss[] >> 534 `1 < m` by rw[finite_field_card_gt_1, Abbr`m`] >> 535 qabbrev_tac `f = \k. master (m ** k)` >> 536 qabbrev_tac `s = IMAGE f (natural n)` >> 537 `FINITE (natural n)` by rw[natural_finite] >> 538 `FINITE s` by rw[Abbr`s`] >> 539 `!k. f k = master (m ** k)` by rw[Abbr`f`] >> 540 `mset s` by metis_tac[IN_IMAGE, poly_master_monic, natural_element, ONE_LT_EXP] >> 541 `INJ f (natural n) UNIV` by 542 (rw_tac std_ss[INJ_DEF, Abbr`f`] >- 543 rw[poly_master_poly] >> 544 `m ** k = m ** k'` by metis_tac[poly_master_eq] >> 545 metis_tac[EXP_BASE_INJECTIVE] 546 ) >> 547 `!k. k IN (natural n) ==> ((deg o f) k = (\k. m ** k) k)` by 548 (rw_tac std_ss[FUN_EQ_THM, Abbr`f`] >> 549 metis_tac[poly_master_deg, natural_element, ONE_LT_EXP]) >> 550 `deg (PPROD s) = SIGMA deg s` by rw[poly_monic_prod_set_deg] >> 551 `_ = SIGMA deg (IMAGE f (natural n))` by rw[Abbr`s`] >> 552 `_ = SIGMA (deg o f) (natural n)` by rw[sum_image_by_composition] >> 553 `_ = SIGMA (\k. m ** k) (natural n)` by rw[SIGMA_CONG] >> 554 `_ = m * (m ** n - 1) DIV (m - 1)` by rw[sigma_geometric_natural] >> 555 rw[]); 556 557(* ------------------------------------------------------------------------- *) 558(* Irreducible Factors of Master Polynomial *) 559(* ------------------------------------------------------------------------- *) 560 561(* Theorem: Ring r ==> !p. ulead p ==> !n. p pdivides (master n) <=> (X ** n == X) (pm p) *) 562(* Proof: 563 p pdivides (master n) 564 <=> master n % p = |0| by poly_divides_alt 565 <=> (X ** n - X) % p = |0| by notation 566 <=> (X ** n) % p = X % p by poly_mod_eq 567 <=> (X ** n == X) (pm p) by pmod_def_alt 568*) 569val poly_ulead_divides_master_condition = store_thm( 570 "poly_ulead_divides_master_condition", 571 ``!r:'a ring. Ring r ==> 572 !p. ulead p ==> !n. p pdivides (master n) <=> (X ** n == X) (pm p)``, 573 rpt strip_tac >> 574 `poly X /\ poly (master n)` by rw[] >> 575 `p pdivides (master n) <=> (master n % p = |0|)` by rw_tac std_ss[poly_divides_alt] >> 576 `_ = ((X ** n) % p = X % p)` by rw_tac std_ss[poly_mod_eq, poly_exp_poly] >> 577 `_ = (X ** n == X) (pm p)` by rw_tac std_ss[pmod_def_alt] >> 578 rw[]); 579 580(* Theorem: FiniteField r ==> !p. monic p /\ ipoly p ==> p pdivides (master (CARD R ** deg p)) *) 581(* Proof: 582 Since FieldField r /\ monic p /\ ipoly p 583 ==> FiniteField (PolyModRing r p) by poly_mod_irreducible_finite_field 584 and (X % p) IN (PolyModRing r p).carrier by poly_mod_ring_element 585 Hence X % p 586 = (PolyModRing r p).prod.exp (X % p) (CARD (PolyModRing r p).carrier) by finite_field_fermat_thm 587 = (X ** (CARD (PolyModRing r p).carrier)) % p by poly_mod_field_exp 588 = (X ** (CARD R ** deg p)) % p by poly_mod_irreducible_field_card 589 Giving (X ** (CARD R ** deg p) == X) (pm p) by pmod_def_alt 590 or p pdivides (master (CARD R ** deg p)) by poly_ulead_divides_master_condition 591*) 592val poly_irreducible_divides_master = store_thm( 593 "poly_irreducible_divides_master", 594 ``!r:'a field. FiniteField r ==> !p. monic p /\ ipoly p ==> p pdivides (master (CARD R ** deg p))``, 595 rpt (stripDup[FiniteField_def]) >> 596 `pmonic p` by rw[poly_monic_irreducible_property] >> 597 `poly X /\ poly (X % p) /\ deg (X % p) < deg p` by rw[poly_deg_mod_less] >> 598 `FiniteField (PolyModRing r p)` by rw[poly_mod_irreducible_finite_field] >> 599 `(X % p) IN (PolyModRing r p).carrier` by rw[poly_mod_ring_element] >> 600 `X % p = (PolyModRing r p).prod.exp (X % p) (CARD (PolyModRing r p).carrier)` by rw[finite_field_fermat_thm] >> 601 `_ = X ** (CARD (PolyModRing r p).carrier) % p` by rw[poly_mod_field_exp] >> 602 `_ = X ** (CARD R ** deg p) % p` by metis_tac[poly_mod_irreducible_field_card] >> 603 `(X ** (CARD R ** deg p) == X) (pm p)` by rw[pmod_def_alt] >> 604 rw[poly_ulead_divides_master_condition]); 605 606(* This is a small milestone theorem. The big one is: poly_irreducible_master_divisibility *) 607 608(* Theorem: Field r ==> !p. monic p /\ ipoly p ==> !x. x IN (PolyModRing r p).carrier ==> 609 !n. poly_root (PolyModRing r p) (Master (PolyModRing r p) n) x <=> (x ** n == x) (pm p) *) 610(* Proof: 611 Since monic p /\ ipoly p ==> pmonic p by poly_monic_irreducible_property 612 then Ring (PolyModRing r p) by poly_mod_ring_ring, pmonic p 613 Also x IN (PolyModRing r p).carrier 614 ==> poly x /\ deg x < deg p by poly_mod_ring_element 615 thus x % p = x by poly_mod_less 616 Apply: poly_master_root |> ISPEC ``PolyModRing r z``; 617 poly_root (PolyModRing r p) (Master (PolyModRing r p) n) x 618 <=> (PolyModRing r p).prod.exp x n = x by poly_master_root 619 <=> (PolyModRing r p).prod.exp (x % p) n = (x % p) by above 620 <=> x ** n % p = x % p by poly_mod_field_exp 621 <=> (x ** n == x) (pm p) by pmod_def_alt 622*) 623val poly_mod_master_root_condition = store_thm( 624 "poly_mod_master_root_condition", 625 ``!r:'a field. Field r ==> !p. monic p /\ ipoly p ==> !x. x IN (PolyModRing r p).carrier ==> 626 !n. poly_root (PolyModRing r p) (Master (PolyModRing r p) n) x <=> (x ** n == x) (pm p)``, 627 rpt strip_tac >> 628 `pmonic p` by rw[poly_monic_irreducible_property] >> 629 `Ring r /\ Ring (PolyModRing r p)` by rw[poly_mod_ring_ring] >> 630 `poly x /\ deg x < deg p` by metis_tac[poly_mod_ring_element, NOT_ZERO] >> 631 `x % p = x` by rw[poly_mod_less] >> 632 `!n. (PolyModRing r p).prod.exp (x % p) n = (x ** n) % p` by rw[poly_mod_field_exp] >> 633 metis_tac[poly_master_root, pmod_def_alt]); 634 635(* Theorem: Ring r ==> !p. pmonic p ==> 636 !f. poly_fun f ==> !n. (poly_sum (GENLIST f n)) % p = poly_sum (GENLIST (\k. (f k) % p) n) % p *) 637(* Proof: 638 By induction on n. 639 Base case: poly_sum (GENLIST f 0) % p = poly_sum (GENLIST (\k. f k % p) 0) % p 640 poly_sum (GENLIST f 0) % p 641 = poly_sum [] % p by GENLIST_0 642 = poly_sum (GENLIST (\k. f k % p) 0) by GENLIST_0 643 Step case: poly_sum (GENLIST f n) % p = poly_sum (GENLIST (\k. f k % p) n) % p ==> 644 poly_sum (GENLIST f (SUC n)) % p = poly_sum (GENLIST (\k. f k % p) (SUC n)) % p 645 poly_sum (GENLIST f (SUC n)) % p 646 = (poly_sum (GENLIST f n) + f n) % p by poly_sum_decompose_last 647 = (poly_sum (GENLIST f n) % p + (f n) % p) % p by poly_mod_add, ulead p 648 = (poly_sum (GENLIST (\k. f k % p) n) % p + (f n) % p) % p by induction hypothesis 649 = (poly_sum (GENLIST (\k. f k % p) n) + (f n) % p) % p by poly_mod_mod, ulead p 650 = poly_sum (GENLIST (\k. f k % p) (SUC n)) % p by poly_sum_decompose_last 651*) 652val poly_mod_poly_sum_gen = store_thm( 653 "poly_mod_poly_sum_gen", 654 ``!r:'a ring. Ring r ==> !p. ulead p ==> 655 !f. poly_fun f ==> !n. (poly_sum (GENLIST f n)) % p = poly_sum (GENLIST (\k. (f k) % p) n) % p``, 656 rpt strip_tac >> 657 Induct_on `n` >- 658 rw_tac std_ss[GENLIST_0] >> 659 `poly (poly_sum (GENLIST f n)) /\ poly (f n)` by rw[] >> 660 `poly_fun ((\k. f k % p))` by rw[poly_mod_poly, poly_ring_element] >> 661 `poly (poly_sum (GENLIST (\k. f k % p) n)) /\ poly ((f n) % p)` by rw[poly_mod_poly] >> 662 `poly_sum (GENLIST f (SUC n)) % p = (poly_sum (GENLIST f n) + f n) % p` by rw_tac std_ss[poly_sum_decompose_last] >> 663 `_ = (poly_sum (GENLIST f n) % p + (f n) % p) % p` by rw_tac std_ss[poly_mod_add] >> 664 `_ = (poly_sum (GENLIST (\k. f k % p) n) % p + (f n) % p) % p` by rw[] >> 665 `_ = (poly_sum (GENLIST (\k. f k % p) n) % p + ((f n) % p) % p) % p` by rw_tac std_ss[poly_mod_mod] >> 666 `_ = (poly_sum (GENLIST (\k. f k % p) n) + (f n) % p) % p` by rw_tac std_ss[poly_mod_add, poly_mod_poly] >> 667 `_ = poly_sum (GENLIST (\k. f k % p) (SUC n)) % p` by rw_tac std_ss[poly_sum_decompose_last] >> 668 rw[]); 669 670(* The following theorem extends: 671> poly_irreducible_divides_master; 672val it = |- !r. FiniteField r ==> !p. monic p /\ ipoly p ==> p pdivides master (CARD R ** deg p): thm 673to an iff-condition, making use of: 674> poly_master_divisibility; 675val it = |- !r. Field r ==> !k. 1 < k ==> !n m. master (k ** n) pdivides master (k ** m) <=> n divides m: thm 676> poly_master_gcd_identity; 677val it = |- !r. Field r ==> !k n m. pgcd (master (k ** n)) (master (k ** m)) ~~ master (k ** gcd n m): thm 678*) 679 680(* This is the core part of poly_irreducible_master_divisibility. *) 681 682(* Theorem: FiniteField r ==> !p. monic p /\ ipoly p ==> 683 !n. p pdivides (master (CARD R ** n)) ==> 684 (PolyModRing r p).carrier SUBSET poly_roots (PolyModRing r p) (Master ((PolyModRing r p)) (CARD R ** n)) *) 685(* Proof: 686 Let s = PolyModRing r p, b = CARD R ** n. 687 By SUBSET_DEF, poly_roots_member, this is to show: 688 !x. x IN s.carrier ==> poly_root s (Master s b) x 689 690 Note x IN s.carrier ==> poly x by poly_mod_ring_element 691 and pmonic p by poly_monic_irreducible_property 692 Also poly_fun (\k. x ' k * X ** k) by poly_ring_element 693 and poly_fun (\k. x ' k * (X ** b) ** k) by poly_ring_element 694 Now p pdivides (master b) by given 695 so (X ** b == X) (pm p) by poly_ulead_divides_master_condition 696 697 Let c = char r 698 Then ?m. 0 < m /\ (CARD R = c ** m) by finite_field_card 699 and b = (CARD R) ** n = c ** (m * n) by EXP_EXP_MULT 700 Also prime c by finite_field_char, FiniteField r 701 and rfun (\k. x ' k) by poly_coeff_ring_fun 702 and poly (X % p) by poly_mod_poly, pmonic p 703 704 x ** b % p 705 = (poly_sum (GENLIST (\k. x ' k * X ** k) (SUC (deg x)))) ** b % p by poly_eq_poly_sum 706 = poly_sum (GENLIST (\k. (x ' k * X ** k) ** b) (SUC (deg x))) % p by poly_sum_freshman_all, b = c ** (m * n) 707 = poly_sum (GENLIST (\k. (x ' k) ** b * (X ** k) ** b) (SUC (deg x))) % p by poly_cmult_exp 708 = poly_sum (GENLIST (\k. (x ' k) * (X ** k) ** b) (SUC (deg x))) % p by finite_field_fermat_all, b = (CARD R) ** n 709 = poly_sum (GENLIST (\k. x ' k * (X ** b) ** k) (SUC (deg x))) % p by poly_exp_mult_comm] 710 = poly_sum (GENLIST (\k. (x ' k * (X ** b) ** k) % p) (SUC (deg x))) % p by poly_mod_poly_sum_gen 711 = poly_sum (GENLIST (\k. (x ' k * ((X ** b) ** k % p)) % p) (SUC (deg x))) % p by poly_mod_cmult 712 = poly_sum (GENLIST (\k. (x ' k * (((X ** b) % p) ** k % p)) % p) (SUC (deg x))) % p by poly_mod_exp 713 = poly_sum (GENLIST (\k. (x ' k * ((X % p) ** k % p)) % p) (SUC (deg x))) % p by pmod_def_alt, (X ** b == X) (pm p) 714 = poly_sum (GENLIST (\k. (x ' k * (X ** k % p)) % p) (SUC (deg x))) % p by poly_mod_exp 715 = poly_sum (GENLIST (\k. (x ' k * X ** k) % p) (SUC (deg x))) % p by poly_mod_cmult 716 = poly_sum (GENLIST (\k. x ' k * X ** k) (SUC (deg x))) % p by poly_mod_poly_sum_gen 717 = x % p by poly_eq_poly_sum 718 719 Therefore, (x ** b == x) (pm p) by pmod_def_alt, x ** b % p = x % p 720 Hence poly_root s (Master s b) x by poly_mod_master_root_condition 721*) 722val poly_irreducible_master_factor_all_roots = store_thm( 723 "poly_irreducible_master_factor_all_roots", 724 ``!r:'a field. FiniteField r ==> !p. monic p /\ ipoly p ==> 725 !n. p pdivides (master (CARD R ** n)) ==> 726 (PolyModRing r p).carrier SUBSET poly_roots (PolyModRing r p) (Master ((PolyModRing r p)) (CARD R ** n))``, 727 rpt (stripDup[FiniteField_def]) >> 728 `Ring r /\ #1 <> #0` by rw[] >> 729 `poly X /\ poly |1| /\ !k. poly (X ** k)` by rw[] >> 730 qabbrev_tac `s = PolyModRing r p` >> 731 qabbrev_tac `b = CARD R ** n` >> 732 rw_tac std_ss[SUBSET_DEF, poly_roots_member] >> 733 `poly x` by metis_tac[poly_mod_ring_element] >> 734 `pmonic p` by rw[poly_monic_irreducible_property] >> 735 `poly_fun (\k. x ' k * X ** k)` by rw[poly_ring_element] >> 736 `poly_fun (\k. x ' k * (X ** b) ** k)` by rw[poly_ring_element] >> 737 `(X ** b == X) (pm p)` by rw[GSYM poly_ulead_divides_master_condition] >> 738 qabbrev_tac `c = char r` >> 739 `?m. 0 < m /\ (CARD R = c ** m)` by rw[finite_field_card, Abbr`c`] >> 740 `b = c ** (m * n)` by rw[EXP_EXP_MULT, Abbr`b`] >> 741 `prime c` by rw[finite_field_char, Abbr`c`] >> 742 `rfun (\k. x ' k)` by rw[poly_coeff_ring_fun] >> 743 `poly (X % p)` by rw[] >> 744 `x ** b % p = (poly_sum (GENLIST (\k. x ' k * X ** k) (SUC (deg x)))) ** b % p` by rw[GSYM poly_eq_poly_sum] >> 745 `_ = poly_sum (GENLIST (\k. (x ' k * X ** k) ** b) (SUC (deg x))) % p` by rw[poly_sum_freshman_all, Abbr`c`] >> 746 `_ = poly_sum (GENLIST (\k. (x ' k) ** b * (X ** k) ** b) (SUC (deg x))) % p` by rw[poly_cmult_exp] >> 747 `_ = poly_sum (GENLIST (\k. (x ' k) * (X ** k) ** b) (SUC (deg x))) % p` by rw[finite_field_fermat_all, Abbr`b`] >> 748 `_ = poly_sum (GENLIST (\k. x ' k * (X ** b) ** k) (SUC (deg x))) % p` by rw_tac std_ss[poly_exp_mult_comm] >> 749 `_ = poly_sum (GENLIST (\k. (x ' k * (X ** b) ** k) % p) (SUC (deg x))) % p` by rw_tac std_ss[poly_mod_poly_sum_gen, Abbr`b`] >> 750 `_ = poly_sum (GENLIST (\k. (x ' k * ((X ** b) ** k % p)) % p) (SUC (deg x))) % p` by rw[GSYM poly_mod_cmult] >> 751 `_ = poly_sum (GENLIST (\k. (x ' k * (((X ** b) % p) ** k % p)) % p) (SUC (deg x))) % p` by rw[GSYM poly_mod_exp] >> 752 `_ = poly_sum (GENLIST (\k. (x ' k * ((X % p) ** k % p)) % p) (SUC (deg x))) % p` by metis_tac[pmod_def_alt] >> 753 `_ = poly_sum (GENLIST (\k. (x ' k * (X ** k % p)) % p) (SUC (deg x))) % p` by rw[GSYM poly_mod_exp] >> 754 `_ = poly_sum (GENLIST (\k. (x ' k * X ** k) % p) (SUC (deg x))) % p` by rw[GSYM poly_mod_cmult] >> 755 `_ = poly_sum (GENLIST (\k. x ' k * X ** k) (SUC (deg x))) % p` by rw[GSYM poly_mod_poly_sum_gen] >> 756 `_ = x % p` by metis_tac[poly_eq_poly_sum] >> 757 `(x ** b == x) (pm p)` by rw[pmod_def_alt] >> 758 rw[poly_mod_master_root_condition, Abbr`s`]); 759 760(* This is a simple consequence of the above theorem *) 761 762(* Theorem: FiniteField r ==> !p. monic p /\ ipoly p ==> 763 !n. 0 < n /\ p pdivides (master (CARD R ** n)) ==> deg p <= n *) 764(* Proof: 765 Step 1: show (CARD R) ** n <> 1 766 Note 1 < CARD R by finite_field_card_gt_1 767 so 1 < CARD R ** n by ONE_LT_EXP, 0 < n 768 or CARD R ** n <> 1 by arithmetic 769 770 Step 2: Apply poly_irreducible_master_factor_all_roots 771 Let s = PolyModRing r p, t = Master s (CARD R ** n). 772 Note FiniteField s by poly_mod_irreducible_finite_field 773 so Field s by finite_field_is_field 774 ==> s.carrier SUBSET poly_roots s t by poly_irreducible_master_factor_all_roots 775 776 Step 3: Apply poly_roots_count 777 Note Poly s t by poly_master_poly 778 and t <> poly_zero s by poly_master_eq_zero, field_one_ne_zero 779 Thus FINITE (poly_roots s t) by poly_roots_finite, t <> poly_zero s 780 ==> CARD s.carrier <= CARD (poly_roots s t) by CARD_SUBSET 781 But CARD (poly_roots s t) <= poly_deg s t by poly_roots_count 782 783 Step 4: Compute CARD s.carrier and poly_deg s t 784 Let d = deg p. 785 Then 0 < d by poly_irreducible_deg_nonzero 786 and CARD s.carrier = CARD R ** d by poly_mod_ring_card, 0 < d 787 also poly_deg s t = CARD R ** n by poly_master_deg, 1 < CARD R ** n 788 789 Thus CARD R ** d <= CARD R ** n by LESS_EQ_TRANS, from 3 and 4. 790 or d <= n by EXP_BASE_LE_MONO, 1 < CARD R 791*) 792val poly_irreducible_master_factor_deg = store_thm( 793 "poly_irreducible_master_factor_deg", 794 ``!r:'a field. FiniteField r ==> !p. monic p /\ ipoly p ==> 795 !n. 0 < n /\ p pdivides (master (CARD R ** n)) ==> deg p <= n``, 796 rpt (stripDup[FiniteField_def]) >> 797 `1 < CARD R` by rw[finite_field_card_gt_1] >> 798 `1 < CARD R ** n` by rw[ONE_LT_EXP] >> 799 `CARD R ** n <> 1 /\ n <> 0` by decide_tac >> 800 qabbrev_tac `s = PolyModRing r p` >> 801 qabbrev_tac `t = Master s (CARD R ** n)` >> 802 `FiniteField s` by rw[poly_mod_irreducible_finite_field, Abbr`s`] >> 803 `Field s /\ Ring s /\ Ring r` by rw[finite_field_is_field] >> 804 `s.carrier SUBSET poly_roots s t` by rw[poly_irreducible_master_factor_all_roots, Abbr`s`, Abbr`t`] >> 805 `Poly s t` by rw[Abbr`t`] >> 806 `t <> poly_zero s` by metis_tac[poly_master_eq_zero, field_one_ne_zero] >> 807 `FINITE (poly_roots s t)` by rw[poly_roots_finite] >> 808 `CARD s.carrier <= CARD (poly_roots s t)` by rw[CARD_SUBSET] >> 809 `CARD (poly_roots s t) <= poly_deg s t` by rw[poly_roots_count] >> 810 qabbrev_tac `d = deg p` >> 811 `0 < d` by rw[poly_irreducible_deg_nonzero, Abbr`d`] >> 812 `CARD s.carrier = CARD R ** d` by metis_tac[poly_mod_ring_card, FiniteRing_def] >> 813 `poly_deg s t = CARD R ** n` by metis_tac[poly_master_deg, field_one_ne_zero] >> 814 `CARD R ** d <= CARD R ** n` by metis_tac[LESS_EQ_TRANS] >> 815 metis_tac[EXP_BASE_LE_MONO]); 816 817(* Theorem: FiniteField r ==> !p. monic p /\ ipoly p ==> 818 !n. p pdivides (master (CARD R ** n)) <=> (deg p) divides n *) 819(* Proof: 820 If part: p pdivides (master (CARD R ** n)) ==> (deg p) divides n 821 822 Step 1: Show p pdivides master (CARD R ** (gcd d n)). 823 Method: By poly_master_gcd_identity. 824 825 Let d = deg p, u = master (CARD R ** d), v = master (CARD R ** n) 826 Since p pdivides u by poly_irreducible_divides_master 827 and p pdivides v by given 828 hence p pdivides (pgcd u v) by poly_gcd_is_gcd 829 But pgcd u v 830 = pgcd (master (CARD R ** d)) (master (CARD R ** n)) 831 ~~ master (CARD R ** (gcd d n)) by poly_master_gcd_identity 832 Let e = gcd d n, q = master (CARD R ** e) 833 Then pgcd u v ~~ q by poly_master_gcd_identity 834 and p pdivides q by poly_unit_eq_divisor, poly_gcd_poly, poly_master_poly 835 836 Step 2: Show e = gcd d n = d, so that d divides n. 837 Method: By d <= e, and e <= d, so e = d. 838 839 Note 0 < e by GCD_EQ_0, 0 < d 840 Then d <= e by poly_irreducible_master_factor_deg 841 But e divides d by GCD_IS_GREATEST_COMMON_DIVISOR 842 so e <= d by DIVIDES_LE, 0 < d 843 Hence e = d by EQ_LESS_EQ 844 or d divides n by divides_iff_gcd_fix 845 846 Only-if part: (deg p) divides n ==> p pdivides (master (CARD R ** n)) 847 Let d = deg p, u = master (CARD R ** d), v = master (CARD R ** n) 848 Since p pdivides u by poly_irreducible_divides_master 849 and u pdivides v by poly_master_divisibility, d divides n 850 hence p pdivides v by poly_divides_transitive 851*) 852val poly_irreducible_master_divisibility = store_thm( 853 "poly_irreducible_master_divisibility", 854 ``!r:'a field. FiniteField r ==> !p. monic p /\ ipoly p ==> 855 !n. p pdivides (master (CARD R ** n)) <=> (deg p) divides n``, 856 rpt (stripDup[FiniteField_def]) >> 857 `Ring r` by rw[] >> 858 qabbrev_tac `d = deg p` >> 859 qabbrev_tac `u = master (CARD R ** d)` >> 860 qabbrev_tac `v = master (CARD R ** n)` >> 861 `p pdivides u` by rw[poly_irreducible_divides_master, Abbr`u`, Abbr`d`] >> 862 `pmonic p` by rw[poly_monic_irreducible_property] >> 863 `poly u /\ poly v` by rw[Abbr`u`, Abbr`v`] >> 864 rw_tac std_ss[EQ_IMP_THM] >| [ 865 `p pdivides (pgcd u v)` by rw[poly_gcd_is_gcd] >> 866 qabbrev_tac `e = gcd d n` >> 867 qabbrev_tac `q = master (CARD R ** e)` >> 868 `pgcd u v ~~ q` by rw[poly_master_gcd_identity, Abbr`u`, Abbr`v`, Abbr`q`, Abbr`e`] >> 869 `p pdivides q` by metis_tac[poly_unit_eq_divisor, poly_gcd_poly, poly_master_poly] >> 870 `0 < e` by metis_tac[GCD_EQ_0, NOT_ZERO_LT_ZERO] >> 871 `d <= e` by rw[poly_irreducible_master_factor_deg, Abbr`d`] >> 872 `e divides d` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`e`] >> 873 `e <= d` by metis_tac[DIVIDES_LE] >> 874 `e = d` by decide_tac >> 875 rw[divides_iff_gcd_fix], 876 `1 < CARD R` by rw[finite_field_card_gt_1] >> 877 `u pdivides v` by rw[poly_master_divisibility, Abbr`u`, Abbr`v`] >> 878 metis_tac[poly_divides_transitive] 879 ]); 880 881(* This is a milestone theorem. *) 882 883(* Theorem: FiniteField r /\ s <<= r ==> !p. monic p /\ IPoly s p ==> 884 (p pdivides (master (CARD B ** (r <:> s))) <=> deg p divides (r <:> s)) *) 885(* Proof: 886 Note FiniteField s by subfield_finite_field 887 and s <= r by subfield_is_subring 888 Note Poly s p by poly_irreducible_poly, by IPoly s p 889 and Monic s p by subring_poly_monic_iff, Poly s p 890 Note deg p = Deg s p by subring_poly_deg 891 so 0 < deg p by poly_irreducible_deg_nonzero, by IPoly s p 892 or 0 < Deg s p by subring_poly_deg 893 Thus Pmonic s p by poly_monic_pmonic 894 Let q = master (CARD R). 895 Then Poly s q by poly_master_spoly 896 and q = Master s (CARD R) by subring_poly_master 897 Thus p pdivides q <=> poly_divides s p (Master s (CARD R)) by subring_poly_divides_iff 898 Now CARD R = CARD B ** (r <:> s) by finite_subfield_card_eqn 899 so p pdivides q <=> deg p divides (r <:> s) by poly_irreducible_master_divisibility 900 901poly_irreducible_master_divisibility |> ISPEC ``s:'a field``; 902|- FiniteField s ==> !p. Monic s p /\ IPoly s p ==> 903 !n. poly_divides s p (Master s (CARD B ** n)) <=> Deg s p divides n 904*) 905val poly_irreducible_master_subfield_divisibility = store_thm( 906 "poly_irreducible_master_subfield_divisibility", 907 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !p. monic p /\ IPoly s p ==> 908 (p pdivides (master (CARD R)) <=> deg p divides (r <:> s))``, 909 rpt (stripDup[FiniteField_def]) >> 910 `FiniteField s` by metis_tac[subfield_finite_field] >> 911 `s <= r` by rw[subfield_is_subring] >> 912 `Poly s p` by rw[poly_irreducible_poly] >> 913 `Monic s p` by metis_tac[subring_poly_monic_iff] >> 914 `deg p = Deg s p` by rw[subring_poly_deg] >> 915 `0 < deg p` by rw[poly_irreducible_deg_nonzero] >> 916 `Pmonic s p` by metis_tac[poly_monic_pmonic, subring_poly_deg] >> 917 qabbrev_tac `q = master (CARD R)` >> 918 `Poly s q` by rw[poly_master_spoly, Abbr`q`] >> 919 `CARD R = CARD B ** (r <:> s)` by rw[finite_subfield_card_eqn] >> 920 metis_tac[poly_irreducible_master_divisibility, subring_poly_divides_iff, subring_poly_master]); 921 922(* ------------------------------------------------------------------------- *) 923(* Master as Product of Factors *) 924(* ------------------------------------------------------------------------- *) 925 926(* Theorem: FiniteField r ==> (master (CARD R) = PPROD (IMAGE factor R)) *) 927(* Proof: 928 Since FiniteField r 929 ==> 1 < CARD R by finite_field_card_gt_1 930 and monic (master (CARD R)) by poly_master_monic, 1 < CARD R 931 and deg (master (CARD R)) = CARD R by poly_master_deg, 1 < CARD R 932 Now roots (master (CARD R)) = R by poly_master_roots_all 933 so CARD R = CARD (roots (master (CARD R))) by above 934 Hence master (CARD R) 935 = poly_factors (master (CARD R)) by poly_prod_factor_roots_eq_poly 936 = PPROD (IMAGE factor R) by notation 937*) 938val poly_master_eq_root_factor_product = store_thm( 939 "poly_master_eq_root_factor_product", 940 ``!r:'a field. FiniteField r ==> (master (CARD R) = PPROD (IMAGE factor R))``, 941 rpt (stripDup[FiniteField_def]) >> 942 `roots (master (CARD R)) = R` by rw[poly_master_roots_all] >> 943 `Ring r /\ #1 <> #0` by rw[] >> 944 `1 < CARD R` by rw[finite_field_card_gt_1] >> 945 `monic (master (CARD R))` by rw[poly_master_monic] >> 946 `deg (master (CARD R)) = CARD R` by rw[poly_master_deg] >> 947 metis_tac[poly_prod_factor_roots_eq_poly]); 948 949(* Theorem: FiniteField r ==> (master (CARD R) = PPROD {X - c * |1| | c | c IN R}) *) 950(* Proof: 951 Note 1 < CARD R by finite_field_card_gt_1 952 and roots (master (CARD R)) = R by poly_master_roots_all 953 Also monic (master (CARD R)) by poly_master_monic, 1 < CARD R 954 and deg (master (CARD R)) = CARD R by poly_master_deg 955 master (CARD R) 956 = PPROD {X - c * |1| | c | c IN R} by poly_eq_prod_factor_roots_alt 957*) 958val poly_master_eq_root_factor_product_alt = store_thm( 959 "poly_master_eq_root_factor_product_alt", 960 ``!r:'a field. FiniteField r ==> (master (CARD R) = PPROD {X - c * |1| | c | c IN R})``, 961 rpt (stripDup[FiniteField_def]) >> 962 `Ring r /\ #1 <> #0` by rw[] >> 963 `1 < CARD R` by rw[finite_field_card_gt_1] >> 964 `roots (master (CARD R)) = R` by rw[poly_master_roots_all] >> 965 `monic (master (CARD R))` by rw[] >> 966 `deg (master (CARD R)) = CARD R` by rw[] >> 967 metis_tac[poly_eq_prod_factor_roots_alt]); 968 969 970(* ------------------------------------------------------------------------- *) 971(* Subfield Conditions *) 972(* ------------------------------------------------------------------------- *) 973 974(* Theorem: FiniteField r ==> !s. s <<= r ==> 975 !x. x IN R ==> (x IN B <=> (x ** CARD B = x)) *) 976(* Proof: 977 Since FiniteField r, FiniteField s by subfield_finite_field 978 If part: x IN B ==> x ** CARD B = x 979 True by finite_field_fermat_thm, subfield_exp. 980 Only-if part: x IN R /\ x ** CARD B = x ==> x IN B 981 Let n = CARD B, p = master n. 982 Then !y. y IN B ==> poly_root s (master s n) y by poly_master_root_all 983 or !y. y IN B ==> root p y by poly_master_subfield_root 984 or !y. y IN B ==> y IN (roots p) by poly_roots_member, subfield_element 985 so B SUBSET (roots p) by SUBSET_DEF 986 But x IN R /\ x ** n = x by given 987 so root p x by poly_master_root 988 or x IN (roots p) by poly_roots_member 989 By contradiction, suppose x NOTIN B. 990 Then B <> roots p by x IN (roots p) 991 so B PSUBSET (roots p) by PSUBSET_DEF 992 Now poly p by poly_master_poly 993 and 1 < n by finite_field_card_gt_1 994 and p <> |0| by poly_master_eq_zero, n <> 1. 995 so FINITE (roots p) by poly_roots_finite, p <> |0| 996 Thus n < CARD (roots p) by CARD_PSUBSET 997 so deg p = n by poly_master_deg, 1 < n 998 Thus CARD (roots p) <= n by poly_roots_count, p <> |0| 999 This contradicts n < CARD (roots p). 1000*) 1001val subfield_element_condition = store_thm( 1002 "subfield_element_condition", 1003 ``!r:'a field. FiniteField r ==> !s. s <<= r ==> 1004 !x. x IN R ==> (x IN B <=> (x ** CARD B = x))``, 1005 rpt (stripDup[FiniteField_def]) >> 1006 `FiniteField s` by metis_tac[subfield_finite_field] >> 1007 rw[EQ_IMP_THM] >- 1008 metis_tac[finite_field_fermat_thm, subfield_exp] >> 1009 `Ring r /\ Ring s` by rw[] >> 1010 qabbrev_tac `n = CARD B` >> 1011 qabbrev_tac `p = master n` >> 1012 `!y. y IN B ==> root p y` by metis_tac[poly_master_root_all, poly_master_subfield_root] >> 1013 `B SUBSET (roots p)` by metis_tac[poly_roots_member, SUBSET_DEF, subfield_element] >> 1014 `x IN roots p` by rw[poly_master_root, poly_roots_member, Abbr`p`, Abbr`n`] >> 1015 spose_not_then strip_assume_tac >> 1016 `B <> roots p` by metis_tac[] >> 1017 `B PSUBSET (roots p)` by rw[PSUBSET_DEF] >> 1018 `poly p` by rw[Abbr`p`] >> 1019 `1 < n` by rw[finite_field_card_gt_1, Abbr`n`] >> 1020 `n <> 1` by decide_tac >> 1021 `p <> |0|` by metis_tac[poly_master_eq_zero, field_one_ne_zero] >> 1022 `deg p = n` by rw[poly_master_deg, Abbr`p`, Abbr`n`] >> 1023 `FINITE (roots p)` by rw[poly_roots_finite] >> 1024 `n < CARD (roots p)` by rw[CARD_PSUBSET, Abbr`n`] >> 1025 `CARD (roots p) <= n` by metis_tac[poly_roots_count] >> 1026 decide_tac); 1027 1028(* This is a milestone theorem. *) 1029 1030(* Theorem: FiniteField r ==> !s. s <<= r ==> 1031 !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B))) *) 1032(* Proof: 1033 Note FiniteField s by subfield_finite_field 1034 and char s = char r by subfield_char 1035 Let m = CARD B, c = char r. 1036 Then prime c by finite_field_char 1037 and ?d. 0 < d /\ (m = c ** d) by finite_field_card 1038 1039 Step 1: compute p ** m 1040 Let n = SUC (deg p). 1041 Claim: p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) 1042 Proof: Let f = \k. p ' k, then rfun f by poly_coeff_ring_fun 1043 p ** m 1044 = (poly_sum (GENLIST (\k. p ' k * X ** k) n)) ** m by poly_eq_poly_sum 1045 = (poly_sum (GENLIST (\k. f k * X ** k) n)) ** m by FUN_EQ_THM, poly_cmult_exp, poly_exp_mult_comm 1046 = poly_sum (GENLIST (\k. f k * X ** k) ** m) n) by poly_sum_freshman_all 1047 = poly_sum (GENLIST (\k. (f k) ** m * (X ** k) ** m) n) by EXP_BASE_MULT 1048 = poly_sum (GENLIST (\k. (f k) ** m * (X ** m) ** k) n) by MULT_COMM 1049 = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) by f = \k. p ' k 1050 1051 If part: Poly s p ==> p ** m = peval p (X ** m) 1052 Since Poly s p 1053 ==> !k. p ' k IN B by subfield_eq_subring, subring_poly_coeff, poly_coeff_element 1054 ==> !k. (p ' k) ** m = p ' k by finite_field_fermat_thm, subfield_exp [1] 1055 Thus peval p (X ** m) 1056 = poly_sum (GENLIST (\k. p ' k * (X ** m) ** k) (SUC (deg p))) by poly_peval_by_poly_sum 1057 = p ** m by Step 1 1058 1059 Only-if part: p ** m = peval p (X ** m) ==> Poly s p 1060 Let q = poly_sum (GENLIST (\k. (p ' k) ** m * X ** k) n) 1061 1062 Claim: p ** m = peval q (X ** m) 1063 Proof: Note rfun (\k. (p ' k) ** m) by ring_fun_def, poly_coeff_element 1064 Let g = (\k. (p ' k) ** m * X ** k), then poly_fun g by poly_fun_from_ring_fun 1065 peval q (X ** m) 1066 = poly_sum (MAP (\x. peval x (X ** m)) (GENLIST g n)) by poly_peval_poly_sum_gen, poly_fun g 1067 = poly_sum (GENLIST ((\x. peval x (X ** m)) o g) n) by MAP_GENLIST 1068 = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) by FUN_EQ_THM, poly_peval_cmult, poly_peval_X_exp 1069 Hence p ** m = peval q (X ** m) by Claim 1 1070 1071 Note p ** m = peval q (X ** m) by Claim 2 1072 Since deg (X ** m) = m by poly_deg_X_exp 1073 and 0 < m by finite_field_card_pos 1074 peval q (X ** m) = peval p (X ** m) 1075 ==> q = p by poly_peval_eq, 0 < deg (X ** m) 1076 Claim: !k. q ' k = (p ' k) ** m [1] 1077 Proof: If p = |0|, 1078 Then q = |0|, 1079 so (p ' k = #0) /\ (q ' k = #0) by poly_coeff_zero 1080 and (p ' k) ** m = #0 by field_zero_exp, m <> 0 1081 Hence true. 1082 If p <> |0|, 1083 If deg p < k, 1084 Then (p ' k = #0) /\ (q ' k = #0) by poly_coeff_nonzero 1085 and (p ' k) ** m = #0 by field_zero_exp, m <> 0 1086 Hence true. 1087 If ~(deg p < k), 1088 Let f = \k. p ' k ** m 1089 Then rfun f by ring_fun_def, poly_coeff_element, ring_exp_element 1090 and f (deg p) 1091 = p ' (deg p) ** m 1092 = (lead p) ** m by poly_coeff_lead, p <> |0| 1093 <> #0 by field_exp_eq_zero, poly_lead_nonzero 1094 q ' k 1095 = f k by poly_sum_gen_coeff 1096 = (p ' k) ** m 1097 1098 Hence !k. q ' k = (p ' k) ** m by claim 1099 Also !k. q ' k = p ' k by q = p, [2] 1100 Thus !k. (p ' k) ** m = p ' k by [1], [2] 1101 Now !k. p ' k IN R by poly_coeff_element 1102 thus !k. p ' k IN B by subfield_element_condition 1103 Hence cpoly r s p by common_poly_alt 1104 or Poly s p by subring_poly_alt 1105*) 1106val subfield_poly_condition = store_thm( 1107 "subfield_poly_condition", 1108 ``!r:'a field. FiniteField r ==> !s. s <<= r ==> 1109 !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B)))``, 1110 rpt (stripDup[FiniteField_def]) >> 1111 `FiniteField s` by metis_tac[subfield_finite_field] >> 1112 `Ring r /\ Ring s /\ #1 <> #0` by rw[] >> 1113 qabbrev_tac `m = CARD B` >> 1114 qabbrev_tac `c = char r` >> 1115 `poly X /\ poly (X ** m)` by rw[] >> 1116 `prime c` by rw[finite_field_char, Abbr`c`] >> 1117 `char s = c` by rw[subfield_char, Abbr`c`] >> 1118 `?d. 0 < d /\ (m = c ** d)` by metis_tac[finite_field_card] >> 1119 qabbrev_tac `n = SUC (deg p)` >> 1120 `p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n)` by 1121 (`(\k. (p ' k * X ** k) ** m) = (\k. (p ' k) ** m * (X ** m) ** k)` by rw[FUN_EQ_THM, poly_cmult_exp, poly_exp_mult_comm] >> 1122 qabbrev_tac `f = \k. p ' k` >> 1123 `rfun f` by rw[poly_coeff_ring_fun, Abbr`f`] >> 1124 `(\j. f j * X ** j) = (\k. p ' k * X ** k)` by rw[Abbr`f`] >> 1125 `p = poly_sum (GENLIST (\k. p ' k * X ** k) n)` by rw[poly_eq_poly_sum, Abbr`n`] >> 1126 `p ** m = poly_sum (GENLIST (\k. (p ' k * X ** k) ** m) n)` by metis_tac[poly_sum_freshman_all] >> 1127 rw[]) >> 1128 rewrite_tac[EQ_IMP_THM] >> 1129 rpt strip_tac >| [ 1130 `!k. p ' k IN B` by metis_tac[subfield_eq_subring, subring_poly_coeff, poly_coeff_element] >> 1131 `!k. (p ' k) ** m = p ' k` by metis_tac[finite_field_fermat_thm, subfield_exp] >> 1132 rw[poly_peval_by_poly_sum], 1133 qabbrev_tac `q = poly_sum (GENLIST (\k. (p ' k) ** m * X ** k) n)` >> 1134 `p ** m = peval q (X ** m)` by 1135 (qabbrev_tac `g = (\k. (p ' k) ** m * X ** k)` >> 1136 `poly_fun g` by rw[poly_fun_from_ring_fun, Abbr`g`] >> 1137 `(\x. peval x (X ** m)) o g = (\k. (p ' k) ** m * (X ** m) ** k)` by rw[FUN_EQ_THM, poly_peval_cmult, poly_peval_X_exp, Abbr`g`] >> 1138 `peval q (X ** m) = poly_sum (MAP (\x. peval x (X ** m)) (GENLIST g n))` by rw[poly_peval_poly_sum_gen, Abbr`q`, Abbr`g`] >> 1139 `_ = poly_sum (GENLIST ((\x. peval x (X ** m)) o g) n)` by rw[MAP_GENLIST] >> 1140 `_ = poly_sum (GENLIST (\k. p ' k ** m * (X ** m) ** k) n)` by rw[] >> 1141 metis_tac[]) >> 1142 `deg (X ** m) = m` by rw[] >> 1143 `0 < m` by rw[finite_field_card_pos, Abbr`m`] >> 1144 `m <> 0` by decide_tac >> 1145 `poly q` by rw[poly_sum_poly, poly_list_gen_from_ring_fun, Abbr`q`] >> 1146 `q = p` by metis_tac[poly_peval_eq] >> 1147 `!k. q ' k = (p ' k) ** m` by 1148 (rpt strip_tac >> 1149 Cases_on `p = |0|` >- 1150 rw[field_zero_exp] >> 1151 Cases_on `deg p < k` >- 1152 rw[poly_coeff_nonzero, field_zero_exp] >> 1153 qabbrev_tac `f = \k. p ' k ** m` >> 1154 `rfun f` by metis_tac[ring_fun_def, poly_coeff_element, ring_exp_element] >> 1155 `f (deg p) = p ' (deg p) ** m` by rw[Abbr`f`] >> 1156 `_ = (lead p) ** m` by metis_tac[poly_coeff_lead] >> 1157 `lead p IN R` by rw[] >> 1158 `f (deg p) <> #0` by metis_tac[field_exp_eq_zero, poly_lead_nonzero] >> 1159 `GENLIST (\k. p ' k ** m * X ** k) n = GENLIST (\k. f k * X ** k) (SUC (deg p))` by rw[] >> 1160 `q = poly_sum (GENLIST (\k. f k * X ** k) (SUC (deg p)))` by metis_tac[] >> 1161 `q ' k = f k` by rw[poly_sum_gen_coeff] >> 1162 rw[] 1163 ) >> 1164 `!k. q ' k = p ' k` by rw[] >> 1165 `!k. p ' k IN B` by metis_tac[poly_coeff_element, subfield_element_condition] >> 1166 metis_tac[subfield_is_subring, subring_poly_alt, common_poly_alt] 1167 ]); 1168 1169(* This is a major milestone theorem. *) 1170(* Proof is still clunky: 1171 Need to have: p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) 1172 This half-result is used for if-part. 1173 Then complete by: peval q (X ** m) = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) 1174 To establish: p ** m = peval q (X ** m) for only-if part. 1175 1176 Did try to show: p ** m = peval q (X ** m) in one go, 1177 but applying this full result to if-part has problems. 1178 1179 Actually, the proof is good, because the if-part depends only on p, 1180 and it has nothing to do with q. The following is essentially a smooth-out 1181 version of the same proof -- not much difference! 1182*) 1183 1184(* Theorem: FiniteField r ==> !s. s <<= r ==> 1185 !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B))) *) 1186(* Proof: 1187 Note FiniteField s by subfield_finite_field 1188 and char s = char r by subfield_char 1189 Let m = CARD B, c = char r. 1190 Then prime c by finite_field_char 1191 and ?d. 0 < d /\ (m = c ** d) by finite_field_card 1192 1193 Step 1: compute p ** m 1194 Let n = SUC (deg p). 1195 Claim 1: p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) 1196 Proof: Let f = \k. p ' k, then rfun f by poly_coeff_ring_fun 1197 p ** m 1198 = (poly_sum (GENLIST (\k. p ' k * X ** k) n)) ** m by poly_eq_poly_sum 1199 = (poly_sum (GENLIST (\k. f k * X ** k) n)) ** m by FUN_EQ_THM, poly_cmult_exp, poly_exp_mult_comm 1200 = poly_sum (GENLIST (\k. f k * X ** k) ** m) n) by poly_sum_freshman_all 1201 = poly_sum (GENLIST (\k. (f k) ** m * (X ** k) ** m) n) by EXP_BASE_MULT 1202 = poly_sum (GENLIST (\k. (f k) ** m * (X ** m) ** k) n) by MULT_COMM 1203 = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) by f = \k. p ' k 1204 1205 If part: Poly s p ==> p ** m = peval p (X ** m) 1206 Since Poly s p 1207 ==> !k. p ' k IN B by subfield_eq_subring, subring_poly_coeff, poly_coeff_element 1208 ==> !k. (p ' k) ** m = p ' k by finite_field_fermat_thm, subfield_exp [1] 1209 Thus peval p (X ** m) 1210 = poly_sum (GENLIST (\k. p ' k * (X ** m) ** k) (SUC (deg p))) by poly_peval_by_poly_sum 1211 = p ** m by Step 1 1212 1213 Only-if part: p ** m = peval p (X ** m) ==> Poly s p 1214 Let q = poly_sum (GENLIST (\k. (p ' k) ** m * X ** k) n) 1215 Step 2: compute peval q (X ** m) 1216 Claim 2: peval q (X ** m) = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) 1217 Proof: Note rfun (\k. (p ' k) ** m) by ring_fun_def, poly_coeff_element 1218 Let g = (\k. (p ' k) ** m * X ** k), then poly_fun g by poly_fun_from_ring_fun 1219 peval q (X ** m) 1220 = poly_sum (MAP (\x. peval x (X ** m)) (GENLIST g n)) by poly_peval_poly_sum_gen, poly_fun g 1221 = poly_sum (GENLIST ((\x. peval x (X ** m)) o g) n) by MAP_GENLIST 1222 = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) by FUN_EQ_THM, poly_peval_cmult, poly_peval_X_exp 1223 1224 Hence p ** m = peval q (X ** m) by Claim 1, Claim 2, [*] 1225 Since deg (X ** m) = m by poly_deg_X_exp 1226 and 0 < m by finite_field_card_pos 1227 With p ** m = peval p (X ** m) by given 1228 ==> peval q (X ** m) = peval p (X ** m) by [*] 1229 ==> q = p by poly_peval_eq, 0 < deg (X ** m) 1230 1231 Claim 3: !k. q ' k = (p ' k) ** m 1232 Proof: If p = |0|, 1233 Then q = |0|, 1234 so (p ' k = #0) /\ (q ' k = #0) by poly_coeff_zero 1235 and (p ' k) ** m = #0 by field_zero_exp, m <> 0 1236 Hence true. 1237 If p <> |0|, 1238 If deg p < k, 1239 Then (p ' k = #0) /\ (q ' k = #0) by poly_coeff_nonzero 1240 and (p ' k) ** m = #0 by field_zero_exp, m <> 0 1241 Hence true. 1242 If ~(deg p < k), 1243 Let f = \k. p ' k ** m 1244 Then rfun f by ring_fun_def, poly_coeff_element, ring_exp_element 1245 and f (deg p) 1246 = p ' (deg p) ** m 1247 = (lead p) ** m by poly_coeff_lead, p <> |0| 1248 <> #0 by field_exp_eq_zero, poly_lead_nonzero 1249 q ' k 1250 = f k by poly_sum_gen_coeff 1251 = (p ' k) ** m 1252 1253 Hence !k. q ' k = (p ' k) ** m by Claim 3, [1] 1254 Also !k. q ' k = p ' k by q = p, [2] 1255 Thus !k. (p ' k) ** m = p ' k by [1], [2] 1256 Now !k. p ' k IN R by poly_coeff_element 1257 thus !k. p ' k IN B by subfield_element_condition 1258 Hence cpoly r s p by common_poly_alt 1259 or Poly s p by subring_poly_alt 1260*) 1261val subfield_poly_condition = store_thm( 1262 "subfield_poly_condition", 1263 ``!r:'a field. FiniteField r ==> !s. s <<= r ==> 1264 !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B)))``, 1265 rpt (stripDup[FiniteField_def]) >> 1266 `FiniteField s` by metis_tac[subfield_finite_field] >> 1267 `Ring r /\ Ring s /\ #1 <> #0` by rw[] >> 1268 qabbrev_tac `m = CARD B` >> 1269 qabbrev_tac `c = char r` >> 1270 `poly X /\ poly (X ** m)` by rw[] >> 1271 `prime c` by rw[finite_field_char, Abbr`c`] >> 1272 `char s = c` by rw[subfield_char, Abbr`c`] >> 1273 `?d. 0 < d /\ (m = c ** d)` by metis_tac[finite_field_card] >> 1274 `0 < m` by rw[finite_field_card_pos, Abbr`m`] >> 1275 `m <> 0` by decide_tac >> 1276 qabbrev_tac `n = SUC (deg p)` >> 1277 `p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n)` by 1278 (`rfun \k. p ' k` by rw[poly_coeff_ring_fun] >> 1279 `p ** m = poly_sum (GENLIST (\k. p ' k * X ** k) n) ** m` by rw[GSYM poly_eq_poly_sum, Abbr`n`] >> 1280 `_ = poly_sum (GENLIST (\k. (p ' k * X ** k) ** m) n)` by rw[poly_sum_freshman_all, Abbr`c`] >> 1281 `_ = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n)` by rw[FUN_EQ_THM, poly_cmult_exp, poly_exp_mult_comm] >> 1282 rw[]) >> 1283 rewrite_tac[EQ_IMP_THM] >> 1284 rpt strip_tac >| [ 1285 `!k. p ' k IN B` by metis_tac[subfield_eq_subring, subring_poly_coeff, poly_coeff_element] >> 1286 `!k. (p ' k) ** m = p ' k` by metis_tac[finite_field_fermat_thm, subfield_exp] >> 1287 rw[poly_peval_by_poly_sum], 1288 qabbrev_tac `q = poly_sum (GENLIST (\k. (p ' k) ** m * X ** k) n)` >> 1289 `deg (X ** m) = m` by rw[] >> 1290 `poly q` by rw[poly_sum_poly, poly_list_gen_from_ring_fun, Abbr`q`] >> 1291 `peval p (X ** m) = peval q (X ** m)` by 1292 (qabbrev_tac `f = (\k. (p ' k) ** m * X ** k)` >> 1293 `poly_fun f` by rw[poly_fun_from_ring_fun, Abbr`f`] >> 1294 `(\x. peval x (X ** m)) o f = (\k. (p ' k) ** m * (X ** m) ** k)` by rw[FUN_EQ_THM, poly_peval_cmult, poly_peval_X_exp, Abbr`f`] >> 1295 `peval q (X ** m) = poly_sum (GENLIST ((\x. peval x (X ** m)) o f) n)` by rw[poly_peval_poly_sum_gen, MAP_GENLIST, Abbr`q`] >> 1296 qabbrev_tac `g = (\k. p ' k ** m * (X ** m) ** k)` >> 1297 metis_tac[]) >> 1298 `q = p` by metis_tac[poly_peval_eq] >> 1299 `!k. q ' k = (p ' k) ** m` by 1300 (rpt strip_tac >> 1301 Cases_on `p = |0|` >- 1302 rw[field_zero_exp] >> 1303 Cases_on `deg p < k` >- 1304 rw[poly_coeff_nonzero, field_zero_exp] >> 1305 qabbrev_tac `f = \k. p ' k ** m` >> 1306 `rfun f` by metis_tac[ring_fun_def, poly_coeff_element, ring_exp_element] >> 1307 `f (deg p) = p ' (deg p) ** m` by rw[Abbr`f`] >> 1308 `_ = (lead p) ** m` by metis_tac[poly_coeff_lead] >> 1309 `lead p IN R` by rw[] >> 1310 `f (deg p) <> #0` by metis_tac[field_exp_eq_zero, poly_lead_nonzero] >> 1311 `GENLIST (\k. p ' k ** m * X ** k) n = GENLIST (\k. f k * X ** k) (SUC (deg p))` by rw[] >> 1312 `q = poly_sum (GENLIST (\k. f k * X ** k) (SUC (deg p)))` by metis_tac[] >> 1313 `q ' k = f k` by rw[poly_sum_gen_coeff] >> 1314 rw[] 1315 ) >> 1316 `!k. p ' k IN B` by metis_tac[poly_coeff_element, subfield_element_condition] >> 1317 metis_tac[subfield_is_subring, subring_poly_alt, common_poly_alt] 1318 ]); 1319 1320(* Another milestone theorem! *) 1321 1322(* ------------------------------------------------------------------------- *) 1323(* Sets of Monic Irreducible Polynomials *) 1324(* ------------------------------------------------------------------------- *) 1325 1326(* Define the set of monic irreducibles in a field, with degree equal to n *) 1327val monic_irreducibles_degree_def = Define` 1328 monic_irreducibles_degree (r:'a field) (n:num) = {p | monic p /\ ipoly p /\ (deg p = n)} 1329`; 1330 1331(* Define the set of monic irreducibles in a field, with degree dividing n *) 1332val monic_irreducibles_bounded_def = Define` 1333 monic_irreducibles_bounded (r:'a field) (n:num) = 1334 BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n)) 1335`; 1336 1337(* Theorem: p IN (monic_irreducibles_degree r n) <=> monic p /\ ipoly p /\ (deg p = n) *) 1338(* Proof: by monic_irreducibles_degree_def *) 1339val monic_irreducibles_degree_member = store_thm( 1340 "monic_irreducibles_degree_member", 1341 ``!(r:'a field) n p. p IN (monic_irreducibles_degree r n) <=> monic p /\ ipoly p /\ (deg p = n)``, 1342 rw[monic_irreducibles_degree_def]); 1343 1344(* Theorem: p IN (monic_irreducibles_bounded r n) <=> 1345 monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n *) 1346(* Proof: 1347 p IN (monic_irreducibles_bounded r n) 1348 <=> p IN BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n)) by monic_irreducibles_bounded_def 1349 <=> ?s. p IN s /\ s IN (IMAGE (monic_irreducibles_degree r) (divisors n)) by IN_BIGUNION 1350 Take s = monic_irreducibles_degree r (deg p), 1351 Then p IN s 1352 <=> monic p /\ ipoly p /\ (deg p = deg p) by monic_irreducibles_degree_member 1353 and s IN (IMAGE (monic_irreducibles_degree r) (divisors n)) 1354 <=> (deg p) IN (divisors n) 1355 <=> (deg p <= n) /\ (deg p) divides n by divisors_element 1356*) 1357val monic_irreducibles_bounded_member = store_thm( 1358 "monic_irreducibles_bounded_member", 1359 ``!(r:'a field) n p. p IN (monic_irreducibles_bounded r n) <=> 1360 monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n``, 1361 (rw[monic_irreducibles_bounded_def, monic_irreducibles_degree_member, divisors_element, EXTENSION, EQ_IMP_THM] >> simp[]) >> 1362 qexists_tac `monic_irreducibles_degree r (deg p)` >> 1363 simp[monic_irreducibles_degree_member] >> 1364 qexists_tac `deg p` >> 1365 simp[]); 1366 1367(* Theorem: FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_degree r n) *) 1368(* Proof: 1369 Let s = monic_irreducibles_degree r n, m = SUC n. 1370 Then n < m by LESS_SUC 1371 and !p. p IN s ==> poly p /\ deg p < m by monic_irreducibles_degree_member, poly_monic_poly 1372 Thus s SUBSET {p | poly p /\ deg p < m} by SUBSET_DEF 1373 Now FINITE {p | poly p /\ deg p < m} by poly_truncated_by_degree_finite 1374 Hence FINITE s by SUBSET_FINITE 1375*) 1376val monic_irreducibles_degree_finite = store_thm( 1377 "monic_irreducibles_degree_finite", 1378 ``!r:'a ring. FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_degree r n)``, 1379 rpt strip_tac >> 1380 `n < SUC n` by decide_tac >> 1381 qabbrev_tac `s = monic_irreducibles_degree r n` >> 1382 qabbrev_tac `m = SUC n` >> 1383 `!p. p IN s ==> poly p /\ deg p < m` by metis_tac[monic_irreducibles_degree_member, poly_monic_poly] >> 1384 `s SUBSET {p | poly p /\ deg p < m}` by rw[SUBSET_DEF] >> 1385 `FINITE {p | poly p /\ deg p < m}` by rw[poly_truncated_by_degree_finite] >> 1386 metis_tac[SUBSET_FINITE]); 1387 1388(* Theorem: FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_bounded r n) *) 1389(* Proof: 1390 By monic_irreducibles_bounded_def, this is to show: 1391 FINITE (BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n))) 1392 By FINITE_BIGUNION, this is to show: 1393 (1) FINITE (IMAGE (monic_irreducibles_degree r) (divisors n)) 1394 Since FINITE (divisors n) by divisors_finite 1395 Hence true by IMAGE_FINITE 1396 (2) EVERY_FINITE (IMAGE (monic_irreducibles_degree r) (divisors n)) 1397 That is, !x. x IN (divisors n), FINITE (monic_irreducibles_degree r x) by IN_IMAGE 1398 This is true by monic_irreducibles_degree_finite 1399*) 1400val monic_irreducibles_bounded_finite = store_thm( 1401 "monic_irreducibles_bounded_finite", 1402 ``!r:'a ring. FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_bounded r n)``, 1403 rw[monic_irreducibles_bounded_def] >- 1404 rw[divisors_finite] >> 1405 rw[monic_irreducibles_degree_finite]); 1406 1407(* Theorem: Field r ==> (monic_irreducibles_degree r 0 = {}) *) 1408(* Proof: 1409 By contradiction, suppose monic_irreducibles_degree r 0 <> {}. 1410 Then ?p. p IN (monic_irreducibles_degree r 0) by MEMBER_NOT_EMPTY 1411 or ?p. monic p /\ ipoly p /\ (deg p = 0) by monic_irreducibles_degree_member 1412 But monic p /\ ipoly p ==> 0 < deg p by poly_irreducible_deg_nonzero 1413 This contradicts deg p = 0. 1414*) 1415val monic_irreducibles_degree_0 = store_thm( 1416 "monic_irreducibles_degree_0", 1417 ``!r:'a field. Field r ==> (monic_irreducibles_degree r 0 = {})``, 1418 rw[monic_irreducibles_degree_member, EXTENSION] >> 1419 spose_not_then strip_assume_tac >> 1420 `0 < deg x` by rw[poly_irreducible_deg_nonzero] >> 1421 decide_tac); 1422 1423(* Theorem: Field r ==> (monic_irreducibles_degree r 1 = IMAGE factor R) *) 1424(* Proof: 1425 By monic_irreducibles_degree_member, this is to show; 1426 (1) monic x /\ (deg x = 1) ==> ?x'. (x = factor x') /\ x' IN R 1427 True by poly_monic_deg1_factor 1428 (2) x' IN R ==> monic (factor x') 1429 True by poly_factor_monic 1430 (3) x' IN R ==> ipoly (factor x') 1431 Since poly (factor x') by poly_factor_poly 1432 and deg (factor x') = 1 by poly_deg_factor 1433 Hence true by poly_deg_1_irreducible 1434 (4) x' IN R ==> deg (factor x') = 1 1435 True by poly_deg_factor 1436*) 1437val monic_irreducibles_degree_1 = store_thm( 1438 "monic_irreducibles_degree_1", 1439 ``!r:'a field. Field r ==> (monic_irreducibles_degree r 1 = IMAGE factor R)``, 1440 rpt strip_tac >> 1441 `Ring r /\ #1 <> #0` by rw[] >> 1442 rw[monic_irreducibles_degree_member, EXTENSION, EQ_IMP_THM] >- 1443 metis_tac[poly_monic_deg1_factor] >- 1444 rw[poly_factor_monic] >- 1445 metis_tac[poly_factor_poly, poly_deg_factor, poly_deg_1_irreducible] >> 1446 rw[poly_deg_factor]); 1447 1448(* Theorem: Field r ==> (monic_irreducibles_bounded r 0 = {}) *) 1449(* Proof: 1450 Since x IN (monic_irreducibles_bounded r 0) 1451 <=> monic x /\ ipoly x /\ deg x <= 0 /\ deg x divides 0 by monic_irreducibles_bounded_member 1452 <=> monic x /\ ipoly x /\ (deg x = 0) by ALL_DIVIDES_0 1453 <=> x IN (monic_irreducibles_degree r 0) by monic_irreducibles_degree_member 1454 Hence (monic_irreducibles_bounded r 0) 1455 = (monic_irreducibles_degree r 0) by EXTENSION 1456 = {} by monic_irreducibles_degree_0 1457*) 1458val monic_irreducibles_bounded_0 = store_thm( 1459 "monic_irreducibles_bounded_0", 1460 ``!r:'a field. Field r ==> (monic_irreducibles_bounded r 0 = {})``, 1461 rpt strip_tac >> 1462 `(monic_irreducibles_bounded r 0) = (monic_irreducibles_degree r 0)` 1463 by rw[monic_irreducibles_bounded_member, monic_irreducibles_degree_member, 1464 EXTENSION, EQ_IMP_THM] >> 1465 rw[monic_irreducibles_degree_0]); 1466 1467(* Theorem: Field r ==> (monic_irreducibles_bounded r 1 = IMAGE factor R) *) 1468(* Proof: 1469 Since x IN (monic_irreducibles_bounded r 1) 1470 <=> monic x /\ ipoly x /\ deg x <= 1 /\ deg x divides 1 by monic_irreducibles_bounded_member 1471 <=> monic x /\ ipoly x /\ (deg x = 1) by DIVIDES_ONE 1472 <=> x IN (monic_irreducibles_degree r 1) by monic_irreducibles_degree_member 1473 Hence (monic_irreducibles_bounded r 1) 1474 = (monic_irreducibles_degree r 1) by EXTENSION 1475 = IMAGE factor R by monic_irreducibles_degree_1 1476*) 1477val monic_irreducibles_bounded_1 = store_thm( 1478 "monic_irreducibles_bounded_1", 1479 ``!r:'a field. Field r ==> (monic_irreducibles_bounded r 1 = IMAGE factor R)``, 1480 rpt strip_tac >> 1481 `(monic_irreducibles_bounded r 1) = (monic_irreducibles_degree r 1)` 1482 by rw[monic_irreducibles_bounded_member, monic_irreducibles_degree_member, 1483 DIVIDES_ONE, EXTENSION, EQ_IMP_THM] >> 1484 rw[monic_irreducibles_degree_1]); 1485 1486(* Theorem: miset (monic_irreducibles_degree r n) *) 1487(* Proof: by monic_irreducibles_degree_member *) 1488val monic_irreducibles_degree_monic_irreducibles_set = store_thm( 1489 "monic_irreducibles_degree_monic_irreducibles_set", 1490 ``!r:'a ring. !n. miset (monic_irreducibles_degree r n)``, 1491 rw_tac std_ss[monic_irreducibles_degree_member]); 1492 1493(* Theorem: mset (monic_irreducibles_degree r n) *) 1494(* Proof: by monic_irreducibles_degree_member *) 1495val monic_irreducibles_degree_monic_set = store_thm( 1496 "monic_irreducibles_degree_monic_set", 1497 ``!r:'a ring. !n. mset (monic_irreducibles_degree r n)``, 1498 rw_tac std_ss[monic_irreducibles_degree_member]); 1499 1500(* Theorem: pset (monic_irreducibles_degree r n) *) 1501(* Proof: by monic_irreducibles_degree_monic_set, monic_set_poly_set *) 1502val monic_irreducibles_degree_poly_set = store_thm( 1503 "monic_irreducibles_degree_poly_set", 1504 ``!r:'a ring. !n. pset (monic_irreducibles_degree r n)``, 1505 metis_tac[monic_irreducibles_degree_monic_set, monic_set_poly_set]); 1506 1507(* Original proof of the same theorem *) 1508 1509(* Theorem: pset (monic_irreducibles_degree r n) *) 1510(* Proof: 1511 Let s = monic_irreducibles_degree r n. 1512 !p. p IN s 1513 ==> monic p by monic_irreducibles_degree_member 1514 ==> poly p by poly_monic_poly 1515 Hence pset s by notation 1516*) 1517val monic_irreducibles_degree_poly_set = store_thm( 1518 "monic_irreducibles_degree_poly_set", 1519 ``!r:'a ring. !n. pset (monic_irreducibles_degree r n)``, 1520 rw[monic_irreducibles_degree_member]); 1521 1522(* Theorem: Field r ==> !n. pcoprime_set (monic_irreducibles_degree r n) *) 1523(* Proof: 1524 By poly_coprime_set_def, this is to show: 1525 (1) p IN monic_irreducibles_degree r n ==> poly p 1526 Note p IN monic_irreducibles_degree r n 1527 ==> monic p by monic_irreducibles_degree_member 1528 ==> poly p by poly_monic_poly 1529 (2) p IN monic_irreducibles_degree r n /\ q IN monic_irreducibles_degree r n /\ p <> q ==> pcoprime p q 1530 Note p, q IN monic_irreducibles_degree r n 1531 ==> monic p /\ ipoly p /\ monic q /\ ipoly q by monic_irreducibles_degree_member 1532 With p <> q ==> pcoprime p q by poly_monic_irreducibles_coprime 1533*) 1534val monic_irreducibles_degree_coprime_set = store_thm( 1535 "monic_irreducibles_degree_coprime_set", 1536 ``!r:'a field. Field r ==> !n. pcoprime_set (monic_irreducibles_degree r n)``, 1537 rw_tac std_ss[poly_coprime_set_def] >- 1538 metis_tac[monic_irreducibles_degree_member, poly_monic_poly] >> 1539 metis_tac[monic_irreducibles_degree_member, poly_monic_irreducibles_coprime]); 1540 1541(* Theorem: Field r ==> !n. pcoprime_set (monic_irreducibles_bounded r n) *) 1542(* Proof: 1543 By poly_coprime_set_def, this is to show: 1544 (1) p IN monic_irreducibles_bounded r n ==> poly p 1545 Note p IN monic_irreducibles_bounded r n 1546 ==> monic p by monic_irreducibles_bounded_member 1547 ==> poly p by poly_monic_poly 1548 (2) p IN monic_irreducibles_bounded r n /\ q IN monic_irreducibles_bounded r n /\ p <> q ==> pcoprime p q 1549 Note p, q IN monic_irreducibles_bounded r n 1550 ==> monic p /\ ipoly p /\ monic q /\ ipoly q by monic_irreducibles_bounded_member 1551 With p <> q ==> pcoprime p q by poly_monic_irreducibles_coprime 1552*) 1553val monic_irreducibles_bounded_coprime_set = store_thm( 1554 "monic_irreducibles_bounded_coprime_set", 1555 ``!r:'a field. Field r ==> !n. pcoprime_set (monic_irreducibles_bounded r n)``, 1556 rw_tac std_ss[poly_coprime_set_def] >- 1557 metis_tac[monic_irreducibles_bounded_member, poly_monic_poly] >> 1558 metis_tac[monic_irreducibles_bounded_member, poly_monic_irreducibles_coprime]); 1559 1560(* ------------------------------------------------------------------------- *) 1561(* Product of Monic Irreducibles of the same degree *) 1562(* ------------------------------------------------------------------------- *) 1563 1564(* Overload on the product of monic irreducibles of same degree *) 1565val _ = overload_on("poly_psi", ``\(r:'a ring) n. PPROD (monic_irreducibles_degree r n)``); 1566val _ = overload_on("Psi", ``poly_psi r``); 1567 1568(* Theorem: FiniteRing r ==> !n. monic (Psi n) *) 1569(* Proof: 1570 Let s = monic_irreducibles_degree r n. 1571 Then FINITE s by monic_irreducibles_degree_finite, FINITE R 1572 and mset s by monic_irreducibles_degree_member 1573 ==> monic (PPROD s) by poly_monic_prod_set_monic 1574 or monic (Psi n) by notation 1575*) 1576val monic_irreducibles_degree_prod_set_monic = store_thm( 1577 "monic_irreducibles_degree_prod_set_monic", 1578 ``!r:'a ring. FiniteRing r ==> !n. monic (Psi n)``, 1579 rw[FiniteRing_def] >> 1580 qabbrev_tac `s = monic_irreducibles_degree r n` >> 1581 `FINITE s` by rw[monic_irreducibles_degree_finite, Abbr`s`] >> 1582 `mset s` by metis_tac[monic_irreducibles_degree_member] >> 1583 rw[poly_monic_prod_set_monic]); 1584 1585(* Theorem: FiniteRing r ==> !n. poly (Psi n) *) 1586(* Proof: by monic_irreducibles_degree_prod_set_monic, poly_monic_poly *) 1587val monic_irreducibles_degree_prod_set_poly = store_thm( 1588 "monic_irreducibles_degree_prod_set_poly", 1589 ``!r:'a ring. FiniteRing r ==> !n. poly (Psi n)``, 1590 rw_tac std_ss[monic_irreducibles_degree_prod_set_monic, poly_monic_poly]); 1591 1592(* Theorem: FiniteRing r /\ #1 <> #0 ==> !n. Psi n <> |0| *) 1593(* Proof: by monic_irreducibles_degree_prod_set_monic, poly_monic_nonzero *) 1594val monic_irreducibles_degree_prod_set_nonzero = store_thm( 1595 "monic_irreducibles_degree_prod_set_nonzero", 1596 ``!r:'a ring. FiniteRing r /\ #1 <> #0 ==> !n. Psi n <> |0|``, 1597 rw_tac std_ss[monic_irreducibles_degree_prod_set_monic, poly_monic_nonzero]); 1598 1599(* ------------------------------------------------------------------------- *) 1600(* Master Polynomial as Product of Monic Irreducibles. *) 1601(* ------------------------------------------------------------------------- *) 1602 1603(* Note: 1604The following result is easy (?) if we know the degrees are equal. 1605However, we want to use the result to show that the degrees are equal, 1606so the proof cannot rely on this. 1607Instead, the strategy goes like this: 1608- (PPROD s) divides master, so master = (q) * (PPROD s) 1609- By poly_ulead_divides_master_condition, only members of s can divide master. 1610- By pgcd master D(master) ~~ |1|, only s divides master, no s ** k with 1 < k divides master. 1611- Hence upoly q, which means q = |1| since (monic master) and (monic (PPROD s)). 1612*) 1613 1614(* Theorem: FiniteField r ==> !s. s <<= r ==> 1615 !n. 0 < n ==> (Master s (CARD B ** n) = poly_prod_set s (monic_irreducibles_bounded s n)) *) 1616(* Proof: 1617 Note FiniteField s by subfield_finite_field 1618 and FINITE B by FiniteField_def 1619 Let b = monic_irreducibles_bounded s n, 1620 p = poly_prod_set s b, 1621 m = Master s (CARD B ** n). 1622 The goal: m = p 1623 The idea: (1) show: p pdivides m, then m = u * p for some u. 1624 (2) show: upoly u, then m ~~ p. 1625 (3) show: monic p /\ monic m, then m = p. 1626 Of course, all these happen in s, the subfield of r. 1627 1628 Step 0, show basic results 1629 Note FINITE b by monic_irreducibles_bounded_finite, 0 < n, FINITE B 1630 Note 1 < CARD B by finite_field_card_gt_1 1631 thus 1 < CARD B ** n by ONE_LT_EXP, 0 < n 1632 Hence poly_monic s m by poly_master_monic, , 1 < CARD B ** n 1633 and !p. p IN b ==> monic p by monic_irreducibles_bounded_member 1634 Hence poly_monic s p by poly_monic_prod_set_monic 1635 1636 Step 1, show: poly_divides s p m 1637 By poly_prod_coprime_set_divides, this is to show: 1638 (1) !p. p IN b ==> poly_divides s p m 1639 Note p IN b 1640 ==> poly_monic s p /\ IPoly s p /\ 1641 (poly_deg s p) divides n by monic_irreducibles_bounded_member 1642 Hence poly_divides s p m by poly_irreducible_master_divisibility 1643 (2) poly_coprime_set s b by monic_irreducibles_bounded_coprime_set 1644 1645 Step 2, show: unit_eq (PolyRing s) m p 1646 By poly_coprime_diff_unit_eq_prod_set, this is to show: 1647 (1) !p. poly_monic s p /\ IPoly s p /\ poly_divides s p m ==> p IN b 1648 Since poly_divides s p m 1649 ==> poly_deg s p divides n by poly_irreducible_master_divisibility 1650 thus poly_deg s p <= n by DIVIDES_LE, 0 < n 1651 With poly_monic s p /\ IPoly s p by given 1652 Hence p IN b by monic_irreducibles_bounded_member 1653 (2) !p. p IN b ==> Poly s p by monic_irreducibles_bounded_member, poly_monic_poly 1654 (3) poly_gcd s m (poly_diff s m) IN (Invertibles (PolyRing s).prod).carrier 1655 Effectively this says: pcoprime m (diff m) in subfield s. 1656 Since poly_gcd s m (poly_diff s m) ~~ |1| by poly_master_coprime_diff 1657 Hence the result follows by poly_gcd_one_coprime 1658 1659 Step 3, conclude: m = p 1660 With poly_monic s m by above 1661 and poly_monic s p by above 1662 Hence unit_eq (PolyRing s) m p ==> (m = p) by poly_unit_eq_monic_eq 1663*) 1664val poly_master_subfield_factors = store_thm( 1665 "poly_master_subfield_factors", 1666 ``!r:'a field. FiniteField r ==> !s. s <<= r ==> 1667 !n. 0 < n ==> (Master s (CARD B ** n) = poly_prod_set s (monic_irreducibles_bounded s n))``, 1668 rpt (stripDup[FiniteField_def]) >> 1669 `FiniteField s` by metis_tac[subfield_finite_field] >> 1670 `FINITE B` by metis_tac[FiniteField_def] >> 1671 qabbrev_tac `b = monic_irreducibles_bounded s n` >> 1672 qabbrev_tac `p = poly_prod_set s b` >> 1673 qabbrev_tac `m = Master s (CARD B ** n)` >> 1674 `FINITE b` by rw[monic_irreducibles_bounded_finite, Abbr`b`] >> 1675 `1 < CARD B` by rw[finite_field_card_gt_1] >> 1676 `1 < CARD B ** n` by rw[ONE_LT_EXP] >> 1677 `poly_monic s m` by rw[poly_master_monic, Abbr`m`] >> 1678 `poly_monic s p` by rw[poly_monic_prod_set_monic, monic_irreducibles_bounded_member, Abbr`b`, Abbr`p`] >> 1679 `poly_divides s p m` by 1680 ((qunabbrev_tac `p` >> irule poly_prod_coprime_set_divides >> rpt conj_tac >> simp[]) >- 1681 metis_tac[monic_irreducibles_bounded_member, poly_irreducible_master_divisibility] >> 1682 rw[monic_irreducibles_bounded_coprime_set, Abbr`b`] 1683 ) >> 1684 `unit_eq (PolyRing s) m p` by 1685 ((qunabbrev_tac `p` >> irule poly_coprime_diff_unit_eq_prod_set >> rpt conj_tac >> simp[]) >- 1686 metis_tac[monic_irreducibles_bounded_member, poly_irreducible_master_divisibility, DIVIDES_LE] >- 1687 rw[Abbr`b`, monic_irreducibles_bounded_member] >> 1688 rw[poly_master_coprime_diff, poly_gcd_one_coprime, Abbr`m`] 1689 ) >> 1690 metis_tac[poly_unit_eq_monic_eq, field_is_ring]); 1691 1692(* Theorem: FiniteField r /\ s <<= r /\ 0 < n ==> 1693 (master (CARD B ** n) = poly_prod_set s (monic_irreducibles_bounded s n)) *) 1694(* Proof: by poly_master_subfield_factors, subring_poly_master *) 1695val poly_master_subfield_factors_alt = store_thm( 1696 "poly_master_subfield_factors_alt", 1697 ``!(r s):'a field n. FiniteField r /\ s <<= r /\ 0 < n ==> 1698 (master (CARD B ** n) = poly_prod_set s (monic_irreducibles_bounded s n))``, 1699 metis_tac[poly_master_subfield_factors, subring_poly_master, subfield_is_subring]); 1700 1701(* This is a milestone theorem. *) 1702 1703(* Theorem: FiniteField r ==> !n. 0 < n ==> (master (CARD R ** n) = PPROD (monic_irreducibles_bounded r n)) *) 1704(* Proof: by poly_master_subfield_factors, taking s = r. *) 1705val poly_master_monic_irreducible_factors = store_thm( 1706 "poly_master_monic_irreducible_factors", 1707 ``!r:'a field. FiniteField r ==> 1708 !n. 0 < n ==> (master (CARD R ** n) = PPROD (monic_irreducibles_bounded r n))``, 1709 metis_tac[poly_master_subfield_factors, finite_field_is_field, subfield_refl]); 1710 1711(* Theorem: FiniteField r ==> !s. s <<= r ==> 1712 (master (CARD R) = poly_prod_set s (monic_irreducibles_bounded s (r <:> s))) *) 1713(* Proof: 1714 Since Master s (CARD R) = master (CARD R) by subring_poly_master 1715 and (CARD R = (CARD B) ** (r <:> s)) 1716 and 0 < (r <:> s) by finite_subfield_card_eqn 1717 The result follows by poly_master_subfield_factors 1718*) 1719val poly_master_eq_irreducibles_product = store_thm( 1720 "poly_master_eq_irreducibles_product", 1721 ``!r:'a field. FiniteField r ==> !s. s <<= r ==> 1722 (master (CARD R) = poly_prod_set s (monic_irreducibles_bounded s (r <:> s)))``, 1723 rpt (stripDup[FiniteField_def]) >> 1724 `s <= r` by rw[subfield_is_subring] >> 1725 `Master s (CARD R) = master (CARD R)` by rw[subring_poly_master] >> 1726 `(CARD R = CARD B ** (r <:> s)) /\ 0 < (r <:> s)` by rw[finite_subfield_card_eqn] >> 1727 metis_tac[poly_master_subfield_factors]); 1728 1729(* ------------------------------------------------------------------------- *) 1730(* Counting Monic Irreducible Polynomials *) 1731(* ------------------------------------------------------------------------- *) 1732 1733(* Define the count of monic irreducible polynomials of a fixed degree in subfield *) 1734val monic_irreducibles_count_def = Define` 1735 monic_irreducibles_count (r:'a ring) n = CARD (monic_irreducibles_degree r n) 1736`; 1737 1738(* Theorem: FiniteRing r ==> !n. deg (Psi n) = n * (monic_irreducibles_count r n) *) 1739(* Proof: 1740 Let s = monic_irreducibles_degree r n. 1741 Then FINITE s by monic_irreducibles_degree_finite 1742 and !p. p IN s ==> monic p by monic_irreducibles_degree_member 1743 also !p. p IN s ==> deg p = n by monic_irreducibles_degree_member 1744 Thus deg (PPROD s) 1745 = SIGMA deg s by poly_monic_prod_set_deg 1746 = n * CARD s by SIGMA_CONSTANT 1747 = n * (monic_irreducibles_count r n) by monic_irreducibles_count_def 1748*) 1749val monic_irreducibles_degree_prod_set_deg = store_thm( 1750 "monic_irreducibles_degree_prod_set_deg", 1751 ``!r:'a ring. FiniteRing r ==> !n. deg (Psi n) = n * (monic_irreducibles_count r n)``, 1752 rw[FiniteRing_def] >> 1753 `#0 IN R` by rw[] >> 1754 qabbrev_tac `s = monic_irreducibles_degree r n` >> 1755 `FINITE s` by rw[monic_irreducibles_degree_finite, Abbr`s`] >> 1756 `!p. p IN s ==> monic p /\ (deg p = n)` by rw[monic_irreducibles_degree_member, Abbr`s`] >> 1757 `deg (PPROD s) = SIGMA deg s` by rw[poly_monic_prod_set_deg] >> 1758 `_ = n * CARD s` by rw[SIGMA_CONSTANT] >> 1759 rw[monic_irreducibles_count_def, Abbr`s`]); 1760 1761(* Theorem: FiniteRing r ==> 1762 (deg o PPROD o monic_irreducibles_degree r = (\d. d * (monic_irreducibles_count r d))) *) 1763(* Proof: 1764 Since (deg o PPROD o monic_irreducibles_degree r) n 1765 = deg (Psi n) by application 1766 = n * monic_irreducibles_count r n by monic_irreducibles_degree_prod_set_deg 1767 = (\d. d * (monic_irreducibles_count r d)) n by application 1768 Hence the functions are equal by FUN_EQ_THM 1769*) 1770val monic_irreducibles_degree_prod_set_deg_fun = store_thm( 1771 "monic_irreducibles_degree_prod_set_deg_fun", 1772 ``!r:'a ring. FiniteRing r ==> 1773 (deg o PPROD o monic_irreducibles_degree r = (\d. d * (monic_irreducibles_count r d)))``, 1774 rw[monic_irreducibles_degree_prod_set_deg, FUN_EQ_THM]); 1775 1776(* Theorem: n <> m ==> DISJOINT (monic_irreducibles_degree r n) (monic_irreducibles_degree r m) *) 1777(* Proof: 1778 Let s = monic_irreducibles_degree r n 1779 t = monic_irreducibles_degree r m 1780 By contradiction, suppose ~(DISJOINT s t), 1781 or s INTER t <> {} by DISJOINT_DEF 1782 Then ?e. e IN (s INTER t) by MEMBER_NOT_EMPTY 1783 or ?e. e IN s /\ e IN t by IN_INTER 1784 Thus e IN s ==> deg e = n by monic_irreducibles_degree_member 1785 and e IN t ==> deg e = m by monic_irreducibles_degree_member 1786 This contradicts n <> m. 1787*) 1788val monic_irreducibles_degree_disjoint = store_thm( 1789 "monic_irreducibles_degree_disjoint", 1790 ``!r:'a ring. !n m. n <> m ==> DISJOINT (monic_irreducibles_degree r n) (monic_irreducibles_degree r m)``, 1791 metis_tac[DISJOINT_DEF, IN_INTER, MEMBER_NOT_EMPTY, monic_irreducibles_degree_member]); 1792 1793(* Theorem: PAIR_DISJOINT (IMAGE (monic_irreducibles_degree r) (divisors n)) *) 1794(* Proof: 1795 Let s = monic_irreducibles_degree r x 1796 t = monic_irreducibles_degree r x' 1797 By IN_IMAGE, this is to show: 1798 x IN divisors n /\ x' IN divisors n /\ s <> t ==> DISJOINT s t 1799 Since s <> t ==> x <> x', hence true by monic_irreducibles_degree_disjoint 1800*) 1801val monic_irreducibles_degree_pair_disjoint = store_thm( 1802 "monic_irreducibles_degree_pair_disjoint", 1803 ``!r:'a ring. !n. PAIR_DISJOINT (IMAGE (monic_irreducibles_degree r) (divisors n))``, 1804 metis_tac[IN_IMAGE, monic_irreducibles_degree_disjoint]); 1805 1806(* Theorem: FiniteField r ==> !p. monic p /\ ipoly p ==> 1807 !n. p pdivides Psi n <=> p IN (monic_irreducibles_degree r n) *) 1808(* Proof: 1809 Let s = monic_irreducibles_degree r n. 1810 Note FINITE s by monic_irreducibles_degree_finite 1811 and miset s by monic_irreducibles_degree_member 1812 Hence p pdivides PPROD s ==> p IN s by poly_prod_monic_irreducible_set_divisor 1813*) 1814val monic_irreducibles_degree_prod_set_divisor = store_thm( 1815 "monic_irreducibles_degree_prod_set_divisor", 1816 ``!r:'a ring. FiniteField r ==> !p. monic p /\ ipoly p ==> 1817 !n. p pdivides Psi n <=> p IN (monic_irreducibles_degree r n)``, 1818 rpt (stripDup[FiniteField_def]) >> 1819 `Ring r /\ #0 IN R` by rw[] >> 1820 qabbrev_tac `s = monic_irreducibles_degree r n` >> 1821 `FINITE s` by rw[monic_irreducibles_degree_finite, Abbr`s`] >> 1822 `miset s` by rw[monic_irreducibles_degree_member, Abbr`s`] >> 1823 rw[poly_prod_monic_irreducible_set_divisor]); 1824 1825(* Theorem: FiniteField r ==> 1826 !n. INJ PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) univ(:'a poly) *) 1827(* Proof: 1828 Let s = monic_irreducibles_degree r x 1829 t = monic_irreducibles_degree r y 1830 By INJ_DEF, this is to show: 1831 x IN divisors n /\ y IN divisors n /\ (PPROD s = PPROD t) ==> (s = t) 1832 Since FINITE s /\ FINITE t by monic_irreducibles_degree_finite 1833 and miset s /\ miset t by monic_irreducibles_degree_member 1834 With PPROD s = PPROD t by given 1835 Hence s = t by poly_prod_monic_irreducible_set_eq 1836*) 1837val monic_irreducibles_degree_poly_prod_inj = store_thm( 1838 "monic_irreducibles_degree_poly_prod_inj", 1839 ``!r:'a field. FiniteField r ==> !n. INJ PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) univ(:'a poly)``, 1840 rpt (stripDup[FiniteField_def]) >> 1841 `Ring r /\ #0 IN R` by rw[] >> 1842 rw[INJ_DEF] >> 1843 qabbrev_tac `s = monic_irreducibles_degree r x'` >> 1844 qabbrev_tac `t = monic_irreducibles_degree r x''` >> 1845 `FINITE s /\ FINITE t` by rw[monic_irreducibles_degree_finite, Abbr`s`, Abbr`t`] >> 1846 `miset s /\ miset t` by rw[monic_irreducibles_degree_member, Abbr`s`, Abbr`t`] >> 1847 metis_tac[poly_prod_monic_irreducible_set_eq]); 1848 1849(* Note: 1850 This assertion: INJ (monic_irreducibles_degree r) (divisors n) univ(:'a poly -> bool) 1851 is vital for the last step of monic_irreducibles_bounded_prod_set_deg. 1852 This is valid only if !d. monic_irreducibles_degree r d <> {}. 1853 However, this is precisely the result we want after having this degree expression, 1854 (then compare to the degree of master equation, apply Mobius Inversion, etc.) 1855 If we know !d. monic_irreducibles_degree r d <> {}, we don't need to get into this 1856 trouble to establish (monic_irreducibles_count r n)! 1857 1858 So, how to get around this obstacle? 1859 The strategy is this: 1860 For the image of the map, IMAGE (monic_irreducibles_degree r) (divisors n) 1861 assume that for some divisors d of n, monic_irreducibles_degree r d = {} 1862 then for other divisors d of n, monic_irreducibles_degree r d <> {} 1863 Partition (divisors n) into these two parts, then the image is split into two: 1864 IMAGE (monic_irreducibles_degree r) (divisors n) 1865 = IMAGE (monic_irreducibles_degree r) (part1 UNION part2) 1866 = IMAGE (monic_irreducibles_degree r) (part1) UNION 1867 IMAGE (monic_irreducibles_degree r) (part2) by IMAGE_UNION 1868 Since these two images are disjoint, the sum splits into two. 1869 The first sum is zero, since PPROD {} = |1|, and deg |1| = 0. 1870 The second sum can apply INJ, since monic_irreducibles_degree r d <> {} by construction. 1871*) 1872 1873(* Theorem: !s. FINITE s /\ (!d. d IN s ==> monic_irreducibles_degree r d <> {}) ==> 1874 INJ (monic_irreducibles_degree r) s univ(:'a poly -> bool) *) 1875(* Proof: 1876 By INJ_DEF, this is to show: 1877 x IN divisors n /\ y IN divisors n /\ 1878 monic_irreducibles_degree r x = monic_irreducibles_degree r y ==> x = y 1879 Let s = monic_irreducibles_degree r x, 1880 t = monic_irreducibles_degree r y. 1881 By contradiction, assume x <> y. 1882 Then DISJOINT s t by monic_irreducibles_degree_disjoint 1883 or s INTER t = {} by DISJOINT_DEF 1884 Given s = t, s INTER t = s by INTER_IDEMPOT 1885 This gives s = {}, 1886 which contradicts s <> {} by given implication. 1887*) 1888val monic_irreducibles_degree_nonempty_inj = store_thm( 1889 "monic_irreducibles_degree_nonempty_inj", 1890 ``!r:'a ring. !s. FINITE s /\ (!d. d IN s ==> monic_irreducibles_degree r d <> {}) ==> 1891 INJ (monic_irreducibles_degree r) s univ(:'a poly -> bool)``, 1892 rw[INJ_DEF] >> 1893 metis_tac[monic_irreducibles_degree_disjoint, INTER_IDEMPOT, DISJOINT_DEF]); 1894 1895(* Theorem: SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = 1896 SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n) *) 1897(* Proof: 1898 Let f = monic_irreducibles_degree r, 1899 s1 = {d | d IN (divisors n) /\ (f d = {})}, 1900 s2 = {d | d IN (divisors n) /\ (f d <> {})}. 1901 Then divisors n = s1 UNION s2 by EXTENSION 1902 and DISJOINT s1 s2 by EXTENSION, DISJOINT_DEF 1903 and DISJOINT (IMAGE f s1) (IMAGE f s2) by EXTENSION, DISJOINT_DEF 1904 Now s1 SUBSET (divisors n) by SUBSET_DEF 1905 s2 SUBSET (divisors n) by SUBSET_DEF 1906 Since FINITE (divisors n) by divisors_finite 1907 thus FINITE s1 /\ FINITE s2 by SUBSET_FINITE 1908 and FINITE (IMAGE f s1) /\ FINITE (IMAGE f s2) by IMAGE_FINITE 1909 1910 Step 1: decompose left summation 1911 SIGMA (deg o PPROD) (IMAGE f (divisors n)) 1912 = SIGMA (deg o PPROD) (IMAGE f (s1 UNION s2)) by above, divisors n = s1 UNION s2 1913 = SIGMA (deg o PPROD) ((IMAGE f s1) UNION (IMAGE f s2)) by IMAGE_UNION 1914 = SIGMA (deg o PPROD) (IMAGE f s1) + 1915 SIGMA (deg o PPROD) (IMAGE f s2) by SUM_IMAGE_DISJOINT 1916 1917 Claim: SIGMA (deg o PPROD) (IMAGE f s1) = 0 1918 Proof: If s1 = {}, 1919 SIGMA (deg o PPROD) (IMAGE f {}) 1920 = SIGMA (deg o PPROD) {} by IMAGE_EMPTY 1921 = 0 by SUM_IMAGE_EMPTY 1922 If s1 <> {}, 1923 Note !d. d IN s1 ==> (f d = {}) by definition of s1 1924 Thus !x. x IN (IMAGE f s1) ==> (x = {}) by IN_IMAGE, IMAGE_EMPTY 1925 Since s1 <> {}, IMAGE f s1 = {{}} by SING_DEF, IN_SING, SING_ONE_ELEMENT 1926 SIGMA (deg o PPROD) (IMAGE f {}) 1927 = SIGMA (deg o PPROD) {{}} by above 1928 = (deg o PPROD) {} by SUM_IMAGE_SING 1929 = deg (PPROD {}) by function application 1930 = deg |1| by poly_prod_set_empty 1931 = 0 by poly_deg_one 1932 1933 Step 2: decompose right summation 1934 Also SIGMA (deg o PPROD o f) (divisors n) 1935 = SIGMA (deg o PPROD o f) (s1 UNION s2) by above, divisors n = s1 UNION s2 1936 = SIGMA (deg o PPROD o f) s1 + 1937 SIGMA (deg o PPROD o f) s2 by SUM_IMAGE_DISJOINT 1938 1939 Claim: SIGMA (deg o PPROD o f) s1 = 0 1940 Proof: Note !d. d IN s1 ==> (f d = {}) by definition of s1 1941 (deg o PPROD o f) d 1942 = deg (PPROD (f d)) by function application 1943 = deg (PPROD {}) by above 1944 = deg |1| by poly_prod_set_empty 1945 = 0 by poly_deg_one 1946 Hence SIGMA (deg o PPROD o f) s1 1947 = 0 * CARD s1 by SIGMA_CONSTANT 1948 = 0 by MULT 1949 1950 Claim: SIGMA (deg o PPROD) (IMAGE f s2) = SIGMA (deg o PPROD o f) (s2) 1951 Proof: Note !d. d IN s2 ==> f d <> {} by definition of s2 1952 Thus INJ f s2 univ(:'a poly -> bool) by monic_irreducibles_degree_nonempty_inj 1953 Hence SIGMA (deg o PPROD) (IMAGE f s2) 1954 = SIGMA (deg o PPROD o f) (s2) by sum_image_by_composition 1955 1956 Result follows by combining all the claims and arithmetic. 1957*) 1958val monic_irreducibles_degree_poly_prod_deg_sum = store_thm( 1959 "monic_irreducibles_degree_poly_prod_deg_sum", 1960 ``!r:'a ring. !n. SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = 1961 SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n)``, 1962 rpt strip_tac >> 1963 qabbrev_tac `f = monic_irreducibles_degree r` >> 1964 qabbrev_tac `s1 = {d | d IN (divisors n) /\ (f d = {})}` >> 1965 qabbrev_tac `s2 = {d | d IN (divisors n) /\ (f d <> {})}` >> 1966 (`divisors n = s1 UNION s2` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION] >> metis_tac[])) >> 1967 (`DISJOINT s1 s2` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION, DISJOINT_DEF] >> metis_tac[])) >> 1968 (`DISJOINT (IMAGE f s1) (IMAGE f s2)` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION, DISJOINT_DEF] >> metis_tac[])) >> 1969 `s1 SUBSET (divisors n) /\ s2 SUBSET (divisors n)` by rw[Abbr`s1`, Abbr`s2`, SUBSET_DEF] >> 1970 `FINITE (divisors n)` by rw[divisors_finite] >> 1971 `FINITE s1 /\ FINITE s2` by metis_tac[SUBSET_FINITE] >> 1972 `FINITE (IMAGE f s1) /\ FINITE (IMAGE f s2)` by rw[] >> 1973 `SIGMA (deg o PPROD) (IMAGE f (divisors n)) = SIGMA (deg o PPROD) ((IMAGE f s1) UNION (IMAGE f s2))` by rw[] >> 1974 `_ = SIGMA (deg o PPROD) (IMAGE f s1) + SIGMA (deg o PPROD) (IMAGE f s2)` by rw[SUM_IMAGE_DISJOINT] >> 1975 `SIGMA (deg o PPROD) (IMAGE f s1) = 0` by 1976 (Cases_on `s1 = {}` >- 1977 rw[SUM_IMAGE_EMPTY] >> 1978 `!d. d IN s1 ==> (f d = {})` by rw[Abbr`s1`] >> 1979 `!x. x IN (IMAGE f s1) ==> (x = {})` by metis_tac[IN_IMAGE, IMAGE_EMPTY] >> 1980 `{} IN {{}} /\ IMAGE f s1 <> {}` by rw[] >> 1981 `IMAGE f s1 = {{}}` by metis_tac[SING_DEF, IN_SING, SING_ONE_ELEMENT] >> 1982 `SIGMA (deg o PPROD) (IMAGE f s1) = (deg o PPROD) {}` by rw[SUM_IMAGE_SING] >> 1983 rw[poly_prod_set_empty] 1984 ) >> 1985 `SIGMA (deg o PPROD o f) (divisors n) = SIGMA (deg o PPROD o f) s1 + SIGMA (deg o PPROD o f) s2` by rw[SUM_IMAGE_DISJOINT] >> 1986 `SIGMA (deg o PPROD o f) s1 = 0` by 1987 (`!d. d IN s1 ==> (f d = {})` by rw[Abbr`s1`] >> 1988 `!d. d IN s1 ==> ((deg o PPROD o f) d = 0)` by rw[poly_prod_set_empty] >> 1989 metis_tac[SIGMA_CONSTANT, MULT]) >> 1990 `SIGMA (deg o PPROD) (IMAGE f s2) = SIGMA (deg o PPROD o f) s2` by 1991 (`!d. d IN s2 ==> f d <> {}` by rw[Abbr`s2`] >> 1992 `INJ f s2 univ(:'a poly -> bool)` by rw[monic_irreducibles_degree_nonempty_inj, Abbr`f`] >> 1993 rw[sum_image_by_composition]) >> 1994 rw[]); 1995 1996(* This proof is unusual, unexpected, highly specialized and unique. *) 1997(* This is so unique for the next theorem that it will be a local lemma. *) 1998 1999(* Extract a general theorem from above and prove lemma again by using the general theorem *) 2000 2001(* Theorem: SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = 2002 SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n) *) 2003(* Proof: 2004 Let s = divisors n, 2005 f = deg o PPROD, 2006 g = monic_irreducibles_degree r. 2007 The goal is to show: SIGMA f (IMAGE g s) = SIGMA (deg o PPROD o g) s 2008 Use sum_image_by_composition_with_partial_inj. 2009 2010 Now FINITE s by divisors_finite 2011 and f {} 2012 = (deg o PPROD) {} by notation of f 2013 = deg (PPROD {}) by function application 2014 = deg |1| by poly_prod_set_empty 2015 = 0 by poly_deg_one 2016 Also !t. FINITE t /\ (!x. x IN t ==> g x <> {}) ==> 2017 INJ g t univ(:'a poly -> bool) by monic_irreducibles_degree_nonempty_inj 2018 Hence SIGMA f (IMAGE g s) 2019 = SIGMA (f o g) s by sum_image_by_composition_with_partial_inj 2020 = SIGMA ((deg o PPROD) o g) s by notation of f 2021 = SIGMA (deg o PPROD o g) s by combinTheory.o_ASSOC 2022*) 2023val monic_irreducibles_degree_poly_prod_deg_sum = store_thm( 2024 "monic_irreducibles_degree_poly_prod_deg_sum", 2025 ``!r:'a ring. !n. SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = 2026 SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n)``, 2027 rpt strip_tac >> 2028 rewrite_tac[combinTheory.o_ASSOC] >> 2029 (irule sum_image_by_composition_with_partial_inj >> rpt conj_tac) >- 2030 rw_tac std_ss[monic_irreducibles_degree_nonempty_inj] >- 2031 rw_tac std_ss[divisors_finite] >> 2032 rw_tac std_ss[poly_prod_set_empty, poly_deg_one]); 2033 2034(* Note: 2035 Again, the following is easy (?) if we know (monic_irreducibles_degree r n) is nonempty, 2036 which gives an easy proof of the fact: INJ (monic_irreducibles_degree r) (divisors n) univ(:'a poly -> bool). 2037 However, we would like to use this result to establish (monic_irreducibles_degree r n) is nonempty. 2038 How to overcome this obstacle? Use the magic of monic_irreducibles_degree_poly_prod_deg_sum above! 2039*) 2040 2041(* Next is the first part of monic_irreducibles_bounded_prod_set_deg *) 2042 2043(* Theorem: FiniteField r ==> !n. PPROD (monic_irreducibles_bounded r n) = 2044 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) *) 2045(* Proof: 2046 Let P = IMAGE (monic_irreducibles_degree r) (divisors n). 2047 Since FINITE (divisors n) by divisors_finite 2048 so FINITE P by IMAGE_FINITE 2049 Also EVERY_FINITE P by monic_irreducibles_degree_finite, IN_IMAGE, FINITE R /\ #0 IN R 2050 and PAIR_DISJOINT P by monic_irreducibles_degree_pair_disjoint 2051 and EVERY_PSET P by monic_irreducibles_degree_member, IN_IMAGE, poly_monic_poly 2052 Note poly_set_multiplicative_fun r PPROD by poly_prod_set_mult_fun, Ring r 2053 and INJ PPROD P univ(:'a poly) by monic_irreducibles_degree_poly_prod_inj, FiniteField r 2054 Also FINITE (IMAGE PPROD P) by IMAGE_FINITE 2055 and mset (IMAGE PPROD P) by poly_monic_prod_set_monic, monic_irreducibles_degree_member 2056 2057 PPROD (monic_irreducibles_bounded r n) 2058 = PPROD (BIGUNION P) by monic_irreducibles_bounded_def 2059 = PPROD (IMAGE PPROD P) by poly_disjoint_bigunion_mult_fun 2060*) 2061val monic_irreducibles_bounded_prod_set = store_thm( 2062 "monic_irreducibles_bounded_prod_set", 2063 ``!r:'a field. FiniteField r ==> !n. PPROD (monic_irreducibles_bounded r n) = 2064 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n))``, 2065 rpt (stripDup[FiniteField_def]) >> 2066 `Ring r /\ #0 IN R` by rw[] >> 2067 qabbrev_tac `P = IMAGE (monic_irreducibles_degree r) (divisors n)` >> 2068 `FINITE (divisors n)` by rw[divisors_finite] >> 2069 `FINITE P` by rw[Abbr`P`] >> 2070 `EVERY_FINITE P` by metis_tac[monic_irreducibles_degree_finite, IN_IMAGE] >> 2071 `PAIR_DISJOINT P` by metis_tac[monic_irreducibles_degree_pair_disjoint] >> 2072 `EVERY_PSET P` by metis_tac[monic_irreducibles_degree_member, IN_IMAGE, poly_monic_poly] >> 2073 `poly_set_multiplicative_fun r PPROD` by rw[poly_prod_set_mult_fun] >> 2074 `INJ PPROD P univ(:'a poly)` by rw[monic_irreducibles_degree_poly_prod_inj, Abbr`P`] >> 2075 `FINITE (IMAGE PPROD P)` by rw[] >> 2076 `mset (IMAGE PPROD P)` by prove_tac[poly_monic_prod_set_monic, monic_irreducibles_degree_member, IN_IMAGE] >> 2077 metis_tac[monic_irreducibles_bounded_def, poly_disjoint_bigunion_mult_fun]); 2078 2079(* Theorem: FiniteField r ==> !n. deg (PPROD (monic_irreducibles_bounded r n)) = 2080 SIGMA (\d. d * (monic_irreducibles_count r d)) (divisors n) *) 2081(* Proof: 2082 Note FiniteField r ==> FiniteRing r by finite_field_is_finite_ring 2083 for monic_irreducibles_degree_prod_set_deg_fun 2084 Let P = IMAGE (monic_irreducibles_degree r) (divisors n). 2085 Since FINITE (divisors n) by divisors_finite 2086 so FINITE P by IMAGE_FINITE 2087 Also EVERY_FINITE P by monic_irreducibles_degree_finite, IN_IMAGE, FINITE R /\ #0 IN R 2088 and PAIR_DISJOINT P by monic_irreducibles_degree_pair_disjoint 2089 and EVERY_PSET P by monic_irreducibles_degree_member, IN_IMAGE, poly_monic_poly 2090 Note poly_set_multiplicative_fun r PPROD by poly_prod_set_mult_fun, Ring r 2091 and INJ PPROD P univ(:'a poly) by monic_irreducibles_degree_poly_prod_inj, FiniteField r 2092 Also FINITE (IMAGE PPROD P) by IMAGE_FINITE 2093 and mset (IMAGE PPROD P) by poly_monic_prod_set_monic, monic_irreducibles_degree_member 2094 2095 deg (PPROD (monic_irreducibles_bounded r n)) 2096 = deg (PPROD (BIGUNION P)) by monic_irreducibles_bounded_def 2097 = deg (PPROD (IMAGE PPROD P)) by poly_disjoint_bigunion_mult_fun 2098 = SIGMA deg (IMAGE PPROD P) by poly_monic_prod_set_deg 2099 = SIGMA (deg o PPROD) P by sum_image_by_composition, INJ PPROD 2100 = SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n) by monic_irreducibles_degree_poly_prod_deg_sum 2101 = SIGMA (\d. d * (monic_irreducibles_count r d)) (divisors n) by monic_irreducibles_degree_prod_set_deg_fun 2102*) 2103val monic_irreducibles_bounded_prod_set_deg = store_thm( 2104 "monic_irreducibles_bounded_prod_set_deg", 2105 ``!r:'a field. FiniteField r ==> !n. deg (PPROD (monic_irreducibles_bounded r n)) = 2106 SIGMA (\d. d * (monic_irreducibles_count r d)) (divisors n)``, 2107 rpt (stripDup[FiniteField_def]) >> 2108 `Ring r /\ #0 IN R` by rw[] >> 2109 `FiniteRing r` by rw[finite_field_is_finite_ring] >> 2110 qabbrev_tac `P = IMAGE (monic_irreducibles_degree r) (divisors n)` >> 2111 `FINITE (divisors n)` by rw[divisors_finite] >> 2112 `FINITE P` by rw[Abbr`P`] >> 2113 `EVERY_FINITE P` by metis_tac[monic_irreducibles_degree_finite, IN_IMAGE] >> 2114 `PAIR_DISJOINT P` by metis_tac[monic_irreducibles_degree_pair_disjoint] >> 2115 `EVERY_PSET P` by metis_tac[monic_irreducibles_degree_member, IN_IMAGE, poly_monic_poly] >> 2116 `poly_set_multiplicative_fun r PPROD` by rw[poly_prod_set_mult_fun] >> 2117 `INJ PPROD P univ(:'a poly)` by rw[monic_irreducibles_degree_poly_prod_inj, Abbr`P`] >> 2118 `FINITE (IMAGE PPROD P)` by rw[] >> 2119 `mset (IMAGE PPROD P)` by prove_tac[poly_monic_prod_set_monic, monic_irreducibles_degree_member, IN_IMAGE] >> 2120 `deg (PPROD (monic_irreducibles_bounded r n)) = deg (PPROD (BIGUNION P))` by rw[monic_irreducibles_bounded_def, Abbr`P`] >> 2121 `_ = deg (PPROD (IMAGE PPROD P))` by metis_tac[poly_disjoint_bigunion_mult_fun] >> 2122 `_ = SIGMA deg (IMAGE PPROD P)` by rw[poly_monic_prod_set_deg] >> 2123 `_ = SIGMA (deg o PPROD) P` by rw[sum_image_by_composition] >> 2124 `_ = SIGMA ((deg o PPROD) o monic_irreducibles_degree r) (divisors n)` by rw[monic_irreducibles_degree_poly_prod_deg_sum, Abbr`P`] >> 2125 `_ = SIGMA (\d. d * (monic_irreducibles_count r d)) (divisors n)` by rw[monic_irreducibles_degree_prod_set_deg_fun] >> 2126 rw[]); 2127 2128(* ------------------------------------------------------------------------- *) 2129(* Finite Field and Subfield Order *) 2130(* ------------------------------------------------------------------------- *) 2131 2132(* Theorem: FiniteField r ==> !s. s <<= r ==> 2133 !n. 0 < n ==> (CARD B ** n = SIGMA (\d. d * (monic_irreducibles_count s d)) (divisors n)) *) 2134(* Proof: 2135 Note FiniteField s by subfield_finite_field 2136 so 1 < CARD B by finite_field_card_gt_1, FiniteField s 2137 and 1 < CARD B ** n by ONE_LT_EXP, 1 < CARD B, 0 < n 2138 2139 CARD B ** n 2140 = poly_deg s (Master s (CARD B ** n)) by poly_master_deg 2141 = poly_deg s (poly_prod_set s (monic_irreducibles_bounded s n)) by poly_master_subfield_factors 2142 = SIGMA (\d. d * (monic_irreducibles_count s d)) (divisors n) by monic_irreducibles_bounded_prod_set_deg 2143*) 2144val finite_subfield_card_exp_eqn = store_thm( 2145 "finite_subfield_card_exp_eqn", 2146 ``!r:'a field. FiniteField r ==> !s. s <<= r ==> 2147 !n. 0 < n ==> (CARD B ** n = SIGMA (\d. d * (monic_irreducibles_count s d)) (divisors n))``, 2148 rpt (stripDup[FiniteField_def]) >> 2149 `FiniteField s` by metis_tac[subfield_finite_field] >> 2150 `1 < CARD B` by rw[finite_field_card_gt_1] >> 2151 `1 < CARD B ** n` by rw[ONE_LT_EXP] >> 2152 `Ring s /\ s.prod.id <> s.sum.id` by rw[] >> 2153 metis_tac[poly_master_deg, poly_master_subfield_factors, monic_irreducibles_bounded_prod_set_deg]); 2154 2155(* Theorem: FiniteField r ==> 2156 !n. 0 < n ==> (CARD R ** n = SIGMA (\d. d * (monic_irreducibles_count r d)) (divisors n)) *) 2157(* Proof: 2158 Since FiniteField r 2159 ==> Field r by finite_field_is_field 2160 and subfield r r by subfield_refl 2161 This is true by finite_subfield_card_exp_eqn 2162*) 2163val finite_field_card_exp_eqn = store_thm( 2164 "finite_field_card_exp_eqn", 2165 ``!r:'a field. FiniteField r ==> 2166 !n. 0 < n ==> (CARD R ** n = SIGMA (\d. d * (monic_irreducibles_count r d)) (divisors n))``, 2167 metis_tac[finite_field_is_field, subfield_refl, finite_subfield_card_exp_eqn]); 2168 2169(* This is a milestone theorem. *) 2170 2171(* ------------------------------------------------------------------------- *) 2172(* Roots of Master is a Subfield *) 2173(* ------------------------------------------------------------------------- *) 2174 2175(* Theorem: FiniteField r ==> !n. #0 IN roots (master ((char r) ** n)) *) 2176(* Proof: 2177 Let m = (char r) ** n, p = master m. 2178 Note 0 < char r by finite_field_char_pos, FiniteField r 2179 so 0 < m by EXP_POS, 0 < char r 2180 Thus root p #0 by poly_master_root_zero 2181 or #0 IN roots p by poly_roots_member 2182*) 2183val poly_master_roots_char_n_zero = store_thm( 2184 "poly_master_roots_char_n_zero", 2185 ``!r:'a field. FiniteField r ==> !n. #0 IN roots (master ((char r) ** n))``, 2186 rpt (stripDup[FiniteField_def]) >> 2187 `0 < (char r) ** n` by rw[finite_field_char_pos, EXP_POS] >> 2188 rw[poly_master_root_zero, poly_roots_member]); 2189 2190(* Theorem: FiniteField r ==> !n. let p = master ((char r) ** n) in 2191 !x y. x IN roots p /\ y IN roots p ==> (x + y) IN roots p *) 2192(* Proof: 2193 Let m = (char r) ** n, p = master m. 2194 Then x IN R /\ (x ** m = x) by poly_master_roots 2195 and y IN R /\ (y ** m = y) by poly_master_roots 2196 Now x + y IN R by field_add_element 2197 and (x + y) ** m 2198 = x ** m + y ** m by finite_field_freshman_all, FiniteField r 2199 = x + y by above 2200 Thus (x + y) IN roots p by poly_master_roots 2201*) 2202val poly_master_roots_add_root = store_thm( 2203 "poly_master_roots_add_root", 2204 ``!r:'a field. FiniteField r ==> !n. let p = master ((char r) ** n) in 2205 !x y. x IN roots p /\ y IN roots p ==> (x + y) IN roots p``, 2206 rpt (stripDup[FiniteField_def]) >> 2207 qabbrev_tac `m = (char r) ** n` >> 2208 rw_tac std_ss[] >> 2209 `Ring r` by rw[] >> 2210 `x IN R /\ (x ** m = x)` by metis_tac[poly_master_roots] >> 2211 `y IN R /\ (y ** m = y)` by metis_tac[poly_master_roots] >> 2212 `x + y IN R` by rw[] >> 2213 `(x + y) ** m = x ** m + y ** m` by rw[finite_field_freshman_all, Abbr`m`] >> 2214 `_ = x + y` by rw[] >> 2215 metis_tac[poly_master_roots]); 2216 2217(* Theorem: FiniteField r ==> !n. let p = master ((char r) ** n) in 2218 !x y. x IN roots p /\ y IN roots p ==> (x - y) IN roots p *) 2219(* Proof: 2220 Let m = (char r) ** n, p = master m. 2221 Then x IN R /\ (x ** m = x) by poly_master_roots 2222 and y IN R /\ (y ** m = y) by poly_master_roots 2223 Now x - y IN R by field_sub_element 2224 and (x - y) ** m 2225 = x ** m - y ** m by finite_field_freshman_all_sub, FiniteField r 2226 = x - y by above 2227 Thus (x - y) IN roots p by poly_master_roots 2228*) 2229val poly_master_roots_sub_root = store_thm( 2230 "poly_master_roots_sub_root", 2231 ``!r:'a field. FiniteField r ==> !n. let p = master ((char r) ** n) in 2232 !x y. x IN roots p /\ y IN roots p ==> (x - y) IN roots p``, 2233 rpt (stripDup[FiniteField_def]) >> 2234 qabbrev_tac `m = (char r) ** n` >> 2235 rw_tac std_ss[] >> 2236 `Ring r` by rw[] >> 2237 `x IN R /\ (x ** m = x)` by metis_tac[poly_master_roots] >> 2238 `y IN R /\ (y ** m = y)` by metis_tac[poly_master_roots] >> 2239 `x - y IN R` by rw[] >> 2240 `(x - y) ** m = x ** m - y ** m` by rw[finite_field_freshman_all_sub, Abbr`m`] >> 2241 `_ = x - y` by rw[] >> 2242 metis_tac[poly_master_roots]); 2243 2244(* Theorem: FiniteField r ==> !n. let p = master ((char r) ** n) in !x. x IN roots p ==> -x IN roots p *) 2245(* Proof: 2246 Let m = (char r) ** n, p = master m. 2247 Then 0 < char r by finite_field_char_pos, FiniteField r 2248 so 0 < m by EXP_POS 2249 Thus #0 IN roots p by poly_master_root_zero, poly_roots_member 2250 Also x IN R by poly_master_roots 2251 and #0 - x = -x by field_zero_sub 2252 Thus -x IN roots p by poly_master_roots_sub_root 2253*) 2254val poly_master_roots_neg_root = store_thm( 2255 "poly_master_roots_neg_root", 2256 ``!r:'a field. FiniteField r ==> !n. let p = master ((char r) ** n) in !x. x IN roots p ==> -x IN roots p``, 2257 rpt (stripDup[FiniteField_def]) >> 2258 qabbrev_tac `m = (char r) ** n` >> 2259 rw_tac std_ss[] >> 2260 `Ring r /\ #0 IN R` by rw[] >> 2261 `0 < m` by rw[finite_field_char_pos, EXP_POS, Abbr`m`] >> 2262 `#0 IN roots p` by rw[poly_master_root_zero, poly_roots_member, Abbr`p`] >> 2263 `x IN R` by metis_tac[poly_master_roots] >> 2264 `#0 - x = -x` by rw[field_zero_sub] >> 2265 metis_tac[poly_master_roots_sub_root]); 2266 2267(* Theorem: Field r ==> !n. let p = master ((char r) ** n) in 2268 !x y. x IN roots p /\ y IN roots p ==> (x * y) IN roots p *) 2269(* Proof: 2270 Let m = (char r) ** n, p = master m. 2271 Then x IN R /\ (x ** m = x) by poly_master_roots 2272 and y IN R /\ (y ** m = y) by poly_master_roots 2273 Now x * y IN R by field_mult_element 2274 and (x * y) ** m 2275 = x ** m * y ** m by field_mult_exp, Field r 2276 = x * y by above 2277 Thus (x * y) IN roots p by poly_master_roots 2278*) 2279val poly_master_roots_mult_root = store_thm( 2280 "poly_master_roots_mult_root", 2281 ``!r:'a field. Field r ==> !n. let p = master ((char r) ** n) in 2282 !x y. x IN roots p /\ y IN roots p ==> (x * y) IN roots p``, 2283 rpt (stripDup[FiniteField_def]) >> 2284 qabbrev_tac `m = (char r) ** n` >> 2285 rw_tac std_ss[] >> 2286 `Ring r` by rw[] >> 2287 `x IN R /\ (x ** m = x)` by metis_tac[poly_master_roots] >> 2288 `y IN R /\ (y ** m = y)` by metis_tac[poly_master_roots] >> 2289 `x * y IN R` by rw[] >> 2290 `(x * y) ** m = x ** m * y ** m` by rw[field_mult_exp] >> 2291 `_ = x * y` by rw[] >> 2292 metis_tac[poly_master_roots]); 2293 2294(* Theorem: Field r ==> !n. let p = master ((char r) ** n) in 2295 !x. x IN roots p /\ x <> #0 ==> |/ x IN roots p *) 2296(* Proof: 2297 Let m = (char r) ** n, p = master m. 2298 Then x IN R /\ (x ** m = x) by poly_master_roots 2299 ==> x IN R+ by field_nonzero_eq, x <> #0 2300 ==> |/ x IN R by field_inv_element 2301 Now ( |/ x) ** m 2302 = |/ (x ** m) by field_inv_exp 2303 = |/ x by above 2304 Thus |/ x IN roots p by poly_master_roots 2305*) 2306val poly_master_roots_inv_root = store_thm( 2307 "poly_master_roots_inv_root", 2308 ``!r:'a field. Field r ==> !n. let p = master ((char r) ** n) in 2309 !x. x IN roots p /\ x <> #0 ==> |/ x IN roots p``, 2310 rpt strip_tac >> 2311 qabbrev_tac `m = (char r) ** n` >> 2312 rw_tac std_ss[] >> 2313 `Ring r` by rw[] >> 2314 `x IN R /\ (x ** m = x)` by metis_tac[poly_master_roots] >> 2315 `x IN R+` by rw[field_nonzero_eq] >> 2316 `|/ x IN R` by rw[field_inv_element] >> 2317 `( |/ x) ** m = |/ (x ** m)` by rw[field_inv_exp] >> 2318 `_ = |/ x` by rw[] >> 2319 metis_tac[poly_master_roots]); 2320 2321(* Theorem: Field r ==> !n. let p = master ((char r) ** n) in 2322 !x y. x IN roots p /\ y IN roots p /\ y <> #0 ==> (x * |/ y) IN roots p *) 2323(* Proof: by poly_master_roots_mult_root, poly_master_roots_inv_root *) 2324val poly_master_roots_div_root = store_thm( 2325 "poly_master_roots_div_root", 2326 ``!r:'a field. Field r ==> !n. let p = master ((char r) ** n) in 2327 !x y. x IN roots p /\ y IN roots p /\ y <> #0 ==> (x * |/ y) IN roots p``, 2328 metis_tac[poly_master_roots_mult_root, poly_master_roots_inv_root]); 2329 2330(* Theorem: FiniteField r ==> !n. AbelianGroup (subset_field r (roots (master ((char r) ** n)))).sum *) 2331(* Proof: 2332 Let m = (char r) ** n, p = master m. 2333 By AbelianGroup_def, group_def_alt, subset_field_property, this is to show: 2334 (1) x IN roots p /\ y IN roots p ==> x + y IN roots p 2335 This is true by poly_master_roots_add_root 2336 (2) x IN roots p /\ y IN roots p /\ z IN roots p ==> x + y + z = x + (y + z) 2337 Note x IN R /\ y IN R /\ z IN R by poly_roots_element 2338 so x + y + z = x + (y + z) by field_add_assoc 2339 (3) #0 IN roots p, true by poly_master_roots_char_n_zero 2340 (4) x IN roots p ==> #0 + x = x 2341 Note x IN R by poly_roots_element 2342 so #0 + x = x by field_add_lzero 2343 (5) x IN roots p ==> ?y. y IN roots p /\ (y + x = #0) 2344 Let y = -x, 2345 Then -x IN roots p by poly_master_roots_neg_root 2346 and x IN R by poly_roots_element 2347 so -x + x = #0 by field_add_lneg 2348 (6) x IN roots p /\ y IN roots p ==> x + y = y + x 2349 Note x IN R /\ y IN R by poly_roots_element 2350 so x + y = y + x by field_add_comm 2351*) 2352val poly_master_roots_sum_abelian_group = store_thm( 2353 "poly_master_roots_sum_abelian_group", 2354 ``!r:'a field. FiniteField r ==> !n. AbelianGroup (subset_field r (roots (master ((char r) ** n)))).sum``, 2355 rpt (stripDup[FiniteField_def]) >> 2356 qabbrev_tac `m = (char r) ** n` >> 2357 qabbrev_tac `p = master m` >> 2358 rw_tac std_ss[AbelianGroup_def, group_def_alt, subset_field_property] >- 2359 metis_tac[poly_master_roots_add_root] >- 2360 metis_tac[field_add_assoc, poly_roots_element] >- 2361 rw[poly_master_roots_char_n_zero, Abbr`p`, Abbr`m`] >- 2362 metis_tac[field_add_lzero, poly_roots_element] >- 2363 metis_tac[poly_master_roots_neg_root, field_add_lneg, poly_roots_element] >> 2364 metis_tac[field_add_comm, poly_roots_element]); 2365 2366(* Theorem: FiniteField r ==> !n. let p = master ((char r) ** n) in 2367 AbelianGroup ((subset_field r (roots p)).prod excluding (subset_field r (roots p)).sum.id) *) 2368(* Proof: 2369 Let m = (char r) ** n, p = master m. 2370 Let s = roots p DELETE #0 2371 Then !x. x IN s <=> x IN roots p /\ x <> #0 by DELETE_DEF 2372 By AbelianGroup_def, group_def_alt, excluding_def, subset_field_property, this is to show: 2373 (1) x IN roots p /\ y IN roots p ==> x * y IN roots p 2374 This is true by poly_master_roots_mult_root 2375 (2) x IN roots p /\ y IN roots p /\ x <> #0 /\ y <> #0 ==> x * y <> #0 2376 This is true by field_mult_eq_zero, poly_roots_element 2377 (3) x IN roots p /\ y IN roots p /\ z IN roots p ==> x * y * z = x * (y * z) 2378 Note x IN R /\ y IN R /\ z IN R by poly_roots_element 2379 so x + y + z = x + (y + z) by field_mult_assoc 2380 (4) #1 IN roots p 2381 This is true by poly_master_root_one, poly_roots_member 2382 (5) #1 <> #0, true by field_one_ne_zero 2383 (6) x IN roots p ==> #1 * x = x 2384 Note x IN R by poly_roots_element 2385 so #1 * x = x by field_mult_lone 2386 (7) x IN roots p /\ x <> #0 ==> ?y. (y IN roots p /\ y <> #0) /\ (y * x = #1) 2387 Note x IN R by poly_roots_element 2388 and x IN R+ by field_nonzero_eq 2389 Let y = |/ x, 2390 Then |/ x IN roots p by poly_master_roots_inv_root 2391 and |/ x IN R+, or |/ x <> #0 by field_inv_nonzero 2392 so |/ x * x = #1 by field_mult_linv 2393 (8) x IN roots p /\ y IN roots p ==> x * y = y * x 2394 Note x IN R /\ y IN R by poly_roots_element 2395 so x * y = y * x by field_mult_comm 2396*) 2397val poly_master_roots_prod_abelian_group = store_thm( 2398 "poly_master_roots_prod_abelian_group", 2399 ``!r:'a field. FiniteField r ==> !n. let p = master ((char r) ** n) in 2400 AbelianGroup ((subset_field r (roots p)).prod excluding (subset_field r (roots p)).sum.id)``, 2401 rpt (stripDup[FiniteField_def]) >> 2402 qabbrev_tac `m = (char r) ** n` >> 2403 rw_tac std_ss[] >> 2404 qabbrev_tac `s = roots p DELETE #0` >> 2405 `!x. x IN s <=> x IN roots p /\ x <> #0` by rw[Abbr`s`] >> 2406 rw_tac std_ss[AbelianGroup_def, group_def_alt, excluding_def, GSYM DELETE_DEF, subset_field_property] >- 2407 metis_tac[poly_master_roots_mult_root] >- 2408 metis_tac[field_mult_eq_zero, poly_roots_element] >- 2409 metis_tac[field_mult_assoc, poly_roots_element] >- 2410 metis_tac[poly_master_root_one, poly_roots_member, field_one_element, field_is_ring] >- 2411 rw[] >- 2412 metis_tac[field_mult_lone, poly_roots_element] >- 2413 metis_tac[poly_master_roots_inv_root, poly_roots_element, field_inv_nonzero, field_mult_linv, field_nonzero_eq] >> 2414 metis_tac[field_mult_comm, poly_roots_element]); 2415 2416(* Theorem: FiniteField r ==> !n. Field (subset_field r (roots (master ((char r) ** n)))) *) 2417(* Proof: 2418 Let m = (char r) ** n, p = master m. 2419 By field_def_alt, this is to show: 2420 (1) AbelianGroup (subset_field r (roots p)).sum 2421 This is true by poly_master_roots_sum_abelian_group 2422 (2) AbelianGroup ((subset_field r (roots p)).prod excluding (subset_field r (roots p)).sum.id) 2423 This is true by poly_master_roots_prod_abelian_group 2424 (3) (subset_field r (roots p)).sum.carrier = (subset_field r (roots p)).carrier 2425 This is true by subset_field_property 2426 (4) (subset_field r (roots p)).prod.carrier = (subset_field r (roots p)).carrier 2427 This is true by subset_field_property 2428 (5) x IN roots p ==> #0 * x = #0 by subset_field_property 2429 This is true by field_mult_lzero, poly_roots_element 2430 (6) x IN roots p /\ y IN roots p /\ z IN roots p ==> x * (y + z) = x * y + x * z by subset_field_property 2431 This is true by field_mult_radd, poly_roots_element 2432*) 2433val poly_master_roots_field = store_thm( 2434 "poly_master_roots_field", 2435 ``!r:'a field. FiniteField r ==> !n. Field (subset_field r (roots (master ((char r) ** n))))``, 2436 rpt (stripDup[FiniteField_def]) >> 2437 qabbrev_tac `m = (char r) ** n` >> 2438 qabbrev_tac `p = master m` >> 2439 rw_tac std_ss[field_def_alt] >- 2440 rw[poly_master_roots_sum_abelian_group, Abbr`p`, Abbr`m`] >- 2441 metis_tac[poly_master_roots_prod_abelian_group] >- 2442 rw_tac std_ss[subset_field_property] >- 2443 rw_tac std_ss[subset_field_property] >- 2444 (fs[subset_field_property] >> 2445 metis_tac[field_mult_lzero, poly_roots_element]) >> 2446 fs[subset_field_property] >> 2447 metis_tac[field_mult_radd, poly_roots_element]); 2448 2449(* Theorem: FiniteField r ==> !n. FiniteField (subset_field r (roots (master (char r ** n)))) *) 2450(* Proof: 2451 Let s = subset_field r (roots (master (char r ** n))). 2452 Then Field s by poly_master_roots_field 2453 and FINITE B by poly_master_roots_finite_alt, subset_field_property 2454 ==> FiniteField s by FiniteField_def 2455*) 2456val poly_master_roots_finite_field = store_thm( 2457 "poly_master_roots_finite_field", 2458 ``!r:'a field. FiniteField r ==> !n. FiniteField (subset_field r (roots (master (char r ** n))))``, 2459 rw_tac std_ss[poly_master_roots_finite_alt, poly_master_roots_field, subset_field_property, FiniteField_def]); 2460 2461(* Theorem: FiniteField r ==> !n. subset_field r (roots (master ((char r) ** n))) <<= r *) 2462(* Proof: 2463 Let m = (char r) ** n, p = master m. 2464 This is to show: 2465 (1) Field (subset_field r (roots p)), true by poly_master_roots_field 2466 (2) subfield (subset_field r (roots p)) r 2467 By subfield_def, FieldHomo_def, RingHomo_def, subset_field_property, this is to show: 2468 (1) x IN roots p ==> x IN R, true by poly_roots_element 2469 (2) GroupHomo I (subset_field r (roots p)).sum r.sum 2470 By GroupHomo_def, subset_field_property, field_carriers, this is to show: 2471 (1) x IN roots p ==> x IN R, true by poly_roots_element 2472 (3) MonoidHomo I (subset_field r (roots p)).prod r.prod 2473 By MonoidHomo_def, subset_field_property, field_carriers, this is to show: 2474 (1) x IN roots p ==> x IN R, true by poly_roots_element 2475*) 2476val poly_master_roots_subfield = store_thm( 2477 "poly_master_roots_subfield", 2478 ``!r:'a field. FiniteField r ==> !n. subset_field r (roots (master ((char r) ** n))) <<= r``, 2479 strip_tac >> 2480 stripDup[FiniteField_def] >> 2481 strip_tac >> 2482 qabbrev_tac `m = (char r) ** n` >> 2483 qabbrev_tac `p = master m` >> 2484 rw_tac std_ss[] >- 2485 rw[poly_master_roots_field, Abbr`p`, Abbr`m`] >> 2486 rw_tac std_ss[subfield_def, FieldHomo_def, RingHomo_def, subset_field_property] >- 2487 metis_tac[poly_roots_element] >- 2488 (rw_tac std_ss[GroupHomo_def, subset_field_property, field_carriers] >> 2489 metis_tac[poly_roots_element]) >> 2490 rw_tac std_ss[MonoidHomo_def, subset_field_property, field_carriers] >> 2491 metis_tac[poly_roots_element]); 2492 2493(* Theorem: FiniteField r ==> (FieldIso I (subset_field r (roots (master (char r ** (fdim r))))) r) *) 2494(* Proof: 2495 Let sm = subset_field r (roots (master (char r ** (fdim r)))). 2496 By subfield_carrier_antisym, this is to show: 2497 (1) R SUBSET sm.carrier 2498 By subset_field_property, SUBSET_DEF, this is to show: 2499 !x. x IN R ==> x IN roots (master (char r ** fdim r)) 2500 Note R = roots (master (CARD R)) by poly_master_roots_all 2501 and CARD R = char r ** fdim r by finite_field_card_eqn 2502 The assertion is true. 2503 (2) subfield sm r by poly_master_roots_subfield 2504*) 2505val poly_master_roots_subfield_iso_field = store_thm( 2506 "poly_master_roots_subfield_iso_field", 2507 ``!r:'a field. FiniteField r ==> (FieldIso I (subset_field r (roots (master (char r ** (fdim r))))) r)``, 2508 rpt strip_tac >> 2509 qabbrev_tac `sm = subset_field r (roots (master (char r ** (fdim r))))` >> 2510 (irule subfield_carrier_antisym >> rpt conj_tac) >| [ 2511 rw_tac std_ss[subset_field_property, SUBSET_DEF, Abbr`sm`] >> 2512 `R = roots (master (CARD R))` by rw[poly_master_roots_all] >> 2513 `CARD R = char r ** fdim r` by rw[finite_field_card_eqn] >> 2514 metis_tac[], 2515 rw[poly_master_roots_subfield, Abbr`sm`] 2516 ]); 2517 2518(* Theorem: FiniteField r ==> (FieldIso I (subset_field r (roots (master (char r ** (fdim r))))) r) *) 2519(* Proof: 2520 Let s = subset_field r (roots (master (char r ** (fdim r)))). 2521 Then FiniteField s by poly_master_roots_finite_field 2522 and FieldIso I s r by poly_master_roots_subfield_iso_field 2523 ==> FieldIso I r s by field_iso_I_iso, finite_field_is_field 2524 Thus r =ff= d by notation 2525*) 2526val poly_master_roots_subfield_isomorphism = store_thm( 2527 "poly_master_roots_subfield_isomorphism", 2528 ``!r:'a field. FiniteField r ==> (r =ff= (subset_field r (roots (master (char r ** (fdim r))))))``, 2529 metis_tac[poly_master_roots_subfield_iso_field, poly_master_roots_finite_field, field_iso_sym, finite_field_is_field]); 2530 2531(* ------------------------------------------------------------------------- *) 2532(* Useful Results (for paper or proof investigation) *) 2533(* ------------------------------------------------------------------------- *) 2534 2535(* The following is not that good: 2536 It only depends on FiniteField s, and monic_irreducibles_bounded_prod_set |> ISPEC ``s:'a field`` 2537*) 2538 2539(* Theorem: FiniteField r /\ s <<= r /\ 0 < n ==> (master (CARD B ** n) = 2540 poly_prod_image s (poly_prod_set s) (IMAGE (monic_irreducibles_degree s) (divisors n))) *) 2541(* Proof: 2542 Note FiniteField s by subfield_finite_field 2543 master (CARD B ** n) 2544 = poly_prod_set s (monic_irreducibles_bounded s n) by poly_master_subfield_factors_alt 2545 = poly_prod_image s (poly_prod_set s) 2546 (IMAGE (monic_irreducibles_degree s) (divisors n)) 2547 by monic_irreducibles_bounded_prod_set 2548*) 2549val poly_master_subfield_eq_monic_irreducibles_prod_image = store_thm( 2550 "poly_master_subfield_eq_monic_irreducibles_prod_image", 2551 ``!(r s):'a field n. FiniteField r /\ s <<= r /\ 0 < n ==> (master (CARD B ** n) = 2552 poly_prod_image s (poly_prod_set s) (IMAGE (monic_irreducibles_degree s) (divisors n)))``, 2553 rpt (stripDup[FiniteField_def]) >> 2554 `FiniteField s` by metis_tac[subfield_finite_field] >> 2555 metis_tac[monic_irreducibles_bounded_prod_set, poly_master_subfield_factors_alt]); 2556 2557(* Theorem: FiniteField r /\ s <<= r /\ 0 < n ==> 2558 (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d IN divisors n}) *) 2559(* Proof: by poly_master_subfield_eq_monic_irreducibles_prod_image *) 2560val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_1 = store_thm( 2561 "poly_master_subfield_eq_monic_irreducibles_prod_image_alt_1", 2562 ``!(r s):'a field n. FiniteField r /\ s <<= r /\ 0 < n ==> 2563 (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d IN divisors n})``, 2564 rw[poly_master_subfield_eq_monic_irreducibles_prod_image] >> 2565 `IMAGE (poly_prod_set s) (IMAGE (monic_irreducibles_degree s) (divisors n)) = {poly_prod_set s (monic_irreducibles_degree s d) | d IN (divisors n)}` suffices_by rw[] >> 2566 rw[EXTENSION, EQ_IMP_THM] >| [ 2567 qexists_tac `x''` >> 2568 `x' = monic_irreducibles_degree s x''` suffices_by rw[] >> 2569 rw[EXTENSION] >> 2570 metis_tac[], 2571 metis_tac[] 2572 ]); 2573 2574(* Theorem: FiniteField r /\ s <<= r /\ 0 < n ==> 2575 (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d divides n}) *) 2576(* Proof: by poly_master_subfield_eq_monic_irreducibles_prod_image *) 2577(* Theorem: FiniteField r /\ 0 < n ==> 2578 (master (CARD R ** n) = PPROD {PPROD (monic_irreducibles_degree r d) | d | d divides n}) *) 2579(* Proof: by poly_master_eq_monic_irreducibles_prod_image *) 2580val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2 = store_thm( 2581 "poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2", 2582 ``!(r s):'a field n. FiniteField r /\ s <<= r /\ 0 < n ==> 2583 (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d divides n})``, 2584 rw[poly_master_subfield_eq_monic_irreducibles_prod_image] >> 2585 `IMAGE (poly_prod_set s) (IMAGE (monic_irreducibles_degree s) (divisors n)) = {poly_prod_set s (monic_irreducibles_degree s d) | d | d divides n}` suffices_by rw[] >> 2586 rw[EXTENSION, EQ_IMP_THM] >| [ 2587 qexists_tac `x''` >> 2588 `x' = monic_irreducibles_degree s x''` suffices_by fs[divisors_def] >> 2589 rw[EXTENSION] >> 2590 metis_tac[], 2591 metis_tac[DIVIDES_LE, divisors_element] 2592 ]); 2593 2594(* Next is better than above. *) 2595 2596(* Theorem: FiniteField r ==> !n. 0 < n ==> 2597 (master (CARD R ** n) = PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n))) *) 2598(* Proof: 2599 master (CARD R ** n) 2600 = PPROD (monic_irreducibles_bounded r n) by poly_master_monic_irreducible_factors 2601 = PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) 2602 by monic_irreducibles_bounded_prod_set 2603*) 2604val poly_master_eq_monic_irreducibles_prod_image = store_thm( 2605 "poly_master_eq_monic_irreducibles_prod_image", 2606 ``!r:'a field. FiniteField r ==> !n. 0 < n ==> 2607 (master (CARD R ** n) = PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)))``, 2608 rw[poly_master_monic_irreducible_factors, monic_irreducibles_bounded_prod_set]); 2609 2610(* Theorem: FiniteField r /\ 0 < n ==> (master (CARD R ** n) = PPROD {Psi d | d IN (divisors n)}) *) 2611(* Proof: by poly_master_eq_monic_irreducibles_prod_image *) 2612val poly_master_eq_monic_irreducibles_prod_image_alt_1 = store_thm( 2613 "poly_master_eq_monic_irreducibles_prod_image_alt_1", 2614 ``!(r:'a field) n. FiniteField r /\ 0 < n ==> 2615 (master (CARD R ** n) = PPROD {Psi d | d IN (divisors n)})``, 2616 rw[poly_master_eq_monic_irreducibles_prod_image] >> 2617 `IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) = {PPROD (monic_irreducibles_degree r d) | d IN (divisors n)}` suffices_by rw[] >> 2618 rw[EXTENSION, EQ_IMP_THM] >| [ 2619 qexists_tac `x''` >> 2620 `x' = monic_irreducibles_degree r x''` suffices_by rw[] >> 2621 rw[EXTENSION] >> 2622 metis_tac[], 2623 metis_tac[] 2624 ]); 2625 2626(* Theorem: FiniteField r /\ 0 < n ==> (master (CARD R ** n) = PPROD {Psi d | d divides n}) *) 2627(* Proof: by poly_master_eq_monic_irreducibles_prod_image *) 2628val poly_master_eq_monic_irreducibles_prod_image_alt_2 = store_thm( 2629 "poly_master_eq_monic_irreducibles_prod_image_alt_2", 2630 ``!(r:'a field) n. FiniteField r /\ 0 < n ==> (master (CARD R ** n) = PPROD {Psi d | d divides n})``, 2631 rw[poly_master_eq_monic_irreducibles_prod_image] >> 2632 `IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)) = {PPROD (monic_irreducibles_degree r d) | d divides n}` suffices_by rw[] >> 2633 rw[EXTENSION, EQ_IMP_THM] >| [ 2634 qexists_tac `x''` >> 2635 `x' = monic_irreducibles_degree r x''` suffices_by fs[divisors_def] >> 2636 rw[EXTENSION] >> 2637 metis_tac[], 2638 metis_tac[DIVIDES_LE, divisors_element] 2639 ]); 2640 2641(* ------------------------------------------------------------------------- *) 2642(* Monic Irreducible Products *) 2643(* ------------------------------------------------------------------------- *) 2644 2645(* Theorem: FiniteRing r ==> !n. mset (IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))) *) 2646(* Proof: 2647 Let f = monic_irreducibles_degree r, s = IMAGE PPROD (IMAGE f (natural n)). 2648 To show (mset s) is to show: !p. p IN s ==> monic p 2649 Note ?k. p = PPROD (f k) by IN_IMAGE 2650 Note FINITE (f k) by monic_irreducibles_degree_finite, FINITE R 2651 and mset (f k) by monic_irreducibles_degree_member 2652 ==> monic (PPROD (f k)) by poly_monic_prod_set_monic 2653 or monic p by p = PPROD (f k) 2654*) 2655val monic_irreducibles_degree_prod_set_image_monic_set = store_thm( 2656 "monic_irreducibles_degree_prod_set_image_monic_set", 2657 ``!r:'a ring. FiniteRing r ==> !n. mset (IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)))``, 2658 rpt (stripDup[FiniteRing_def]) >> 2659 qabbrev_tac `s = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))` >> 2660 `?k. p = PPROD (monic_irreducibles_degree r k)` by prove_tac[IN_IMAGE] >> 2661 `FINITE (monic_irreducibles_degree r k)` by rw[monic_irreducibles_degree_finite] >> 2662 `mset (monic_irreducibles_degree r k)` by metis_tac[monic_irreducibles_degree_member] >> 2663 rw[poly_monic_prod_set_monic]); 2664 2665(* Theorem: FiniteRing r ==> !n. monic (PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))) *) 2666(* Proof: 2667 Let f = monic_irreducibles_degree r, s = IMAGE PPROD (IMAGE f (natural n)). 2668 Note FINITE (natural n) by natural_finite 2669 ==> FINITE (IMAGE f (natural n)) by IMAGE_FINITE 2670 ==> FINITE s by IMAGE_FINITE 2671 Note mset s by monic_irreducibles_degree_prod_set_image_monic_set 2672 Hence monic (PPROD s) by poly_monic_prod_set_monic, mset s 2673*) 2674val monic_irreducibles_degree_prod_set_image_monic = store_thm( 2675 "monic_irreducibles_degree_prod_set_image_monic", 2676 ``!r:'a ring. FiniteRing r ==> !n. monic (PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)))``, 2677 rpt (stripDup[FiniteRing_def]) >> 2678 qabbrev_tac `s = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))` >> 2679 `FINITE s` by rw[natural_finite, Abbr`s`] >> 2680 `mset s` by metis_tac[monic_irreducibles_degree_prod_set_image_monic_set] >> 2681 rw[poly_monic_prod_set_monic]); 2682 2683(* Theorem: FiniteRing r ==> !n. poly (PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))) *) 2684(* Proof: monic_irreducibles_degree_prod_set_image_monic, poly_monic_poly *) 2685val monic_irreducibles_degree_prod_set_image_poly = store_thm( 2686 "monic_irreducibles_degree_prod_set_image_poly", 2687 ``!r:'a ring. FiniteRing r ==> !n. poly (PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)))``, 2688 rw_tac std_ss[monic_irreducibles_degree_prod_set_image_monic, poly_monic_poly]); 2689 2690(* Theorem: FiniteRing r /\ #1 <> #0 ==> 2691 !n. PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)) <> |0| *) 2692(* Proof: by monic_irreducibles_degree_prod_set_image_monic, poly_monic_nonzero *) 2693val monic_irreducibles_degree_prod_set_image_nonzero = store_thm( 2694 "monic_irreducibles_degree_prod_set_image_nonzero", 2695 ``!r:'a ring. FiniteRing r /\ #1 <> #0 ==> 2696 !n. PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)) <> |0|``, 2697 rw_tac std_ss[monic_irreducibles_degree_prod_set_image_monic, poly_monic_nonzero]); 2698 2699(* ------------------------------------------------------------------------- *) 2700(* Existence of Monic Irreducible by Master Polynomial *) 2701(* ------------------------------------------------------------------------- *) 2702 2703(* 2704The Picture: Let s <<= r, both FiniteField s /\ FiniteField r. 2705 CARD R = (CARD B) ** d, where d = r <:> s. 2706 2707Note that master (CARD R) = product of all monic irreducibles of degree k, k <= d, k divides d. 2708e.g. if d = 6, 2709 master (CARD R) = irreducibles of deg 1 * 2710 irreducibles of deg 2 * 2711 irreducibles of deg 3 * 2712 irreducibles of deg 6 2713 2714There are IPoly s p with deg 4, deg 5, deg 7, etc. but they are not included in master (CARD R). 2715However, by including all degrees from 1 to 6, 2716 master (CARD R) pdivides PPROD (irreducibles of deg k) (1 to 6) 2717 2718Now, if {irreducibles of deg 6} = {}, then 2719 PPROD (irreducibles of deg k) (1 to 6) = PPROD (irreducibles of deg k) (1 to 5) = q 2720Note that 2721 PPROD (ipoly of deg 1) pdivides master (CARD B ** 1) since it is PPROD ipoly deg (divisors of 1) 2722 PPROD (ipoly of deg 2) pdivides master (CARD B ** 2) since it is PPROD ipoly deg (divisors of 2) 2723 PPROD (ipoly of deg 3) pdivides master (CARD B ** 3) since it is PPROD ipoly deg (divisors of 3) 2724 .... 2725so PPROD (irreducibles of deg k) (1 to 5) pdivides PPROD (master (CARD B ** k)) (1 to 5) = t. 2726 2727Thus master (CARD R) = master (CARD B ** d) pdivides q, and q pdivides t. 2728==> CARD B ** d <= deg t, 2729However, 2730 deg t = sum of master degree 2731 = (CARD B) ** 1 + (CARD B) ** 2 + (CARD B) ** 3 + (CARD B) ** 4 + (CARD B) ** 5 2732 = ((CARD B) ** 6 - 1) / 5 2733 = ((CARD B) ** d - 1) / 5 d = 6 2734 < (CARD B) ** d, which is impossible. 2735 2736Another way to argue: 2737Let m = maximum degree of (subfield) irreducible in (big) field (CARD B) ** n, 2738 PPROD (ipoly of deg 1) pdivides master (CARD B ** 1) 2739 PPROD (ipoly of deg 2) pdivides master (CARD B ** 2) 2740... 2741 PPROD (ipoly of deg m) pdivides master (CARD B ** m) 2742and no more for higher degree, since m is assumed maximum. 2743Hence, 2744 PPROD (PPROD (ipoly of degree k)) (1 to m) pdivides PPROD (master (CARD B ** k)) (1 to m) 2745LHS is the product of all irreducibles, and PPROD (all irreducibles, each once) = master (CARD B ** n). 2746Thus master (CARD B ** n) pdivides PPROD (master (CARD B ** k)) (1 to m) 2747degree of LHS = a = CARD B ** n. 2748degree of RHS = b = CARD B ** 1 + CARD B ** 2 + ... + CARD B ** m 2749 = [(CARD B) ** (m + 1) - 1] / [CARD B - 1] 2750 < (CARD B) ** (m + 1) - 1 since 1 < CARD B. 2751For pdivides to hold, a <= b. 2752If m < n, then m + 1 <= n, b < CARD B ** n - 1 2753so a <= b implies CARD B ** n < CARD B ** n - 1, which is impossible. 2754Thus m = n, or there is an irreducible in the subfield of degree n. 2755 2756*) 2757 2758(* Theorem: FiniteField r ==> !n. Psi n pdivides (master (CARD R ** n)) *) 2759(* Proof: 2760 Let s = monic_irreducibles_degree r n, q = master (CARD R ** n). 2761 The goal is: PPROD s pdivides q. 2762 Note FINITE s by monic_irreducibles_degree_finite 2763 and pcoprime_set s by monic_irreducibles_degree_coprime_set 2764 and poly q by poly_master_poly 2765 Also !p. p IN s 2766 ==> monic p /\ ipoly p /\ (deg p = n) by monic_irreducibles_degree_member 2767 ==> p pdivides q by poly_irreducible_divides_master 2768 Thus PPROD s pdivides q by poly_prod_coprime_set_divides 2769*) 2770val monic_irreducibles_degree_prod_set_divides_master = store_thm( 2771 "monic_irreducibles_degree_prod_set_divides_master", 2772 ``!r:'a field. FiniteField r ==> 2773 !n. Psi n pdivides (master (CARD R ** n))``, 2774 rpt (stripDup[FiniteField_def]) >> 2775 qabbrev_tac `s = monic_irreducibles_degree r n` >> 2776 qabbrev_tac `q = master (CARD R ** n)` >> 2777 `FINITE s` by rw[monic_irreducibles_degree_finite, Abbr`s`] >> 2778 `pcoprime_set s` by rw[monic_irreducibles_degree_coprime_set, Abbr`s`] >> 2779 `poly q` by rw[Abbr`q`] >> 2780 `!p. p IN s ==> p pdivides q` by metis_tac[monic_irreducibles_degree_member, poly_irreducible_divides_master] >> 2781 rw[poly_prod_coprime_set_divides]); 2782 2783(* Theorem: FiniteField r ==> !n. 0 < n ==> 2784 master (CARD R ** n) pdivides PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)) *) 2785(* Proof: 2786 Let s = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n)), 2787 t = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n)). 2788 By poly_master_eq_monic_irreducibles_prod_image, this is to show: PPROD s pdivides PPROD t 2789 2790 Note FINITE (natural n) by natural_finite 2791 ==> FINITE t by IMAGE_FINITE 2792 Note (divisors n) SUBSET (natural n) by divisors_subset_natural, 0 < n 2793 ==> s SUBSET t by IMAGE_SUBSET 2794 Claim: pset t 2795 Proof: This is to show: poly (PPROD (monic_irreducibles_degree r (SUC x''))) 2796 Let u = monic_irreducibles_degree r (SUC x''). 2797 Note FINITE u by monic_irreducibles_degree_finite 2798 and pset u by monic_irreducibles_degree_poly_set 2799 ==> poly (PPROD u) by poly_prod_set_poly 2800 2801 Thus PPROD s pdivides PPROD t by poly_prod_set_divides_prod_set, Claim 2802*) 2803val poly_master_divides_monic_irreducibles_degree_prod_set_image = store_thm( 2804 "poly_master_divides_monic_irreducibles_degree_prod_set_image", 2805 ``!r:'a field. FiniteField r ==> !n. 0 < n ==> 2806 master (CARD R ** n) pdivides PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))``, 2807 rpt (stripDup[FiniteField_def]) >> 2808 rw[poly_master_eq_monic_irreducibles_prod_image] >> 2809 qabbrev_tac `s = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (divisors n))` >> 2810 qabbrev_tac `t = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) (natural n))` >> 2811 `FINITE (natural n)` by rw[natural_finite] >> 2812 `FINITE t` by rw[Abbr`t`] >> 2813 `(divisors n) SUBSET (natural n)` by rw[divisors_subset_natural] >> 2814 `s SUBSET t` by rw[Abbr`s`, Abbr`t`] >> 2815 `pset t` by 2816 (rw[Abbr`t`] >> 2817 `FINITE (monic_irreducibles_degree r (SUC x''))` by rw[monic_irreducibles_degree_finite] >> 2818 `pset (monic_irreducibles_degree r (SUC x''))` by metis_tac[monic_irreducibles_degree_poly_set] >> 2819 rw[poly_prod_set_poly]) >> 2820 rw[poly_prod_set_divides_prod_set]); 2821 2822(* Theorem: FiniteField r ==> !s. FINITE s ==> 2823 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) s) pdivides 2824 PPIMAGE (\n. master (CARD R ** n)) s *) 2825(* Proof: 2826 Let f = \n. master (CARD R ** n), t = PPIMAGE f s. 2827 u = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) s) 2828 The goal is to show: PPROD u pdivides t 2829 2830 Step 1: properties of f and t 2831 Note FINITE (IMAGE f s) by IMAGE_FINITE 2832 and pset (IMAGE f s) by IN_IMAGE, poly_master_poly 2833 ==> poly t by poly_prod_set_poly 2834 2835 Step 2: properties of u 2836 Note FINITE u by IMAGE_FINITE 2837 and !n. FINITE (monic_irreducibles_degree r n) by monic_irreducibles_degree_finite 2838 and !n. pset (monic_irreducibles_degree r n) by monic_irreducibles_degree_poly_set 2839 ==> pset u by IN_IMAGE, poly_prod_set_poly 2840 Claim: pcoprime_set u 2841 Proof: By poly_coprime_set_def, this is to show: 2842 p IN u /\ q IN u /\ p <> q ==> pcomprime p q 2843 Note ?n. n IN s /\ (p = Psi n) by IN_IMAGE 2844 and ?m. m IN s /\ (q = Psi m) by IN_IMAGE 2845 Note miset (monic_irreducibles_degree r n) by monic_irreducibles_degree_member 2846 and miset (monic_irreducibles_degree r m) by monic_irreducibles_degree_member 2847 Now m <> n by p <> q 2848 Thus DISJOINT (monic_irreducibles_degree r n) 2849 (monic_irreducibles_degree r m) by monic_irreducibles_degree_disjoint 2850 ==> pcomprime p q by poly_prod_monic_irreducible_set_coprime 2851 2852 Step 3: assert p IN u ==> p pdivides t 2853 Claim: !p. p IN u ==> p pdivides t 2854 Proof: Note ?n. n IN s /\ (p = Psi n) by IN_IMAGE 2855 and master (CARD R ** n) IN (IMAGE f s) by IN_IMAGE 2856 ==> master (CARD R ** n) pdivides t by poly_prod_set_element_divides 2857 But p pdivides (master (CARD R ** n)) by monic_irreducibles_degree_prod_set_divides_master 2858 ==> p pdivides t by poly_divides_transitive 2859 2860 Therefore PPROD u pdivides t by poly_prod_coprime_set_divides, claims. 2861*) 2862val monic_irreducibles_degree_prod_set_image_divides_master_image = store_thm( 2863 "monic_irreducibles_degree_prod_set_image_divides_master_image", 2864 ``!r:'a field. FiniteField r ==> !s. FINITE s ==> 2865 PPIMAGE PPROD (IMAGE (monic_irreducibles_degree r) s) pdivides PPIMAGE (\n. master (CARD R ** n)) s``, 2866 rpt (stripDup[FiniteField_def]) >> 2867 `Ring r` by rw[] >> 2868 qabbrev_tac `f = \n. master (CARD R ** n)` >> 2869 qabbrev_tac `t = PPIMAGE f s` >> 2870 qabbrev_tac `u = IMAGE PPROD (IMAGE (monic_irreducibles_degree r) s)` >> 2871 `!n. f n = master (CARD R ** n)` by rw[Abbr`f`] >> 2872 `FINITE (IMAGE f s)` by rw[] >> 2873 `pset (IMAGE f s)` by metis_tac[IN_IMAGE, poly_master_poly] >> 2874 `poly t` by metis_tac[poly_prod_set_poly] >> 2875 `FINITE u` by rw[Abbr`u`] >> 2876 `!n. FINITE (monic_irreducibles_degree r n)` by rw[monic_irreducibles_degree_finite] >> 2877 `!n. pset (monic_irreducibles_degree r n)` by metis_tac[monic_irreducibles_degree_poly_set] >> 2878 `pset u` by 2879 (rw_tac std_ss[Abbr`u`] >> 2880 metis_tac[IN_IMAGE, poly_prod_set_poly]) >> 2881 `pcoprime_set u` by 2882 (rw_tac std_ss[poly_coprime_set_def, Abbr`u`] >> 2883 `?n. n IN s /\ (p = Psi n)` by metis_tac[IN_IMAGE] >> 2884 `?m. m IN s /\ (q = Psi m)` by metis_tac[IN_IMAGE] >> 2885 `miset (monic_irreducibles_degree r n)` by rw[monic_irreducibles_degree_member] >> 2886 `miset (monic_irreducibles_degree r m)` by rw[monic_irreducibles_degree_member] >> 2887 `DISJOINT (monic_irreducibles_degree r n) (monic_irreducibles_degree r m)` by metis_tac[monic_irreducibles_degree_disjoint] >> 2888 rw[poly_prod_monic_irreducible_set_coprime]) >> 2889 `!p. p IN u ==> p pdivides t` by 2890 (rw_tac std_ss[Abbr`u`, Abbr`t`] >> 2891 `?n. n IN s /\ (p = Psi n)` by metis_tac[IN_IMAGE] >> 2892 `master (CARD R ** n) IN (IMAGE f s)` by metis_tac[IN_IMAGE] >> 2893 `p pdivides (master (CARD R ** n))` by rw[monic_irreducibles_degree_prod_set_divides_master] >> 2894 metis_tac[poly_prod_set_element_divides, poly_divides_transitive]) >> 2895 rw[poly_prod_coprime_set_divides]); 2896 2897(* Theorem: FiniteField r ==> !n. 0 < n ==> ?p. monic p /\ ipoly p /\ (deg p = n) *) 2898(* Proof: 2899 By contradiction, suppose !p. monic p /\ ipoly p ==> deg p <> n. 2900 Let b = CARD R. 2901 Then 1 < b by finite_field_card_gt_1 2902 Let m = n - 1, 2903 Then n = SUC m by ADD1 2904 2905 Let f = \k. master (b ** k), t = PPIMAGE f (natural m). 2906 Note 1 < b ** n by ONE_LT_EXP, 0 < n 2907 ==> monic (master (b ** n)) by poly_master_monic, 1 < b ** n 2908 so poly (master (b ** n)) by poly_monic_poly 2909 Note monic t by poly_master_prod_set_over_natural_monic 2910 so poly t /\ t <> |0| by poly_monic_poly, poly_monic_nonzero 2911 2912 Claim: master (b ** n) pdivides t 2913 Proof: Let g = monic_irreducibles_degree r, s = IMAGE PPROD (IMAGE g (natural m)). 2914 Then FINITE s by natural_finite, IMAGE_FINITE 2915 and mset s by monic_irreducibles_degree_prod_set_image_monic_set 2916 so pset s by monic_set_poly_set 2917 Note master (b ** n) pdivides PPIMAGE PPROD (IMAGE g (natural (SUC m))) ...(1) 2918 by poly_master_divides_monic_irreducibles_degree_prod_set_image, 0 < n 2919 Note that from contradiction hypothesis, 2920 g (SUC m) = {} by monic_irreducibles_degree_member, MEMBER_NOT_EMPTY 2921 PPIMAGE PPROD (IMAGE g (natural (SUC m))) 2922 = PPROD (IMAGE PPROD (IMAGE g (natural (SUC m)))) by notation 2923 = PPROD (PPROD (g (SUC m)) INSERT s) by natural_suc 2924 = PPROD (PPROD {}) INSERT s) by above 2925 = PPROD ( |1| INSERT s) by poly_prod_set_empty 2926 = PPROD s by poly_prod_set_with_one ...(2) 2927 2928 Note (PPROD s) pdivides t by monic_irreducibles_degree_prod_set_image_divides_master_image 2929 and poly (PPROD s) by monic_irreducibles_degree_prod_set_image_poly 2930 Thus master (b ** n) pdivides t by poly_divides_transitive, (1), (2), above. 2931 2932 2933 Next: compare degrees 2934 Note deg (master (b ** n)) = b ** n by poly_master_deg, 1 < b ** n 2935 and deg t = b * (b ** m - 1) DIV (b - 1) by poly_master_prod_set_over_natural_deg 2936 <= b * (b ** m - 1) by DIV_LESS_EQ 2937 = b * b ** m - b * 1 by LEFT_SUB_DISTRIB 2938 < b * b ** m by SUB_LESS 2939 = b ** n by EXP 2940 ==> deg t < b ** n by above ... (3) 2941 But 0 < b ** n by EXP_POS, 0 < b 2942 so pmonic (master (b ** n)) by poly_monic_pmonic, 0 < b ** n 2943 ==> b ** n <= deg t by poly_field_divides_deg_le, t <> |0| ... (4) 2944 This contradicts deg t < b ** n by (3), (4). 2945*) 2946val poly_monic_irreducible_exists_alt = store_thm( 2947 "poly_monic_irreducible_exists_alt", 2948 ``!r:'a field. FiniteField r ==> !n. 0 < n ==> ?p. monic p /\ ipoly p /\ (deg p = n)``, 2949 rpt (stripDup[FiniteField_def]) >> 2950 spose_not_then strip_assume_tac >> 2951 `Ring r /\ #1 <> #0` by rw[] >> 2952 `FiniteRing r` by metis_tac[FiniteRing_def] >> 2953 qabbrev_tac `b = CARD R` >> 2954 `1 < b` by rw[finite_field_card_gt_1, Abbr`b`] >> 2955 `n = SUC (n - 1)` by decide_tac >> 2956 qabbrev_tac `m = n - 1` >> 2957 qabbrev_tac `f = \k. master (b ** k)` >> 2958 qabbrev_tac `t = PPIMAGE f (natural m)` >> 2959 `!k. f k = master (b ** k)` by rw[Abbr`f`] >> 2960 `monic (master (b ** n))` by rw[poly_master_monic, ONE_LT_EXP] >> 2961 `poly (master (b ** n))` by rw[] >> 2962 `monic t` by rw[poly_master_prod_set_over_natural_monic, Abbr`t`, Abbr`f`, Abbr`b`] >> 2963 `poly t /\ t <> |0|` by metis_tac[poly_monic_poly, poly_monic_nonzero] >> 2964 `master (b ** n) pdivides t` by 2965 (qabbrev_tac `g = monic_irreducibles_degree r` >> 2966 qabbrev_tac `s = IMAGE PPROD (IMAGE g (natural m))` >> 2967 `master (b ** n) pdivides PPIMAGE PPROD (IMAGE g (natural (SUC m)))` by rw[poly_master_divides_monic_irreducibles_degree_prod_set_image, Abbr`b`, Abbr`g`] >> 2968 `PPIMAGE PPROD (IMAGE g (natural (SUC m))) = PPROD s` by 2969 (rw[natural_suc] >> 2970 `g (SUC m) = {}` by metis_tac[monic_irreducibles_degree_member, MEMBER_NOT_EMPTY] >> 2971 rw[poly_prod_set_empty] >> 2972 `FINITE s` by rw[natural_finite, Abbr`s`] >> 2973 `pset s` by metis_tac[monic_irreducibles_degree_prod_set_image_monic_set, monic_set_poly_set] >> 2974 rw[poly_prod_set_with_one]) >> 2975 `PPROD s pdivides t` by rw[monic_irreducibles_degree_prod_set_image_divides_master_image, Abbr`s`, Abbr`b`, Abbr`t`, Abbr`g`, Abbr`f`] >> 2976 `poly (PPROD s)` by rw[monic_irreducibles_degree_prod_set_image_poly, Abbr`s`, Abbr`g`] >> 2977 metis_tac[poly_divides_transitive]) >> 2978 `t = PPIMAGE (\k. master (b ** k)) (natural m)` by rw[Abbr`t`, Abbr`f`] >> 2979 `deg t = b * (b ** m - 1) DIV (b - 1)` by metis_tac[poly_master_prod_set_over_natural_deg] >> 2980 `deg t <= b * (b ** m - 1)` by rw[DIV_LESS_EQ] >> 2981 `b * (b ** m - 1) < b * b ** m` by rw[] >> 2982 `b * b ** m = b ** n` by metis_tac[EXP] >> 2983 `deg t < b ** n` by decide_tac >> 2984 `deg (master (b ** n)) = b ** n` by rw[poly_master_deg, ONE_LT_EXP] >> 2985 `pmonic (master (b ** n))` by rw[poly_monic_pmonic] >> 2986 `b ** n <= deg t` by metis_tac[poly_field_divides_deg_le] >> 2987 decide_tac); 2988 2989(* Another proof of the existence of irreducible of a given degree, Yes! *) 2990 2991(* poly_monic_irreducible_exists_alt: 2992 This proof is based on the fact that the master polynomial is the product of all monic irreducibles. 2993 Compare with the more advanced proof in ffExist: (poly_monic_irreducible_exists) 2994 That proof depends on counting the number of monic irreducibles. 2995 2996 Used in ffConjugate: poly_unity_mod_exp_char_equal, as that script cannot use ffExist. 2997*) 2998 2999(* ------------------------------------------------------------------------- *) 3000(* Finite Field Subgroup and Master Polynomial *) 3001(* ------------------------------------------------------------------------- *) 3002 3003(* Theorem: FiniteField r /\ g <= f* ==> (roots (master (CARD G + 1)) = G UNION {#0}) *) 3004(* Proof: 3005 Let n = CARD G + 1, then 0 < n by SUC_POS, ADD1 3006 Note FiniteGroup g by field_subgroup_finite_group 3007 so FINITE G by FiniteGroup_def 3008 3009 Claim: G UNION {#0} SUBSET roots (master n) 3010 Proof: By SUBSET_DEF, IN_UNION, IN_SING, this is to show: 3011 (1) x IN G ==> x IN roots (master n) 3012 Note x IN R by field_subgroup_element 3013 so x ** (CARD G) = #1 by finite_group_Fermat, field_subgroup_exp 3014 x ** n 3015 = x ** (SUC (CARD G)) by ADD1 3016 = x ** x ** (CARD G) by field_exp_SUC 3017 = x ** #1 by above 3018 = x by field_mult_rone 3019 Hence root (master n) x by poly_master_root 3020 or x IN roots (master n) by poly_roots_member 3021 (2) #0 IN roots (master n), true by poly_master_root_zero, 0 < n 3022 3023 Now 0 < CARD G by finite_group_card_pos 3024 so 1 < n, or n <> 1, or 1 < n by arithmetic 3025 Note poly (master n) by poly_master_poly 3026 and master n <> |0| by poly_master_eq_zero, n <> 1 3027 ==> FINITE (roots (master n)) by poly_roots_finite 3028 ==> CARD (roots (master n)) <= deg (master n) by poly_roots_count 3029 or CARD (roots (master n)) <= n by poly_master_deg, 1 < n 3030 3031 Note G UNION {#0} SUBSET roots (master n) by Claim 3032 so CARD (G UNION {#0}) <= CARD (roots (master n)) by CARD_SUBSET 3033 and CARD (G UNION {#0}) = n by field_subgroup_card 3034 Thus CARD (roots (master n)) = n by above 3035 or roots (master (CARD G + 1)) = G UNION {#0} by SUBSET_EQ_CARD 3036*) 3037val field_subgroup_master_roots = store_thm( 3038 "field_subgroup_master_roots", 3039 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> (roots (master (CARD G + 1)) = G UNION {#0})``, 3040 rpt (stripDup[FiniteField_def, Subgroup_def]) >> 3041 `FINITE G /\ FiniteGroup g` by metis_tac[FiniteGroup_def, field_subgroup_finite_group] >> 3042 `0 < CARD G` by rw[finite_group_card_pos] >> 3043 `0 < CARD G + 1 /\ 1 < CARD G + 1 /\ CARD G + 1 <> 1` by decide_tac >> 3044 qabbrev_tac `n = CARD G + 1` >> 3045 `G UNION {#0} SUBSET roots (master n)` by 3046 (rw_tac std_ss[SUBSET_DEF, IN_UNION, IN_SING] >| [ 3047 `x ** (CARD G) = #1` by metis_tac[finite_group_Fermat, field_subgroup_exp, field_subgroup_id] >> 3048 `x IN R` by metis_tac[field_subgroup_element] >> 3049 `x ** n = x ** (SUC (CARD G))` by rw_tac std_ss[ADD1, Abbr`n`] >> 3050 `_ = x` by rw[field_exp_SUC] >> 3051 rw[poly_master_root, poly_roots_member], 3052 rw[poly_master_root_zero, poly_roots_member] 3053 ]) >> 3054 `Ring r /\ #1 <> #0` by rw[] >> 3055 `poly (master n) /\ master n <> |0|` by rw[poly_master_eq_zero] >> 3056 `FINITE (roots (master n))` by rw[poly_roots_finite] >> 3057 `CARD (roots (master n)) <= n ` by metis_tac[poly_roots_count, poly_master_deg] >> 3058 `CARD (G UNION {#0}) = n` by rw[field_subgroup_card, Abbr`n`] >> 3059 `CARD (G UNION {#0}) <= CARD (roots (master n))` by rw[CARD_SUBSET] >> 3060 `CARD (roots (master n)) = n` by decide_tac >> 3061 rw[SUBSET_EQ_CARD]); 3062 3063(* This is the key theorem to show that g <= f* eventually guarantees additive closure. *) 3064 3065(* ------------------------------------------------------------------------- *) 3066(* Finite Field Subgroup Field *) 3067(* ------------------------------------------------------------------------- *) 3068 3069(* Note: 3070 A subset_field, defined in fieldMap for sub-structures, 3071 takes a subset s of field elements to form a field. 3072 However, it is hard to ensure closure for addition and multiplication. 3073 3074 Here we study subgroup_field: take g <= f* to form a field. 3075 This guarantees closure of multiplication. 3076 The closure of addition depends on the roots of the Master polynomial. 3077 see: subgroup_field_element_iff_master_root. 3078*) 3079 3080(* Define the subgroup field: takes a multiplicative group and gives a field candidate *) 3081val subgroup_field_def = Define` 3082 subgroup_field (r:'a field) (g:'a group) = 3083 <| carrier := G UNION {#0}; 3084 sum := <| carrier := G UNION {#0}; op := r.sum.op; id := #0 |>; 3085 prod := g including #0 3086 |> 3087`; 3088 3089(* Theorem: properties of subgroup_field *) 3090(* Proof: by subgroup_field_def, including_def *) 3091val subgroup_field_property = store_thm( 3092 "subgroup_field_property", 3093 ``!(r:'a field) (g:'a group). 3094 ((subgroup_field r g).carrier = G UNION {#0}) /\ 3095 ((subgroup_field r g).sum.carrier = G UNION {#0}) /\ 3096 ((subgroup_field r g).prod.carrier = G UNION {#0}) /\ 3097 ((subgroup_field r g).sum.op = r.sum.op) /\ 3098 ((subgroup_field r g).sum.id = #0)``, 3099 rw_tac std_ss[subgroup_field_def, including_def]); 3100 3101(* Theorem: ((subgroup_field r g).sum.op = r.sum.op) /\ ((subgroup_field r g).sum.id = #0) *) 3102(* Proof: by subgroup_field_property *) 3103val subgroup_field_sum_property = store_thm( 3104 "subgroup_field_sum_property", 3105 ``!(r:'a field) (g:'a group). ((subgroup_field r g).sum.op = r.sum.op) /\ ((subgroup_field r g).sum.id = #0)``, 3106 rw[subgroup_field_property]); 3107 3108(* Theorem: Field r /\ g <= f* ==> 3109 ((subgroup_field r g).prod.op = r.prod.op) /\ ((subgroup_field r g).prod.id = #1) *) 3110(* Proof: 3111 This is to show: 3112 (1) (subgroup_field r g).prod.op = r.prod.op 3113 (subgroup_field r g).prod.op 3114 = (g including #0).op by subgroup_field_def 3115 = g.op by including_def 3116 = f*.op by Subgroup_def, g <= f* 3117 = r.prod.op by field_nonzero_mult_property 3118 (2) (subgroup_field r g).prod.id = #1 3119 (subgroup_field r g).prod.id 3120 = (g including #0).id by subgroup_field_def 3121 = g.id by including_def 3122 = f*.id by subgroup_id 3123 = #1 by field_nonzero_mult_property 3124*) 3125val subgroup_field_prod_property = store_thm( 3126 "subgroup_field_prod_property", 3127 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> 3128 ((subgroup_field r g).prod.op = r.prod.op) /\ ((subgroup_field r g).prod.id = #1)``, 3129 ntac 3 strip_tac >> 3130 `g.op = r.prod.op` by fs[Subgroup_def] >> 3131 `g.id = #1` by metis_tac[subgroup_id, field_nonzero_mult_property] >> 3132 rw_tac std_ss[subgroup_field_def, including_def]); 3133 3134(* Theorem: Field r /\ g <= f* ==> 3135 ((subgroup_field r g).sum.id = #0) /\ ((subgroup_field r g).prod.id = #1) *) 3136(* Proof: by subgroup_field_sum_property, subgroup_field_prod_property *) 3137val subgroup_field_ids = store_thm( 3138 "subgroup_field_ids", 3139 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> 3140 ((subgroup_field r g).sum.id = #0) /\ ((subgroup_field r g).prod.id = #1)``, 3141 rw_tac std_ss[subgroup_field_sum_property, subgroup_field_prod_property]); 3142 3143(* Theorem: FiniteGroup g /\ #0 NOTIN G ==> (CARD (subgroup_field r g).carrier = CARD G + 1) *) 3144(* Proof: 3145 Note FINITE G by FiniteGroup_def 3146 and (subgroup_field r g).carrier = G UNION {#0} by subgroup_field_property 3147 but G INTER {#0} = {} by IN_INTER, IN_SING, MEMBER_NOT_EMPTY 3148 CARD (subgroup_field r g).carrier 3149 = CARD (G UNION {#0}) 3150 = CARD G + CARD {#0} - CARD (G INTER {#0}) by CARD_UNION_EQN, FINITE_SING 3151 = CARD G + 1 - 0 = CARD G + 1 by CARD_SING 3152*) 3153val subgroup_field_card = store_thm( 3154 "subgroup_field_card", 3155 ``!(r:'a field) g. FiniteGroup g /\ #0 NOTIN G ==> (CARD (subgroup_field r g).carrier = CARD G + 1)``, 3156 rpt (stripDup[FiniteGroup_def]) >> 3157 `(subgroup_field r g).carrier = G UNION {#0}` by rw[subgroup_field_property] >> 3158 `G INTER {#0} = {}` by metis_tac[IN_INTER, IN_SING, MEMBER_NOT_EMPTY] >> 3159 rw[CARD_UNION_EQN]); 3160 3161(* Theorem: Field r /\ g <= f* ==> #0 IN G UNION {#0} /\ #1 IN G UNION {#0} *) 3162(* Proof: 3163 Note #1 IN G by field_subgroup_property 3164 ==> #1 IN G UNION {#0} by IN_UNION 3165 and #0 IN G UNION {#0} by IN_UNION, IN_SING 3166*) 3167val subgroup_field_has_ids = store_thm( 3168 "subgroup_field_has_ids", 3169 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> #0 IN G UNION {#0} /\ #1 IN G UNION {#0}``, 3170 ntac 3 strip_tac >> 3171 metis_tac[field_subgroup_property, IN_UNION, IN_SING]); 3172 3173(* Theorem: Field r /\ g <= f* ==> !x. x IN G UNION {#0} ==> x IN R *) 3174(* Proof: 3175 Note x IN G UNION {#0} 3176 ==> x IN G \/ (x = #0) by IN_UNION, IN_SING 3177 If x IN G, x IN R by field_subgroup_element 3178 If x = #0, #0 IN R by field_zero_element 3179*) 3180val subgroup_field_element = store_thm( 3181 "subgroup_field_element", 3182 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> !x. x IN G UNION {#0} ==> x IN R``, 3183 metis_tac[IN_UNION, IN_SING, field_zero_element, field_subgroup_element]); 3184 3185(* Theorem: Field r /\ g <= f* ==> !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x * y IN G UNION {#0} *) 3186(* Proof: 3187 By IN_UNION, IN_SING, field_mult_lzero, field_mult_rzero, this is to show: 3188 (1) x IN G /\ y IN G ==> x * y IN G 3189 Note g <= f* ==> Group g by Subgroup_def 3190 This is true by group_op_element 3191*) 3192val subgroup_field_mult_element = store_thm( 3193 "subgroup_field_mult_element", 3194 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> 3195 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x * y IN G UNION {#0}``, 3196 rpt (stripDup[Subgroup_def]) >> 3197 `!x. x IN G ==> x IN R+` by metis_tac[SUBSET_DEF, field_mult_carrier] >> 3198 `!x. x IN R+ <=> x IN R /\ x <> #0` by rw[field_nonzero_eq] >> 3199 fs[] >> 3200 metis_tac[group_op_element]); 3201 3202(* Theorem: Field r /\ g <= f* ==> !x. x IN G UNION {#0} ==> !n. x ** n IN G UNION {#0} *) 3203(* Proof: 3204 By IN_UNION, IN_SING, field_mult_lzero, field_mult_rzero, this is to show: 3205 (1) x IN G ==> x ** n IN G 3206 Note g <= f* ==> Group g by Subgroup_def 3207 Thus g.exp x n IN G by group_exp_element 3208 g.exp x n 3209 = f*.exp x n by subgroup_exp 3210 = x ** n by field_nonzero_mult_property 3211 (2) #0 ** n IN G \/ (#0 ** n = #0) 3212 If n = 0, #0 ** 0 = #1 by field_zero_exp 3213 and #1 IN G by field_subgroup_property 3214 If n <> 0, #0 ** n = #0 by field_zero_exp 3215*) 3216val subgroup_field_exp_element = store_thm( 3217 "subgroup_field_exp_element", 3218 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> 3219 !x. x IN G UNION {#0} ==> !n. x ** n IN G UNION {#0}``, 3220 rpt (stripDup[Subgroup_def]) >> 3221 `!x. x IN G ==> x IN R+` by metis_tac[SUBSET_DEF, field_mult_carrier] >> 3222 `!x. x IN R+ <=> x IN R /\ x <> #0` by rw[field_nonzero_eq] >> 3223 fs[] >- 3224 metis_tac[group_exp_element, subgroup_exp, field_nonzero_mult_property] >> 3225 rw[field_zero_exp, field_subgroup_property]); 3226 3227(* Theorem: Field r /\ g <= f* ==> !x. x IN G ==> |/ x IN G *) 3228(* Proof: 3229 Note g <= f* ==> Group g by Subgroup_def 3230 so x IN G ==> g.inv x IN G by group_inv_element 3231 and g.inv x = |/ x by field_subgroup_inv 3232 Hence |/ x IN G. 3233*) 3234val subgroup_field_inv_element = store_thm( 3235 "subgroup_field_inv_element", 3236 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> !x. x IN G ==> |/ x IN G``, 3237 metis_tac[Subgroup_def, field_subgroup_inv, group_inv_element]); 3238 3239(* ------------------------------------------------------------------------- *) 3240(* Subgroup Field Additive Closure *) 3241(* ------------------------------------------------------------------------- *) 3242 3243(* Theorem: FiniteField r /\ g <= f* ==> 3244 !x. x IN G UNION {#0} <=> x IN R /\ (x ** (CARD G + 1) = x) *) 3245(* Proof: 3246 Let n = CARD G + 1. 3247 x IN G UNION {#0} 3248 <=> x IN roots (master n) by field_subgroup_master_roots 3249 <=> x IN R /\ root (master n) x by poly_roots_member 3250 <=> x IN R /\ (x ** n = x) by poly_master_root 3251*) 3252val subgroup_field_element_iff_master_root = store_thm( 3253 "subgroup_field_element_iff_master_root", 3254 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> 3255 !x. x IN G UNION {#0} <=> x IN R /\ (x ** (CARD G + 1) = x)``, 3256 metis_tac[field_subgroup_master_roots, poly_roots_member, poly_master_root, finite_field_is_field, field_is_ring]); 3257 3258(* This is the more accessible form of field_subgroup_master_roots, 3259 the key to show that (subgroup_field r g).sum has additive closure. 3260*) 3261 3262(* Theorem: FiniteField r /\ g <= f* ==> !n. (CARD G = (char r) ** n - 1) ==> 3263 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x + y IN G UNION {#0} *) 3264(* Proof: 3265 Note FiniteGroup g by field_subgroup_finite_group 3266 so 0 < CARD G by finite_group_card_pos, FiniteGroup g 3267 ==> (char r) ** n = CARD G + 1 by arithmetic, 0 < CARD G 3268 3269 Now x IN R /\ y IN R by subgroup_field_element 3270 so x + y IN R by field_add_element 3271 3272 Let m = (char r) ** n. 3273 (x + y) ** m 3274 = x ** m + y ** m by finite_field_freshman_all 3275 = x + y by subgroup_field_element_iff_master_root 3276 Thus x + y IN G UNION {#0} by subgroup_field_element_iff_master_root 3277*) 3278val subgroup_field_add_element = store_thm( 3279 "subgroup_field_add_element", 3280 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> !n. (CARD G = (char r) ** n - 1) ==> 3281 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x + y IN G UNION {#0}``, 3282 rpt (stripDup[FiniteField_def]) >> 3283 `FiniteGroup g` by metis_tac[field_subgroup_finite_group] >> 3284 `0 < CARD G` by rw[finite_group_card_pos] >> 3285 `(char r) ** n = CARD G + 1` by decide_tac >> 3286 `x IN R /\ y IN R` by metis_tac[subgroup_field_element] >> 3287 `x + y IN R` by rw[] >> 3288 metis_tac[finite_field_freshman_all, subgroup_field_element_iff_master_root]); 3289 3290(* Theorem: FiniteField r /\ g <= f* ==> !n. (CARD G = (char r) ** n - 1) ==> 3291 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x - y IN G UNION {#0} *) 3292(* Proof: 3293 Note FiniteGroup g by field_subgroup_finite_group 3294 so 0 < CARD G by finite_group_card_pos, FiniteGroup g 3295 ==> (char r) ** n = CARD G + 1 by arithmetic, 0 < CARD G 3296 3297 Now x IN R /\ y IN R by subgroup_field_element 3298 so x - y IN R by field_sub_element 3299 3300 Let m = (char r) ** n. 3301 (x - y) ** m 3302 = x ** m - y ** m by finite_field_freshman_all_sub 3303 = x - y by subgroup_field_element_iff_master_root 3304 Thus x - y IN G UNION {#0} by subgroup_field_element_iff_master_root 3305*) 3306val subgroup_field_sub_element = store_thm( 3307 "subgroup_field_sub_element", 3308 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> !n. (CARD G = (char r) ** n - 1) ==> 3309 !x y. x IN G UNION {#0} /\ y IN G UNION {#0} ==> x - y IN G UNION {#0}``, 3310 rpt (stripDup[FiniteField_def]) >> 3311 `FiniteGroup g` by metis_tac[field_subgroup_finite_group] >> 3312 `0 < CARD G` by rw[finite_group_card_pos] >> 3313 `(char r) ** n = CARD G + 1` by decide_tac >> 3314 `x IN R /\ y IN R` by metis_tac[subgroup_field_element] >> 3315 `x - y IN R` by rw[] >> 3316 metis_tac[finite_field_freshman_all_sub, subgroup_field_element_iff_master_root]); 3317 3318(* Theorem: FiniteField r /\ g <= f* ==> !n. (CARD G = (char r) ** n - 1) ==> 3319 !x. x IN G UNION {#0} ==> -x IN G UNION {#0} *) 3320(* Proof: 3321 Note x IN R by subgroup_field_element 3322 so -x IN R by field_neg_element 3323 Also #0 IN G UNION {#0} by IN_UNION, IN_SING 3324 and #0 - x = -x by field_zero_sub 3325 Since #0 - x IN G by subgroup_field_sub_element 3326 so -x IN G by above 3327*) 3328val subgroup_field_neg_element = store_thm( 3329 "subgroup_field_neg_element", 3330 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> !n. (CARD G = (char r) ** n - 1) ==> 3331 !x. x IN G UNION {#0} ==> -x IN G UNION {#0}``, 3332 rpt (stripDup[FiniteField_def]) >> 3333 `x IN R` by metis_tac[subgroup_field_element] >> 3334 `-x IN R` by rw[] >> 3335 `#0 IN G UNION {#0} /\ (-x = #0 - x)` by rw[] >> 3336 metis_tac[subgroup_field_sub_element]); 3337 3338(* ------------------------------------------------------------------------- *) 3339(* Subgroup Field Properties *) 3340(* ------------------------------------------------------------------------- *) 3341 3342(* Theorem: Field r /\ g <= f* ==> AbelianMonoid (subgroup_field r g).prod *) 3343(* Proof: 3344 Note g <= f* 3345 ==> Group g /\ G SUBSET F* by Subgroup_def 3346 Thus !x. x IN G ==> x IN R+ by SUBSET_DEF, field_mult_carrier 3347 Also !x. x IN R+ <=> x IN R /\ x <> #0 by field_nonzero_eq 3348 By AbelianMonoid_def, Monoid_def, subgroup_field_property, subgroup_field_prod_property, this is to show: 3349 (1) x IN G UNION {#0} /\ y IN G UNION {#0} ==> x * y IN G UNION {#0} 3350 This is true by subgroup_field_mult_element 3351 (2) x IN G UNION {#0} /\ y IN G UNION {#0} /\ z IN G UNION {#0} ==> x * y * z = x * (y * z) 3352 By IN_UNION, IN_SING, field_mult_lzero, field_mult_rzero, only need to show: 3353 x IN G /\ y IN G /\ z IN G ==> x * y * z = x * (y * z), true by group_assoc 3354 (3) #1 IN G UNION {#0}, true by field_subgroup_property 3355 (4) x IN G UNION {#0} ==> #1 * x = x, true by field_mult_lone 3356 (5) x IN G UNION {#0} ==> x * #1 = x, true by field_mult_rone 3357 (6) x IN G UNION {#0} /\ y IN G UNION {#0} ==> x * y = y * x 3358 By IN_UNION, IN_SING, field_mult_lzero, field_mult_rzero, only need to show: 3359 x IN G /\ y IN G ==> x * y IN G 3360 Note AbelianGroup f* by field_subgroup_abelian_group 3361 Hence x IN G /\ y IN G ==> x * y IN G by AbelianGroup_def 3362*) 3363val subgroup_field_prod_abelian_monoid = store_thm( 3364 "subgroup_field_prod_abelian_monoid", 3365 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> AbelianMonoid (subgroup_field r g).prod``, 3366 rpt (stripDup[Subgroup_def]) >> 3367 `!x. x IN G ==> x IN R+` by metis_tac[SUBSET_DEF, field_mult_carrier] >> 3368 `!x. x IN R+ <=> x IN R /\ x <> #0` by rw[field_nonzero_eq] >> 3369 rw_tac std_ss[AbelianMonoid_def, Monoid_def, subgroup_field_property, subgroup_field_prod_property] >- 3370 rw[subgroup_field_mult_element] >- 3371 (fs[] >> 3372 metis_tac[group_assoc]) >- 3373 rw[field_subgroup_property] >- 3374 fs[] >- 3375 fs[] >> 3376 fs[] >> 3377 metis_tac[field_subgroup_abelian_group, AbelianGroup_def]); 3378 3379(* Theorem: Field r /\ g <= f* ==> Monoid (subgroup_field r g).prod *) 3380(* Proof: by subgroup_field_prod_abelian_monoid, AbelianMonoid_def *) 3381val subgroup_field_prod_monoid = store_thm( 3382 "subgroup_field_prod_monoid", 3383 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> Monoid (subgroup_field r g).prod``, 3384 metis_tac[subgroup_field_prod_abelian_monoid, AbelianMonoid_def]); 3385 3386(* Theorem: FiniteField r /\ g <= f* ==> 3387 !n. (CARD G = (char r) ** n - 1) ==> AbelianGroup (subgroup_field r g).sum *) 3388(* Proof: 3389 Note g <= f* 3390 ==> Group g /\ G SUBSET F* by Subgroup_def 3391 Thus !x. x IN G ==> x IN R+ by SUBSET_DEF, field_mult_carrier 3392 Also !x. x IN R+ <=> x IN R /\ x <> #0 by field_nonzero_eq 3393 By AbelianGroup_def, group_def_alt, subgroup_field_property, this is to show: 3394 (1) x IN G UNION {#0} /\ y IN G UNION {#0} ==> x + y IN G UNION {#0} 3395 This is true by subgroup_field_add_element 3396 (2) x IN G UNION {#0} /\ y IN G UNION {#0} /\ z IN G UNION {#0} ==> x + y + z = x + (y + z) 3397 Since x IN R /\ y IN R /\ z IN R by subgroup_field_element 3398 Hence x + y + z = x + (y + z) by field_add_assoc 3399 (3) #0 IN G UNION {#0}, true by subgroup_field_has_ids 3400 (4) x IN G UNION {#0} ==> #0 + x = x 3401 Since x IN R by subgroup_field_element 3402 Hence #0 + x = x by field_add_lzero 3403 (5) x IN G UNION {#0} ==> ?y. y IN G UNION {#0} /\ (y + x = #0) 3404 Let y = -x, 3405 Then -x IN G UNION {#0} by subgroup_field_neg_element 3406 and -x + x = #0 by field_add_lneg 3407 (6) x IN G UNION {#0} /\ y IN G UNION {#0} ==> x + y = y + x 3408 Since x IN R /\ y IN R by subgroup_field_element 3409 Hence x + y + z = x + (y + z) by field_add_comm 3410*) 3411val subgroup_field_sum_abelian_group = store_thm( 3412 "subgroup_field_sum_abelian_group", 3413 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> 3414 !n. (CARD G = (char r) ** n - 1) ==> AbelianGroup (subgroup_field r g).sum``, 3415 rpt (stripDup[FiniteField_def, Subgroup_def]) >> 3416 `!x. x IN G ==> x IN R+` by metis_tac[SUBSET_DEF, field_mult_carrier] >> 3417 `!x. x IN R+ <=> x IN R /\ x <> #0` by rw[field_nonzero_eq] >> 3418 rw_tac std_ss[AbelianGroup_def, group_def_alt, subgroup_field_property] >- 3419 metis_tac[subgroup_field_add_element] >- 3420 metis_tac[field_add_assoc, subgroup_field_element] >- 3421 rw[] >- 3422 fs[] >- 3423 metis_tac[subgroup_field_neg_element, field_add_lneg, subgroup_field_element] >> 3424 metis_tac[field_add_comm, subgroup_field_element]); 3425 3426(* Theorem: FiniteField r /\ g <= f* ==> 3427 !n. (CARD G = (char r) ** n - 1) ==> Group (subgroup_field r g).sum *) 3428(* Proof: by subgroup_field_sum_abelian_group, AbelianGroup_def *) 3429val subgroup_field_sum_group = store_thm( 3430 "subgroup_field_sum_group", 3431 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> 3432 !n. (CARD G = (char r) ** n - 1) ==> Group (subgroup_field r g).sum``, 3433 metis_tac[subgroup_field_sum_abelian_group, AbelianGroup_def]); 3434 3435(* Theorem: FiniteField r /\ g <= f* ==> 3436 !n. (CARD G = (char r) ** n - 1) ==> Ring (subgroup_field r g) *) 3437(* Proof: 3438 By Ring_def, subgroup_field_property, subgroup_field_prod_property, this is to show: 3439 (1) AbelianGroup (subgroup_field r g).sum, true by subgroup_field_sum_abelian_group 3440 (2) AbelianMonoid (subgroup_field r g).prod, true by subgroup_field_prod_abelian_monoid 3441 (3) x IN G UNION {#0} /\ y IN G UNION {#0} /\ z IN G UNION {#0} ==> x * (y + z) = x * y + x * z 3442 Since x IN R /\ y IN R /\ z IN R by subgroup_field_element 3443 Hence x * (y + z) = x * y + x * z by field_mult_radd 3444*) 3445val subgroup_field_ring = store_thm( 3446 "subgroup_field_ring", 3447 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> 3448 !n. (CARD G = (char r) ** n - 1) ==> Ring (subgroup_field r g)``, 3449 rpt (stripDup[FiniteField_def]) >> 3450 rw_tac std_ss[Ring_def, subgroup_field_property, subgroup_field_prod_property] >- 3451 metis_tac[subgroup_field_sum_abelian_group] >- 3452 rw[subgroup_field_prod_abelian_monoid] >> 3453 metis_tac[field_mult_radd, subgroup_field_element]); 3454 3455(* Theorem: FiniteField r /\ g <= f* ==> 3456 !n. (CARD G = (char r) ** n - 1) ==> Field (subgroup_field r g) *) 3457(* Proof: 3458 By field_def_by_inv, subgroup_field_property, subgroup_field_prod_property, this is to show: 3459 (1) Ring (subgroup_field r g), true by subgroup_field_ring 3460 (2) #1 <> #0, true by field_one_ne_zero 3461 (3) x IN G UNION {#0} /\ x <> #0 ==> ?y. y IN G UNION {#0} /\ (x * y = #1) 3462 Note x IN G by IN_UNION, IN_SING, x <> #0 3463 so |/ x IN G by subgroup_field_inv_element 3464 Also x IN R+ by field_subgroup_property, SUBSET_DEF 3465 so x * |/ x = #1 by field_mult_rinv 3466 Take y = |/ x, then y IN G UNION {#0} by IN_UNION 3467*) 3468val subgroup_field_field = store_thm( 3469 "subgroup_field_field", 3470 ``!(r:'a field) (g:'a group). FiniteField r /\ g <= f* ==> 3471 !n. (CARD G = (char r) ** n - 1) ==> Field (subgroup_field r g)``, 3472 rpt (stripDup[FiniteField_def]) >> 3473 rw_tac std_ss[field_def_by_inv, subgroup_field_property, subgroup_field_prod_property] >- 3474 metis_tac[subgroup_field_ring] >- 3475 rw[] >> 3476 `x IN G` by metis_tac[IN_UNION, IN_SING] >> 3477 `x IN R+` by metis_tac[field_subgroup_property, SUBSET_DEF] >> 3478 metis_tac[subgroup_field_inv_element, field_mult_rinv, IN_UNION]); 3479 3480(* Theorem: Field r /\ g <= f* ==> subfield (subgroup_field r g) r *) 3481(* Proof: 3482 By subfield_def, FieldHomo_def, RingHomo_def, subgroup_field_property, this is to show: 3483 (1) x IN G UNION {#0} ==> x IN R, true by subgroup_field_element 3484 (2) GroupHomo I (subgroup_field r g).sum r.sum 3485 By GroupHomo_def, subgroup_field_property, field_carriers, this is to show: 3486 (1) x IN G UNION {#0} ==> x IN R, true by subgroup_field_element 3487 (2) x IN G UNION {#0} /\ y IN G UNION {#0} ==> (subgroup_field r g).sum.op x y = x + y 3488 This is true by subgroup_field_property 3489 (3) MonoidHomo I (subgroup_field r g).prod r.prod 3490 By MonoidHomo_def, subgroup_field_property, subgroup_field_prod_property, field_carriers, this is to show: 3491 (1) x IN G UNION {#0} ==> x IN R, true by subgroup_field_element 3492 (2) x IN G UNION {#0} /\ y IN G UNION {#0} ==> (subgroup_field r g).prod.op x y = x * y 3493 This is true by subgroup_field_prod_property 3494 (3) (subgroup_field r g).prod.id = #1, true by subgroup_field_prod_property 3495*) 3496val subgroup_field_subfield = store_thm( 3497 "subgroup_field_subfield", 3498 ``!(r:'a field) (g:'a group). Field r /\ g <= f* ==> subfield (subgroup_field r g) r``, 3499 rw_tac std_ss[subfield_def, FieldHomo_def, RingHomo_def, subgroup_field_property] >- 3500 metis_tac[subgroup_field_element] >- 3501 (rw_tac std_ss[GroupHomo_def, subgroup_field_property, field_carriers] >> 3502 metis_tac[subgroup_field_element]) >> 3503 rw_tac std_ss[MonoidHomo_def, subgroup_field_property, subgroup_field_prod_property, field_carriers] >> 3504 metis_tac[subgroup_field_element]); 3505 3506(* ------------------------------------------------------------------------- *) 3507(* Subfield Classification *) 3508(* ------------------------------------------------------------------------- *) 3509 3510(* ------------------------------------------------------------------------- *) 3511(* Subfield Classification - by subgroup *) 3512(* ------------------------------------------------------------------------- *) 3513 3514(* Theorem: FiniteField r /\ s <<= r ==> ?g. g <= f* /\ (CARD G = (char r) ** (fdim s) - 1) *) 3515(* Proof: 3516 Note FiniteField s by subfield_finite_field 3517 ==> CARD B = char s ** fdim s by finite_field_card_alt 3518 = char r ** fdim s by subfield_char 3519 Also FINITE B by subfield_carrier_finite 3520 and #0 IN B by subfield_ids, field_zero_element 3521 ==> B INTER {#0} = {#0} by INTER_SING 3522 3523 Let g = subset_group f* (s.prod.carrier DIFF {#0}). 3524 Then g <= f* by subfield_mult_subset_group_subgroup 3525 CARD G 3526 = CARD (B DIFF {#0}) by subset_group_property 3527 = CARD B - CARD (B INTER {#0}) by CARD_DIFF_EQN, FINITE 3528 = CARD B - CARD {#0} by above 3529 = CARD B - 1 by CARD_SING 3530 Take this g, and the result follows. 3531*) 3532val finite_field_subfield_gives_subgroup = store_thm( 3533 "finite_field_subfield_gives_subgroup", 3534 ``!(r:'a field) s. FiniteField r /\ s <<= r ==> ?g. g <= f* /\ (CARD G = (char r) ** (fdim s) - 1)``, 3535 rpt (stripDup[FiniteField_def]) >> 3536 `FiniteField s` by metis_tac[subfield_finite_field] >> 3537 `CARD B = char r ** fdim s` by rw[finite_field_card_alt, subfield_char] >> 3538 `FINITE B` by metis_tac[subfield_carrier_finite] >> 3539 `#0 IN B` by metis_tac[subfield_ids, field_zero_element] >> 3540 `B INTER {#0} = {#0}` by rw[INTER_SING] >> 3541 qabbrev_tac `g = subset_group f* (s.prod.carrier DIFF {#0})` >> 3542 `g <= f*` by rw[subfield_mult_subset_group_subgroup, Abbr`g`] >> 3543 `G = B DIFF {#0}` by rw[subset_group_property, Abbr`g`] >> 3544 `CARD G = CARD B - 1` by rw[CARD_DIFF_EQN] >> 3545 metis_tac[]); 3546 3547(* Theorem: FiniteField r ==> !g n. g <= f* /\ (CARD G = (char r) ** n - 1) ==> 3548 ?s. s <<= r /\ (fdim s = n) *) 3549(* Proof: 3550 Let p = char r. 3551 Then 1 < p by finite_field_char_gt_1 3552 Note FiniteGroup g by field_subgroup_finite_group 3553 ==> Group g /\ FINITE G by FiniteGroup_def 3554 Now G <> {} by group_carrier_nonempty 3555 so CARD G <> 0 by CARD_EQ_0 3556 ==> n <> 0 by EXP_0, CARD G = (char r) ** n - 1 3557 Thus 1 < p ** n by ONE_LT_EXP, 1 < p, n <> 0 3558 or p ** n = CARD G + 1 by 1 < p ** n 3559 3560 Let s = subset_field r (roots (master (p ** n))). 3561 Then s <<= r by poly_master_roots_subfield 3562 and B = roots (master (p ** n)) by subset_field_property 3563 Note B = G UNION {#0} by field_subgroup_master_roots 3564 and CARD B = CARD G + 1 by field_subgroup_card 3565 = p ** n by above 3566 Now char s = p by subfield_char, s <<= r 3567 and FiniteField s by subfield_finite_field, s <= r 3568 ==> fdim s = n by finite_field_dim_eq 3569 Take this s, and the result follows. 3570*) 3571val finite_field_subgroup_gives_subfield = store_thm( 3572 "finite_field_subgroup_gives_subfield", 3573 ``!r:'a field. FiniteField r ==> !g n. g <= f* /\ (CARD G = (char r) ** n - 1) ==> 3574 ?s. s <<= r /\ (fdim s = n)``, 3575 rpt (stripDup[FiniteField_def]) >> 3576 qabbrev_tac `p = char r` >> 3577 `1 < p` by rw[finite_field_char_gt_1, Abbr`p`] >> 3578 `FiniteGroup g` by metis_tac[field_subgroup_finite_group] >> 3579 `Group g /\ FINITE G` by metis_tac[FiniteGroup_def] >> 3580 `CARD G <> 0` by metis_tac[group_carrier_nonempty, CARD_EQ_0] >> 3581 `n <> 0` by metis_tac[EXP_0, DECIDE``1 - 1 = 0``] >> 3582 `1 < p ** n` by rw[ONE_LT_EXP] >> 3583 `p ** n = CARD G + 1` by decide_tac >> 3584 qabbrev_tac `s = subset_field r (roots (master (p ** n)))` >> 3585 `s <<= r` by rw[poly_master_roots_subfield, Abbr`s`, Abbr`p`] >> 3586 `B = roots (master (p ** n))` by rw[GSYM subset_field_property, Abbr`s`] >> 3587 `B = G UNION {#0}` by metis_tac[field_subgroup_master_roots] >> 3588 `CARD B = p ** n` by metis_tac[field_subgroup_card] >> 3589 `char s = p` by rw[subfield_char, Abbr`p`] >> 3590 `FiniteField s` by metis_tac[subfield_finite_field] >> 3591 `fdim s = n` by metis_tac[finite_field_dim_eq] >> 3592 metis_tac[]); 3593 3594(* Theorem: FiniteField r ==> !n. (?s. s <<= r /\ (fdim s = n)) <=> (?g. g <= f* /\ (CARD G = (char r) ** n - 1)) *) 3595(* Proof: 3596 If part: s <<= r /\ (fdim s = n)) ==> ?g. g <= f* /\ (CARD G = (char r) ** n - 1) 3597 This is true by finite_field_subfield_gives_subgroup 3598 Only-if part: g <= f* /\ (CARD G = (char r) ** n - 1) ==> ?s. s <<= r /\ (fdim s = n) 3599 This is true by finite_field_subgroup_gives_subfield 3600*) 3601val finite_field_subfield_exists_iff_subgroup_exists = store_thm( 3602 "finite_field_subfield_exists_iff_subgroup_exists", 3603 ``!r:'a field. FiniteField r ==> 3604 !n. (?s. s <<= r /\ (fdim s = n)) <=> (?g. g <= f* /\ (CARD G = (char r) ** n - 1))``, 3605 metis_tac[finite_field_subfield_gives_subgroup, finite_field_subgroup_gives_subfield]); 3606 3607(* This is a major theorem. *) 3608 3609(* Theorem: FiniteField r ==> !n. (?s. s <<= r /\ (fdim s = n)) <=> n divides fdim r *) 3610(* Proof: 3611 Note FINITE F* by field_nonzero_finite, field_mult_carrier 3612 and cyclic f* by finite_field_mult_group_cyclic 3613 Let p = char r, d = fdim r. 3614 Then 1 < p by finite_field_char_gt_1 3615 and CARD R = p ** d by finite_field_card_alt 3616 3617 ?s. s <<= r /\ (fdim s = n) 3618 <=> ?g. g <= f* /\ (CARD G = p ** n - 1) by finite_field_subfield_exists_iff_subgroup_exists 3619 <=> (p ** n - 1) divides (CARD F* ) by cyclic_subgroup_condition, cyclic f* 3620 <=> (p ** n - 1) divides (p ** d - 1) by finite_field_mult_carrier_card 3621 <=> n divides d by power_predecessor_divisibility 3622*) 3623val finite_field_subfield_exists_condition = store_thm( 3624 "finite_field_subfield_exists_condition", 3625 ``!r:'a field. FiniteField r ==> !n. (?s. s <<= r /\ (fdim s = n)) <=> n divides fdim r``, 3626 rpt (stripDup[FiniteField_def]) >> 3627 `FINITE F*` by rw[field_nonzero_finite, field_mult_carrier] >> 3628 `cyclic f*` by rw[finite_field_mult_group_cyclic] >> 3629 qabbrev_tac `p = char r` >> 3630 qabbrev_tac `d = fdim r` >> 3631 `1 < p` by rw[finite_field_char_gt_1, Abbr`p`] >> 3632 `CARD R = p ** d` by rw[finite_field_card_alt, Abbr`p`, Abbr`d`] >> 3633 `(?s. s <<= r /\ (fdim s = n)) <=> (?g. g <= f* /\ (CARD G = p ** n - 1))` by rw[finite_field_subfield_exists_iff_subgroup_exists, Abbr`p`] >> 3634 `_ = (p ** n - 1) divides (CARD F*)` by rw[cyclic_subgroup_condition] >> 3635 `_ = (p ** n - 1) divides (p ** d - 1)` by rw[finite_field_mult_carrier_card] >> 3636 `_ = n divides d` by rw[power_predecessor_divisibility] >> 3637 rw[]); 3638 3639(* This is a really cute proof of the subfield criteria. *) 3640 3641 3642(* ------------------------------------------------------------------------- *) 3643 3644(* export theory at end *) 3645val _ = export_theory(); 3646 3647(*===========================================================================*) 3648