feat(field_theory/finite/galois_field): uniqueness of finite fields (#…

…9817)

Every finite field is isomorphic to some Galois field. Closes #9599 



Co-authored-by: Anupam Nayak <88547452+AaronGreen001@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/field_theory/finite/basic.lean

@@ -151,7 +151,8 @@ begin
   exact absurd this zero_ne_one,
 end
 
-theorem card' : ∃ (p : ℕ) (n : ℕ+), nat.prime p ∧ q = p^(n : ℕ) :=
+-- this statement doesn't use `q` because we want `K` to be an explicit parameter
+theorem card' : ∃ (p : ℕ) (n : ℕ+), nat.prime p ∧ fintype.card K = p^(n : ℕ) :=
 let ⟨p, hc⟩ := char_p.exists K in ⟨p, @finite_field.card K _ _ p hc⟩
 
 @[simp] lemma cast_card_eq_zero : (q : K) = 0 :=

src/field_theory/finite/galois_field.lean

@@ -20,6 +20,10 @@ It is a finite field with `p ^ n` elements.
 
 * `galois_field p n` is a field with `p ^ n` elements
 
+## Main Results
+
+- `galois_field.alg_equiv_galois_field`: Uniqueness of finite fields
+
 -/
 
 noncomputable theory
@@ -135,4 +139,30 @@ have inst : is_splitting_field (zmod p) (zmod p) (X ^ p ^ 1 - X),
   by { rw h, apply_instance },
 by exactI (is_splitting_field.alg_equiv (zmod p) (X ^ (p ^ 1) - X : polynomial (zmod p))).symm
 
+variables {K : Type*} [field K] [fintype K] [algebra (zmod p) K]
+
+theorem splits_X_pow_card_sub_X : splits (algebra_map (zmod p) K) (X ^ fintype.card K - X) :=
+by rw [←splits_id_iff_splits, map_sub, map_pow, map_X, splits_iff_card_roots,
+  finite_field.roots_X_pow_card_sub_X, ←finset.card_def, finset.card_univ,
+  finite_field.X_pow_card_sub_X_nat_degree_eq]; exact fintype.one_lt_card
+
+lemma is_splitting_field_of_card_eq (h : fintype.card K = p ^ n) :
+  is_splitting_field (zmod p) K (X ^ (p ^ n) - X) :=
+{ splits := by { rw ← h, exact splits_X_pow_card_sub_X p },
+  adjoin_roots :=
+  begin
+    have hne : n ≠ 0,
+    { rintro rfl, rw [pow_zero, fintype.card_eq_one_iff_nonempty_unique] at h,
+      cases h, resetI, exact false_of_nontrivial_of_subsingleton K },
+    refine algebra.eq_top_iff.mpr (λ x, algebra.subset_adjoin _),
+    rw [map_sub, map_pow, map_X, finset.mem_coe, multiset.mem_to_finset, mem_roots,
+        is_root.def, eval_sub, eval_pow, eval_X, ← h, finite_field.pow_card, sub_self],
+    exact finite_field.X_pow_card_pow_sub_X_ne_zero K hne (fact.out _)
+  end }
+
+/-- Uniqueness of finite fields : Any finite field is isomorphic to some Galois field. -/
+def alg_equiv_galois_field (h : fintype.card K = p ^ n) :
+  K ≃ₐ[zmod p] galois_field p n :=
+by haveI := is_splitting_field_of_card_eq _ _ h; exact is_splitting_field.alg_equiv _ _
+
 end galois_field