refactor(field_theory): preparations for Chevalley–Warning (#2590)

This PR adds some preparations for the Chevalley–Warning theorem.

depends on: ~#2606, #2607, #2623~

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/algebra/group/units.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro, Johannes, Hölzl, Chris Hughes
 -/
 import logic.function.basic
 import algebra.group.to_additive
+import algebra.group.hom
 import tactic.norm_cast
 
 /-!
@@ -118,6 +119,19 @@ by rw [mul_assoc, inv_mul, mul_one]
 @[to_additive] theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
 ⟨λ h, by rw [← h, inv_mul_cancel_right], λ h, by rw [h, mul_inv_cancel_right]⟩
 
+variable (α)
+
+/-- The injective homomorphism from `units M` to the monoid `M`. -/
+@[to_additive "The injective homomorphism from `add_units M` to the additive monoid `M`."]
+def val_hom : units α →* α :=
+{ to_fun   := coe,
+  map_one' := coe_one,
+  map_mul' := coe_mul }
+
+variable {α}
+
+@[simp, to_additive] lemma coe_val_hom : (val_hom α : units α → α) = coe := rfl
+
 end units
 
 theorem nat.units_eq_one (u : units ℕ) : u = 1 :=

src/field_theory/finite.lean

@@ -9,40 +9,55 @@ import data.zmod.basic
 import linear_algebra.basis
 import ring_theory.integral_domain
 
-universes u v
-variables {K : Type u} {R : Type v}
+/-!
+# Finite fields
 
-open function finset polynomial nat
+This file contains basic results about finite fields.
+Throughout most of this file, `K` denotes a finite field
+and `q` is notation for the cardinality of `K`.
 
-namespace finite_field
+## Main results
 
-def field_of_integral_domain [fintype R] [decidable_eq R] [integral_domain R] :
-  field R :=
-{ inv := λ a, if h : a = 0 then 0
-    else fintype.bij_inv (show function.bijective (* a),
-      from fintype.injective_iff_bijective.1 $ λ _ _, (domain.mul_left_inj h).1) 1,
-  mul_inv_cancel := λ a ha, show a * dite _ _ _ = _, by rw [dif_neg ha, mul_comm];
-    exact fintype.right_inverse_bij_inv (show function.bijective (* a), from _) 1,
-  inv_zero := dif_pos rfl,
-  ..show integral_domain R, by apply_instance }
+1. Every finite integral domain is a field (`field_of_integral_domain`).
+2. The unit group of a finite field is a cyclic group of order `q - 1`.
+   (`finite_field.is_cyclic` and `card_units`)
+3. `sum_pow_units`: The sum of `x^i`, where `x` ranges over the units of `K`, is
+   - `q-1` if `q-1 ∣ i`
+   - `0`   otherwise
+4. `finite_field.card`: The cardinality `q` is a power of the characteristic of `K`.
+   See `card'` for a variant.
 
-section polynomial
+## Notation
+
+Throughout most of this file, `K` denotes a finite field
+and `q` is notation for the cardinality of `K`.
+
+-/
 
-variables [fintype R] [integral_domain R]
+variables {K : Type*} [field K] [fintype K]
+variables {R : Type*} [integral_domain R]
+local notation `q` := fintype.card K
 
-open finset polynomial
+open_locale big_operators
+
+namespace finite_field
+open finset function
+
+section polynomial
 
-/-- The cardinality of a field is at most n times the cardinality of the image of a degree n
+open polynomial
+
+/-- The cardinality of a field is at most `n` times the cardinality of the image of a degree `n`
   polynomial -/
-lemma card_image_polynomial_eval [decidable_eq R] {p : polynomial R} (hp : 0 < p.degree) :
+lemma card_image_polynomial_eval [fintype R] [decidable_eq R] {p : polynomial R} (hp : 0 < p.degree) :
   fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
 finset.card_le_mul_card_image _ _
   (λ a _, calc _ = (p - C a).roots.card : congr_arg card
     (by simp [finset.ext, mem_roots_sub_C hp, -sub_eq_add_neg])
     ... ≤ _ : card_roots_sub_C' hp)
 
 /-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution. -/
-lemma exists_root_sum_quadratic {f g : polynomial R} (hf2 : degree f = 2)
+lemma exists_root_sum_quadratic [fintype R] {f g : polynomial R} (hf2 : degree f = 2)
   (hg2 : degree g = 2) (hR : fintype.card R % 2 = 1) : ∃ a b, f.eval a + g.eval b = 0 :=
 by letI := classical.dec_eq R; exact
 suffices ¬ disjoint (univ.image (λ x : R, eval x f)) (univ.image (λ x : R, eval x (-g))),
@@ -70,9 +85,6 @@ calc 2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-
 
 end polynomial
 
-section
-variables [field K] [fintype K]
-
 lemma card_units : fintype.card (units K) = fintype.card K - 1 :=
 begin
   classical,
@@ -85,12 +97,6 @@ begin
   congr; simp [set.ext_iff, classical.em]
 end
 
-instance : is_cyclic (units K) :=
-by haveI := classical.dec_eq K;
-haveI := set_fintype (@set.univ (units K)); exact
-let ⟨g, hg⟩ := is_cyclic.exists_generator (@set.univ (units K)) in
-⟨⟨g, λ x, let ⟨n, hn⟩ := hg ⟨x, trivial⟩ in ⟨n, by rw [← is_subgroup.coe_gpow, hn]; refl⟩⟩⟩
-
 lemma prod_univ_units_id_eq_neg_one :
   univ.prod (λ x, x) = (-1 : units K) :=
 begin
@@ -104,7 +110,15 @@ begin
       this, mul_one]
 end
 
-theorem card (p : ℕ) [char_p K p] : ∃ (n : ℕ+), nat.prime p ∧ fintype.card K = p^(n : ℕ) :=
+lemma pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) :
+  a ^ (fintype.card K - 1) = 1 :=
+calc a ^ (fintype.card K - 1) = (units.mk0 a ha ^ (fintype.card K - 1) : units K) :
+    by rw [units.coe_pow, units.coe_mk0]
+  ... = 1 : by { classical, rw [← card_units, pow_card_eq_one], refl }
+
+variable (K)
+
+theorem card (p : ℕ) [char_p K p] : ∃ (n : ℕ+), nat.prime p ∧ q = p^(n : ℕ) :=
 begin
   haveI hp : fact p.prime := char_p.char_is_prime K p,
   have V : vector_space (zmod p) K, from { .. (zmod.cast_hom p K).to_module },
@@ -118,22 +132,81 @@ begin
   exact absurd this zero_ne_one,
 end
 
-theorem card' : ∃ (p : ℕ) (n : ℕ+), nat.prime p ∧ fintype.card K = p^(n : ℕ) :=
+theorem card' : ∃ (p : ℕ) (n : ℕ+), nat.prime p ∧ q = 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 :=
+begin
+  rcases char_p.exists K with ⟨p, _char_p⟩, resetI,
+  rcases card K p with ⟨n, hp, hn⟩,
+  simp only [char_p.cast_eq_zero_iff K p, hn],
+  conv { congr, rw [← nat.pow_one p] },
+  exact nat.pow_dvd_pow _ n.2,
 end
 
-lemma pow_card_sub_one_eq_one [field K] [fintype K] (a : K) (ha : a ≠ 0) :
-  a ^ (fintype.card K - 1) = 1 :=
-calc a ^ (fintype.card K - 1) = (units.mk0 a ha ^ (fintype.card K - 1) : units K) :
-    by rw [units.coe_pow, units.coe_mk0]
-  ... = 1 : by { classical, rw [← card_units, pow_card_eq_one], refl }
+lemma forall_pow_eq_one_iff (i : ℕ) :
+  (∀ x : units K, x ^ i = 1) ↔ q - 1 ∣ i :=
+begin
+  obtain ⟨x, hx⟩ := is_cyclic.exists_generator (units K),
+  classical,
+  rw [← card_units, ← order_of_eq_card_of_forall_mem_gpowers hx, order_of_dvd_iff_pow_eq_one],
+  split,
+  { intro h, apply h },
+  { intros h y,
+    rw ← powers_eq_gpowers at hx,
+    rcases hx y with ⟨j, rfl⟩,
+    rw [← pow_mul, mul_comm, pow_mul, h, one_pow], }
+end
+
+/-- The sum of `x ^ i` as `x` ranges over the units of a finite field of cardinality `q`
+is equal to `0` unless `(q - 1) ∣ i`, in which case the sum is `q - 1`. -/
+lemma sum_pow_units (i : ℕ) :
+  ∑ x : units K, (x ^ i : K) = if (q - 1) ∣ i then -1 else 0 :=
+begin
+  let φ : units K →* K :=
+  { to_fun   := λ x, x ^ i,
+    map_one' := by rw [units.coe_one, one_pow],
+    map_mul' := by { intros, rw [units.coe_mul, mul_pow] } },
+  haveI : decidable (φ = 1) := by { classical, apply_instance },
+  calc ∑ x : units K, φ x = if φ = 1 then fintype.card (units K) else 0 : sum_hom_units φ
+                      ... = if (q - 1) ∣ i then -1 else 0 : _,
+  suffices : (q - 1) ∣ i ↔ φ = 1,
+  { simp only [this],
+    split_ifs with h h, swap, refl,
+    rw [card_units, nat.cast_sub, cast_card_eq_zero, nat.cast_one, zero_sub],
+    show 1 ≤ q, from fintype.card_pos_iff.mpr ⟨0⟩ },
+  rw [← forall_pow_eq_one_iff, monoid_hom.ext_iff],
+  apply forall_congr, intro x,
+  rw [units.ext_iff, units.coe_pow, units.coe_one, monoid_hom.one_apply],
+  refl,
+end
+
+/-- The sum of `x ^ i` as `x` ranges over a finite field of cardinality `q`
+is equal to `0` if `i < q - 1`. -/
+lemma sum_pow_lt_card_sub_one (i : ℕ) (h : i < q - 1) :
+  ∑ x : K, x ^ i = 0 :=
+begin
+  by_cases hi : i = 0,
+  { simp only [hi, add_monoid.smul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero], },
+  classical,
+  have hiq : ¬ (q - 1) ∣ i, { contrapose! h,  exact nat.le_of_dvd (nat.pos_of_ne_zero hi) h },
+  let φ : units K ↪ K := ⟨coe, units.ext⟩,
+  have : univ.map φ = univ \ {0},
+  { ext x,
+    simp only [true_and, embedding.coe_fn_mk, mem_sdiff, units.exists_iff_ne_zero,
+               mem_univ, mem_map, exists_prop_of_true, mem_singleton] },
+  calc ∑ x : K, x ^ i = ∑ x in univ \ {(0 : K)}, x ^ i :
+    by rw [← sum_sdiff ({0} : finset K).subset_univ, sum_singleton,
+           zero_pow (nat.pos_of_ne_zero hi), add_zero]
+    ... = ∑ x : units K, x ^ i : by { rw [← this, univ.sum_map φ], refl }
+    ... = 0 : by { rw [sum_pow_units K i, if_neg], exact hiq, }
+end
 
 end finite_field
 
 namespace zmod
 
-open finite_field
+open finite_field polynomial
 
 lemma sum_two_squares (p : ℕ) [hp : fact p.prime] (x : zmod p) :
   ∃ a b : zmod p, a^2 + b^2 = x :=
@@ -184,6 +257,6 @@ begin
   let x' : units (zmod (n+1)) := zmod.unit_of_coprime _ h,
   have := zmod.pow_totient x',
   apply_fun (coe : units (zmod (n+1)) → zmod (n+1)) at this,
-  simpa only [-zmod.pow_totient, succ_eq_add_one, cast_pow, units.coe_one,
+  simpa only [-zmod.pow_totient, nat.succ_eq_add_one, nat.cast_pow, units.coe_one,
     nat.cast_one, cast_unit_of_coprime, units.coe_pow],
 end

src/ring_theory/integral_domain.lean

@@ -15,33 +15,59 @@ import algebra.geom_sum
 
 section
 
-open finset polynomial
-
-variables {R : Type*} [integral_domain R] (S : set (units R)) [is_subgroup S] [fintype S]
+open finset polynomial function
+open_locale big_operators nat
 
-lemma card_nth_roots_subgroup_units [decidable_eq R] {n : ℕ} (hn : 0 < n) (a : S) :
-  (univ.filter (λ b : S, b ^ n = a)).card ≤ (nth_roots n ((a : units R) : R)).card :=
-card_le_card_of_inj_on (λ a, ((a : units R) : R))
-  (by simp [mem_nth_roots hn, (units.coe_pow _ _).symm, -units.coe_pow, units.ext_iff.symm, subtype.coe_ext])
-  (by simp [units.ext_iff.symm, subtype.coe_ext.symm])
+variables {R : Type*} {G : Type*} [integral_domain R] [group G] [fintype G]
 
-instance subgroup_units_cyclic : is_cyclic S :=
-by haveI := classical.dec_eq R; exact
-is_cyclic_of_card_pow_eq_one_le
-  (λ n hn, le_trans (card_nth_roots_subgroup_units S hn 1) (card_nth_roots _ _))
+lemma card_nth_roots_subgroup_units (f : G →* R) (hf : injective f) {n : ℕ} (hn : 0 < n) (g₀ : G) :
+  ({g ∈ univ | g ^ n = g₀} : finset G).card ≤ (nth_roots n (f g₀)).card :=
+begin
+  apply card_le_card_of_inj_on f,
+  { intros g hg, rw [sep_def, mem_filter] at hg, rw [mem_nth_roots hn, ← f.map_pow, hg.2] },
+  { intros, apply hf, assumption }
+end
 
+/-- A finite subgroup of the unit group of an integral domain is cyclic. -/
+lemma is_cyclic_of_subgroup_integral_domain (f : G →* R) (hf : injective f) : is_cyclic G :=
+begin
+  haveI := classical.dec_eq G,
+  apply is_cyclic_of_card_pow_eq_one_le,
+  intros n hn,
+  convert (le_trans (card_nth_roots_subgroup_units f hf hn 1) (card_nth_roots n (f 1)))
 end
 
+/-- The unit group of a finite integral domain is cyclic. -/
+instance [fintype R] : is_cyclic (units R) :=
+is_cyclic_of_subgroup_integral_domain (units.val_hom R) $ units.ext
+
+/-- Every finite integral domain is a field. -/
+def field_of_integral_domain [fintype R] [decidable_eq R] : field R :=
+{ inv := λ a, if h : a = 0 then 0
+    else fintype.bij_inv (show function.bijective (* a),
+      from fintype.injective_iff_bijective.1 $ λ _ _, (domain.mul_left_inj h).1) 1,
+  mul_inv_cancel := λ a ha, show a * dite _ _ _ = _, by rw [dif_neg ha, mul_comm];
+    exact fintype.right_inverse_bij_inv (show function.bijective (* a), from _) 1,
+  inv_zero := dif_pos rfl,
+  ..show integral_domain R, by apply_instance }
+
 section
-variables {G : Type*} {R : Type*} [group G] [integral_domain R]
 
-open_locale big_operators nat
+variables (S : set (units R)) [is_subgroup S] [fintype S]
 
-open finset
+/-- A finite subgroup of the units of an integral domain is cyclic. -/
+instance subgroup_units_cyclic : is_cyclic S :=
+begin
+  refine is_cyclic_of_subgroup_integral_domain ⟨(coe : S → R), _, _⟩
+    (units.ext.comp subtype.val_injective),
+  { simp only [is_submonoid.coe_one, units.coe_one, coe_coe] },
+  { intros, simp only [is_submonoid.coe_mul, units.coe_mul, coe_coe] },
+end
 
-lemma card_fiber_eq_of_mem_range [fintype G]
-  {H : Type*} [group H] [decidable_eq H] (f : G →* H) {x y : H}
-  (hx : x ∈ set.range f) (hy : y ∈ set.range f) :
+end
+
+lemma card_fiber_eq_of_mem_range {H : Type*} [group H] [decidable_eq H]
+  (f : G →* H) {x y : H} (hx : x ∈ set.range f) (hy : y ∈ set.range f) :
   (univ.filter $ λ g, f g = x).card = (univ.filter $ λ g, f g = y).card :=
 begin
   rcases hx with ⟨x, rfl⟩,
@@ -56,8 +82,6 @@ begin
       mul_inv_cancel_right, inv_mul_cancel_right], }
 end
 
-variables {G} [fintype G]
-
 /-- In an integral domain, a sum indexed by a nontrivial homomorphism from a finite group is zero. -/
 lemma sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0 :=
 begin