feat(field_theory): finite fields exist (#8692)

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>
Co-authored-by: Aaron Anderson <awainverse@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

src/algebra/char_p/algebra.lean

@@ -54,6 +54,15 @@ lemma char_zero_of_injective_algebra_map {R A : Type*} [comm_semiring R] [semiri
 -- `char_p.char_p_to_char_zero A _ (char_p_of_injective_algebra_map h 0)` does not work
 -- here as it would require `ring A`.
 
+section
+
+variables (K L : Type*) [field K] [comm_semiring L] [nontrivial L] [algebra K L]
+
+lemma algebra.char_p_iff (p : ℕ) : char_p K p ↔ char_p L p :=
+(algebra_map K L).char_p_iff_char_p p
+
+end
+
 namespace free_algebra
 
 variables {R X : Type*} [comm_semiring R] (p : ℕ)

src/algebra/char_p/basic.lean

@@ -193,7 +193,24 @@ begin
   rw fact_iff at *, linarith,
 end
 
-lemma ring_hom.char_p_iff_char_p {K L : Type*} [field K] [field L] (f : K →+* L) (p : ℕ) :
+lemma char_p.neg_one_pow_char [comm_ring R] (p : ℕ) [char_p R p] [fact p.prime] :
+  (-1 : R) ^ p = -1 :=
+begin
+  rw eq_neg_iff_add_eq_zero,
+  nth_rewrite 1 ← one_pow p,
+  rw [← add_pow_char, add_left_neg, zero_pow (fact.out (nat.prime p)).pos],
+end
+
+lemma char_p.neg_one_pow_char_pow [comm_ring R] (p n : ℕ) [char_p R p] [fact p.prime] :
+  (-1 : R) ^ p ^ n = -1 :=
+begin
+  rw eq_neg_iff_add_eq_zero,
+  nth_rewrite 1 ← one_pow (p ^ n),
+  rw [← add_pow_char_pow, add_left_neg, zero_pow (pow_pos (fact.out (nat.prime p)).pos _)],
+end
+
+lemma ring_hom.char_p_iff_char_p {K L : Type*} [division_ring K] [semiring L] [nontrivial L]
+  (f : K →+* L) (p : ℕ) :
   char_p K p ↔ char_p L p :=
 begin
   split;
@@ -213,7 +230,7 @@ def frobenius : R →+* R :=
 { to_fun := λ x, x^p,
   map_one' := one_pow p,
   map_mul' := λ x y, mul_pow x y p,
-  map_zero' := zero_pow (lt_trans zero_lt_one (fact.out (nat.prime p)).one_lt),
+  map_zero' := zero_pow (fact.out (nat.prime p)).pos,
   map_add' := add_pow_char R }
 
 variable {R}

src/algebra/group_power/lemmas.lean

@@ -846,6 +846,12 @@ h.cast_int_mul_cast_int_mul m n
 
 variables (a) (m n : ℤ)
 
+@[simp] lemma cast_int_left : commute (m : R) a :=
+by { rw [← mul_one (m : R)], exact (one_left a).cast_int_mul_left m }
+
+@[simp] lemma cast_int_right : commute a m :=
+by { rw [← mul_one (m : R)], exact (one_right a).cast_int_mul_right m }
+
 @[simp] theorem self_cast_int_mul : commute a (n * a) := (commute.refl a).cast_int_mul_right n
 
 @[simp] theorem cast_int_mul_self : commute ((n : R) * a) a := (commute.refl a).cast_int_mul_left n

src/data/fintype/basic.lean

@@ -970,6 +970,9 @@ by { haveI : nontrivial α := one_lt_card_iff_nontrivial.1 h, exact exists_pair_
 lemma card_eq_one_of_forall_eq {i : α} (h : ∀ j, j = i) : card α = 1 :=
 fintype.card_eq_one_iff.2 ⟨i,h⟩
 
+lemma one_lt_card [h : nontrivial α] : 1 < fintype.card α :=
+fintype.one_lt_card_iff_nontrivial.mpr h
+
 lemma injective_iff_surjective {f : α → α} : injective f ↔ surjective f :=
 by haveI := classical.prop_decidable; exact
 have ∀ {f : α → α}, injective f → surjective f,

src/data/polynomial/algebra_map.lean

@@ -228,6 +228,10 @@ aeval_alg_hom_apply (algebra.of_id R A) x p
 lemma coeff_zero_eq_aeval_zero (p : polynomial R) : p.coeff 0 = aeval 0 p :=
 by simp [coeff_zero_eq_eval_zero]
 
+lemma coeff_zero_eq_aeval_zero' (p : polynomial R) :
+  algebra_map R A (p.coeff 0) = aeval (0 : A) p :=
+by simp [aeval_def]
+
 section comm_semiring
 
 variables [comm_semiring S] {f : R →+* S}

src/data/zmod/algebra.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import data.zmod.basic
+import algebra.algebra.basic
+
+/-!
+# The `zmod n`-algebra structure on rings whose characteristic divides `n`
+-/
+
+namespace zmod
+
+variables (R : Type*) [ring R]
+
+section
+variables {n : ℕ} (m : ℕ) [char_p R m]
+
+/-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
+def algebra' (h : m ∣ n) : algebra (zmod n) R :=
+{ smul := λ a r, a * r,
+  commutes' := λ a r, show (a * r : R) = r * a,
+  begin
+    rcases zmod.int_cast_surjective a with ⟨k, rfl⟩,
+    show zmod.cast_hom h R k * r = r * zmod.cast_hom h R k,
+    rw ring_hom.map_int_cast,
+    exact commute.cast_int_left r k,
+  end,
+  smul_def' := λ a r, rfl,
+  .. zmod.cast_hom h R }
+
+end
+
+section
+variables (n : ℕ) [char_p R n]
+
+instance : algebra (zmod n) R := algebra' R n (dvd_refl n)
+
+end
+
+end zmod

src/data/zmod/basic.lean

@@ -364,9 +364,6 @@ cast_nat_cast (dvd_refl _) k
 lemma cast_int_cast' (k : ℤ) : ((k : zmod n) : R) = k :=
 cast_int_cast (dvd_refl _) k
 
-instance (R : Type*) [comm_ring R] [char_p R n] : algebra (zmod n) R :=
-(zmod.cast_hom (dvd_refl n) R).to_algebra
-
 variables (R)
 
 lemma cast_hom_injective : function.injective (zmod.cast_hom (dvd_refl n) R) :=

src/field_theory/finite/basic.lean

@@ -5,10 +5,11 @@ Authors: Chris Hughes, Joey van Langen, Casper Putz
 -/
 import tactic.apply_fun
 import data.equiv.ring
-import data.zmod.basic
-import linear_algebra.basis
+import data.zmod.algebra
+import linear_algebra.finite_dimensional
 import ring_theory.integral_domain
 import field_theory.separable
+import field_theory.splitting_field
 
 /-!
 # Finite fields
@@ -121,12 +122,19 @@ calc a ^ (fintype.card K - 1) = (units.mk0 a ha ^ (fintype.card K - 1) : units K
 
 lemma pow_card (a : K) : a ^ q = a :=
 begin
-  have hp : fintype.card K > 0 := fintype.card_pos_iff.2 (by apply_instance),
+  have hp : 0 < fintype.card K := lt_trans zero_lt_one fintype.one_lt_card,
   by_cases h : a = 0, { rw h, apply zero_pow hp },
   rw [← nat.succ_pred_eq_of_pos hp, pow_succ, nat.pred_eq_sub_one,
     pow_card_sub_one_eq_one a h, mul_one],
 end
 
+lemma pow_card_pow (n : ℕ) (a : K) : a ^ q ^ n = a :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp [pow_succ, pow_mul, ih, pow_card], },
+end
+
 variable (K)
 
 theorem card (p : ℕ) [char_p K p] : ∃ (n : ℕ+), nat.prime p ∧ q = p^(n : ℕ) :=
@@ -213,6 +221,73 @@ begin
     ... = 0 : by { rw [sum_pow_units K i, if_neg], exact hiq, }
 end
 
+section is_splitting_field
+open polynomial
+
+section
+
+variables (K' : Type*) [field K'] {p n : ℕ}
+
+lemma X_pow_card_sub_X_nat_degree_eq (hp : 1 < p) :
+  (X ^ p - X : polynomial K').nat_degree = p :=
+begin
+  have h1 : (X : polynomial K').degree < (X ^ p : polynomial K').degree,
+  { rw [degree_X_pow, degree_X],
+    exact_mod_cast hp },
+  rw [nat_degree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1), nat_degree_X_pow],
+end
+
+lemma X_pow_card_pow_sub_X_nat_degree_eq (hn : n ≠ 0) (hp : 1 < p) :
+  (X ^ p ^ n - X : polynomial K').nat_degree = p ^ n :=
+X_pow_card_sub_X_nat_degree_eq K' $ nat.one_lt_pow _ _ (nat.pos_of_ne_zero hn) hp
+
+lemma X_pow_card_sub_X_ne_zero (hp : 1 < p) : (X ^ p - X : polynomial K') ≠ 0 :=
+ne_zero_of_nat_degree_gt $
+calc 1 < _ : hp
+... = _ : (X_pow_card_sub_X_nat_degree_eq K' hp).symm
+
+lemma X_pow_card_pow_sub_X_ne_zero (hn : n ≠ 0) (hp : 1 < p) :
+  (X ^ p ^ n - X : polynomial K') ≠ 0 :=
+X_pow_card_sub_X_ne_zero K' $ nat.one_lt_pow _ _ (nat.pos_of_ne_zero hn) hp
+
+end
+
+variables (p : ℕ) [fact p.prime] [char_p K p]
+lemma roots_X_pow_card_sub_X : roots (X^q - X : polynomial K) = finset.univ.val :=
+begin
+  classical,
+  have aux : (X^q - X : polynomial K) ≠ 0 := X_pow_card_sub_X_ne_zero K fintype.one_lt_card,
+  have : (roots (X^q - X : polynomial K)).to_finset = finset.univ,
+  { rw eq_univ_iff_forall,
+    intro x,
+    rw [multiset.mem_to_finset, mem_roots aux, is_root.def, eval_sub, eval_pow, eval_X, sub_eq_zero,
+      pow_card] },
+  rw [←this, multiset.to_finset_val, eq_comm, multiset.erase_dup_eq_self],
+  apply nodup_roots,
+  rw separable_def,
+  convert is_coprime_one_right.neg_right,
+  rw [derivative_sub, derivative_X, derivative_X_pow, ←C_eq_nat_cast,
+    C_eq_zero.mpr (char_p.cast_card_eq_zero K), zero_mul, zero_sub],
+end
+
+instance : is_splitting_field (zmod p) K (X^q - X) :=
+{ splits :=
+  begin
+    have h : (X^q - X : polynomial K).nat_degree = q :=
+      X_pow_card_sub_X_nat_degree_eq K fintype.one_lt_card,
+    rw [←splits_id_iff_splits, splits_iff_card_roots, map_sub, map_pow, map_X, h,
+      roots_X_pow_card_sub_X K, ←finset.card_def, finset.card_univ],
+  end,
+  adjoin_roots :=
+  begin
+    classical,
+    transitivity algebra.adjoin (zmod p) ((roots (X^q - X : polynomial K)).to_finset : set K),
+    { simp only [map_pow, map_X, map_sub], convert rfl },
+    { rw [roots_X_pow_card_sub_X, val_to_finset, coe_univ, algebra.adjoin_univ], }
+  end }
+
+end is_splitting_field
+
 variables {K}
 
 theorem frobenius_pow {p : ℕ} [fact p.prime] [char_p K p] {n : ℕ} (hcard : q = p^n) :
@@ -292,13 +367,36 @@ begin
     nat.cast_one, coe_unit_of_coprime, units.coe_pow],
 end
 
+section
+
+variables {V : Type*} [add_comm_group V] [module K V]
+
+-- should this go in a namespace?
+-- finite_dimensional would be natural,
+-- but we don't assume it...
+lemma card_eq_pow_finrank [fintype V] :
+  fintype.card V = q ^ (finite_dimensional.finrank K V) :=
+begin
+  let b := is_noetherian.finset_basis K V,
+  rw [module.card_fintype b, ← finite_dimensional.finrank_eq_card_basis b],
+end
+
+end
+
 open finite_field
 namespace zmod
 
 /-- A variation on Fermat's little theorem. See `zmod.pow_card_sub_one_eq_one` -/
 @[simp] lemma pow_card {p : ℕ} [fact p.prime] (x : zmod p) : x ^ p = x :=
 by { have h := finite_field.pow_card x, rwa zmod.card p at h }
 
+@[simp] lemma pow_card_pow {n p : ℕ} [fact p.prime] (x : zmod p) : x ^ p ^ n = x :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp [pow_succ, pow_mul, ih, pow_card], },
+end
+
 @[simp] lemma frobenius_zmod (p : ℕ) [fact p.prime] :
   frobenius (zmod p) p = ring_hom.id _ :=
 by { ext a, rw [frobenius_def, zmod.pow_card, ring_hom.id_apply] }