feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship …

…theorem (#3953)

adds several assorted lemmas about matrices and `zmod p`
proves that if `M` is a square matrix with entries in `zmod p`, then `tr M^p = tr M`, needed for friendship theorem




Co-authored-by: Aaron Anderson <awainverse@gmail.com>

src/algebra/char_p.lean

@@ -67,7 +67,7 @@ classical.by_cases
 theorem char_p.exists_unique (α : Type u) [semiring α] : ∃! p, char_p α p :=
 let ⟨c, H⟩ := char_p.exists α in ⟨c, H, λ y H2, char_p.eq α H2 H⟩
 
-/-- Noncomuptable function that outputs the unique characteristic of a semiring. -/
+/-- Noncomputable function that outputs the unique characteristic of a semiring. -/
 noncomputable def ring_char (α : Type u) [semiring α] : ℕ :=
 classical.some (char_p.exists_unique α)
 
@@ -79,8 +79,8 @@ theorem ring_char.eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) : p
 (classical.some_spec (char_p.exists_unique α)).2 p C
 
 theorem add_pow_char_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
-  [char_p R p] (x y : R) (h : commute x y):
-(x + y)^p = x^p + y^p :=
+  [char_p R p] (x y : R) (h : commute x y) :
+  (x + y)^p = x^p + y^p :=
 begin
   rw [commute.add_pow h, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
   rw [nat.cast_one, mul_one, mul_one, add_right_inj],
@@ -93,14 +93,50 @@ begin
   rwa ← finset.mem_range
 end
 
-theorem add_pow_char (α : Type u) [comm_ring α] {p : ℕ} (hp : nat.prime p)
-  [char_p α p] (x y : α) : (x + y)^p = x^p + y^p :=
+theorem add_pow_char_pow_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
+  [char_p R p] {n : ℕ} (x y : R) (h : commute x y) :
+  (x + y) ^ (p ^ n) = x ^ (p ^ n) + y ^ (p ^ n) :=
+begin
+  induction n, { simp, },
+  rw [nat.pow_succ, pow_mul, pow_mul, pow_mul, n_ih],
+  apply add_pow_char_of_commute, apply commute.pow_pow h,
+end
+
+theorem sub_pow_char_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
+  [char_p R p] (x y : R) (h : commute x y) :
+  (x - y)^p = x^p - y^p :=
 begin
-  haveI : fact p.prime := hp,
-  apply add_pow_char_of_commute,
-  apply commute.all,
+  rw [eq_sub_iff_add_eq, ← add_pow_char_of_commute _ _ _ (commute.sub_left h rfl)],
+  simp, repeat {apply_instance},
 end
 
+theorem sub_pow_char_pow_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
+  [char_p R p] {n : ℕ} (x y : R) (h : commute x y) :
+  (x - y) ^ (p ^ n) = x ^ (p ^ n) - y ^ (p ^ n) :=
+begin
+  induction n, { simp, },
+  rw [nat.pow_succ, pow_mul, pow_mul, pow_mul, n_ih],
+  apply sub_pow_char_of_commute, apply commute.pow_pow h,
+end
+
+theorem add_pow_char (α : Type u) [comm_ring α] {p : ℕ} [fact p.prime]
+  [char_p α p] (x y : α) : (x + y)^p = x^p + y^p :=
+add_pow_char_of_commute _ _ _ (commute.all _ _)
+
+theorem add_pow_char_pow (R : Type u) [comm_ring R] {p : ℕ} [fact p.prime]
+  [char_p R p] {n : ℕ} (x y : R) :
+  (x + y) ^ (p ^ n) = x ^ (p ^ n) + y ^ (p ^ n) :=
+add_pow_char_pow_of_commute _ _ _ (commute.all _ _)
+
+theorem sub_pow_char (α : Type u) [comm_ring α] {p : ℕ} [fact p.prime]
+  [char_p α p] (x y : α) : (x - y)^p = x^p - y^p :=
+sub_pow_char_of_commute _ _ _ (commute.all _ _)
+
+theorem sub_pow_char_pow (R : Type u) [comm_ring R] {p : ℕ} [fact p.prime]
+  [char_p R p] {n : ℕ} (x y : R) :
+  (x - y) ^ (p ^ n) = x ^ (p ^ n) - y ^ (p ^ n) :=
+sub_pow_char_pow_of_commute _ _ _ (commute.all _ _)
+
 lemma eq_iff_modeq_int (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
   (a : R) = b ↔ a ≡ b [ZMOD p] :=
 by rw [eq_comm, ←sub_eq_zero, ←int.cast_sub,
@@ -129,12 +165,18 @@ def frobenius : R →+* R :=
   map_one' := one_pow p,
   map_mul' := λ x y, mul_pow x y p,
   map_zero' := zero_pow (lt_trans zero_lt_one ‹nat.prime p›.one_lt),
-  map_add' := add_pow_char R ‹nat.prime p› }
+  map_add' := add_pow_char R }
 
 variable {R}
 
 theorem frobenius_def : frobenius R p x = x ^ p := rfl
 
+theorem iterate_frobenius (n : ℕ) : (frobenius R p)^[n] x = x ^ p ^ n :=
+begin
+  induction n, {simp},
+  rw [function.iterate_succ', nat.pow_succ, pow_mul, function.comp_apply, frobenius_def, n_ih]
+end
+
 theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=
 (frobenius R p).map_mul x y
 

src/data/matrix/basic.lean

@@ -76,6 +76,16 @@ lemma map_add [add_monoid α] {β : Type w} [add_monoid β] (f : α →+ β)
   (M N : matrix m n α) : (M + N).map f = M.map f + N.map f :=
 by { ext, simp, }
 
+lemma map_sub [add_group α] {β : Type w} [add_group β] (f : α →+ β)
+  (M N : matrix m n α) : (M - N).map f = M.map f - N.map f :=
+by { ext, simp }
+
+lemma subsingleton_of_empty_left (hm : ¬ nonempty m) : subsingleton (matrix m n α) :=
+⟨λ M N, by { ext, contrapose! hm, use i }⟩
+
+lemma subsingleton_of_empty_right (hn : ¬ nonempty n) : subsingleton (matrix m n α) :=
+⟨λ M N, by { ext, contrapose! hn, use j }⟩
+
 end matrix
 
 /-- The `add_monoid_hom` between spaces of matrices induced by an `add_monoid_hom` between their
@@ -446,6 +456,15 @@ lemma scalar_apply_ne (a : α) (i j : n) (h : i ≠ j) :
   scalar n a i j = 0 :=
 by simp only [h, coe_scalar, one_apply_ne, ne.def, not_false_iff, smul_apply, mul_zero]
 
+lemma scalar_inj [nonempty n] {r s : α} : scalar n r = scalar n s ↔ r = s :=
+begin
+  split,
+  { intro h,
+    inhabit n,
+    rw [← scalar_apply_eq r (arbitrary n), ← scalar_apply_eq s (arbitrary n), h] },
+  { rintro rfl, refl }
+end
+
 end scalar
 
 end semiring

src/data/matrix/char_p.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2020 Aaron Anderson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Anderson
+-/
+import data.matrix.basic
+import algebra.char_p
+/-!
+# Matrices in prime characteristic
+-/
+
+open matrix
+variables {n : Type*} [fintype n] {R : Type*} [ring R]
+
+instance matrix.char_p [decidable_eq n] [nonempty n] (p : ℕ) [char_p R p] :
+  char_p (matrix n n R) p :=
+⟨begin
+  intro k,
+  rw [← char_p.cast_eq_zero_iff R p k, ← nat.cast_zero, ← (scalar n).map_nat_cast],
+  convert scalar_inj,
+  simpa
+ end⟩

src/data/polynomial/basic.lean

@@ -64,10 +64,7 @@ def X : polynomial R := monomial 1 1
 
 /-- `X` commutes with everything, even when the coefficients are noncommutative. -/
 lemma X_mul : X * p = p * X :=
-begin
-  ext,
-  simp [X, monomial, add_monoid_algebra.mul_apply, sum_single_index, add_comm],
-end
+by { ext, simp [X, monomial, add_monoid_algebra.mul_apply, sum_single_index, add_comm] }
 
 lemma X_pow_mul {n : ℕ} : X^n * p = p * X^n :=
 begin
@@ -80,6 +77,8 @@ end
 lemma X_pow_mul_assoc {n : ℕ} : (p * X^n) * q = (p * q) * X^n :=
 by rw [mul_assoc, X_pow_mul, ←mul_assoc]
 
+lemma commute_X (p : polynomial R) : commute X p := X_mul
+
 /-- coeff p n is the coefficient of X^n in p -/
 def coeff (p : polynomial R) := p.to_fun
 

src/field_theory/finite.lean

@@ -8,6 +8,7 @@ import data.equiv.ring
 import data.zmod.basic
 import linear_algebra.basis
 import ring_theory.integral_domain
+import field_theory.separable
 
 /-!
 # Finite fields
@@ -110,12 +111,19 @@ begin
       this, mul_one]
 end
 
-lemma pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) :
-  a ^ (fintype.card K - 1) = 1 :=
+lemma pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) : a ^ (q - 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 pow_card (a : K) : a ^ q = a :=
+begin
+  have hp : fintype.card K > 0 := fintype.card_pos_iff.2 (by apply_instance),
+  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
+
 variable (K)
 
 theorem card (p : ℕ) [char_p K p] : ∃ (n : ℕ+), nat.prime p ∧ q = p^(n : ℕ) :=
@@ -202,6 +210,28 @@ begin
     ... = 0 : by { rw [sum_pow_units K i, if_neg], exact hiq, }
 end
 
+variables {K}
+
+theorem frobenius_pow {p : ℕ} [fact p.prime] [char_p K p] {n : ℕ} (hcard : q = p^n) :
+  (frobenius K p) ^ n = 1 :=
+begin
+  ext, conv_rhs { rw [ring_hom.one_def, ring_hom.id_apply, ← pow_card x, hcard], }, clear hcard,
+  induction n, {simp},
+  rw [pow_succ, nat.pow_succ, pow_mul, ring_hom.mul_def, ring_hom.comp_apply, frobenius_def, n_ih]
+end
+
+open polynomial
+
+lemma expand_card (f : polynomial K) :
+  expand K q f = f ^ q :=
+begin
+  cases char_p.exists K with p hp, letI := hp,
+  rcases finite_field.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩, letI : fact p.prime := hp,
+  dsimp at hn, rw hn at *,
+  rw ← map_expand_pow_char,
+  rw [frobenius_pow hn, ring_hom.one_def, map_id],
+end
+
 end finite_field
 
 namespace zmod
@@ -258,3 +288,31 @@ begin
   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
+
+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 card_units (p : ℕ) [fact p.prime] : fintype.card (units (zmod p)) = p - 1 :=
+by rw [card_units, card]
+
+/-- Fermat's Little Theorem: for every unit `a` of `zmod p`, we have `a ^ (p - 1) = 1`. -/
+theorem units_pow_card_sub_one_eq_one (p : ℕ) [fact p.prime] (a : units (zmod p)) :
+  a ^ (p - 1) = 1 :=
+by rw [← card_units p, pow_card_eq_one]
+
+/-- Fermat's Little Theorem: for all nonzero `a : zmod p`, we have `a ^ (p - 1) = 1`. -/
+theorem pow_card_sub_one_eq_one {p : ℕ} [fact p.prime] {a : zmod p} (ha : a ≠ 0) :
+  a ^ (p - 1) = 1 :=
+by { have h := pow_card_sub_one_eq_one a ha, rwa zmod.card p at h }
+
+open polynomial
+
+lemma expand_card {p : ℕ} [fact p.prime] (f : polynomial (zmod p)) :
+  expand (zmod p) p f = f ^ p :=
+by { have h := finite_field.expand_card f, rwa zmod.card p at h }
+
+end zmod

src/field_theory/separable.lean

@@ -191,6 +191,10 @@ begin
     rw [coeff_expand_mul hp, ← leading_coeff], exact mt leading_coeff_eq_zero.1 hf }
 end
 
+theorem map_expand {p : ℕ} (hp : 0 < p) {f : R →+* S} {q : polynomial R} :
+  map f (expand R p q) = expand S p (map f q) :=
+by { ext, rw [coeff_map, coeff_expand hp, coeff_expand hp], split_ifs; simp, }
+
 end comm_semiring
 
 section comm_ring
@@ -302,6 +306,25 @@ ih $ of_irreducible_expand p $ by rwa [expand_expand, mul_comm]
 variables [HF : char_p F p]
 include HF
 
+theorem expand_char (f : polynomial F) :
+  map (frobenius F p) (expand F p f) = f ^ p :=
+begin
+  refine f.induction_on' (λ a b ha hb, _) (λ n a, _),
+  { rw [alg_hom.map_add, map_add, ha, hb, add_pow_char], },
+  { rw [expand_monomial, map_monomial, single_eq_C_mul_X, single_eq_C_mul_X,
+        mul_pow, ← C.map_pow, frobenius_def],
+    ring_exp }
+end
+
+theorem map_expand_pow_char (f : polynomial F) (n : ℕ) :
+   map ((frobenius F p) ^ n) (expand F (p ^ n) f) = f ^ (p ^ n) :=
+begin
+  induction n, {simp [ring_hom.one_def]},
+  symmetry,
+  rw [nat.pow_succ, pow_mul, ← n_ih, ← expand_char, pow_succ, ring_hom.mul_def, ← map_map, mul_comm,
+      expand_mul, ← map_expand (nat.prime.pos hp)],
+end
+
 theorem expand_contract {f : polynomial F} (hf : f.derivative = 0) :
   expand F p (contract p f) = f :=
 begin

src/linear_algebra/char_poly/coeff.lean

@@ -4,11 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Aaron Anderson, Jalex Stark.
 -/
 
+import data.matrix.char_p
 import linear_algebra.char_poly
 import linear_algebra.matrix
 import ring_theory.polynomial.basic
 import algebra.polynomial.big_operators
 import group_theory.perm.cycles
+import field_theory.finite
 
 /-!
 # Characteristic polynomials
@@ -160,3 +162,44 @@ begin
   rw [coeff_zero_eq_eval_zero, char_poly, eval_det, mat_poly_equiv_char_matrix, ← det_smul],
   simp
 end
+
+variables {p : ℕ} [fact p.prime]
+
+@[simp] lemma finite_field.char_poly_pow_card {K : Type*} [field K] [fintype K] (M : matrix n n K) :
+  char_poly (M ^ (fintype.card K)) = char_poly M :=
+begin
+  by_cases hn : nonempty n,
+  { letI := hn,
+    cases char_p.exists K with p hp, letI := hp,
+    rcases finite_field.card K p with ⟨⟨k, kpos⟩, ⟨hp, hk⟩⟩,
+    letI : fact p.prime := hp,
+    dsimp at hk, rw hk at *,
+    apply (frobenius_inj (polynomial K) p).iterate k,
+    repeat { rw iterate_frobenius, rw ← hk },
+    rw ← finite_field.expand_card,
+    unfold char_poly, rw [alg_hom.map_det, ← is_monoid_hom.map_pow],
+    apply congr_arg det,
+    apply mat_poly_equiv.injective, swap, { apply_instance },
+    rw [← mat_poly_equiv.coe_alg_hom, alg_hom.map_pow, mat_poly_equiv.coe_alg_hom,
+          mat_poly_equiv_char_matrix, hk, sub_pow_char_pow_of_commute, ← C_pow],
+    swap, { apply polynomial.commute_X },
+    -- the following is a nasty case bash that should be abstracted as a lemma
+    -- (and maybe it can be proven more... algebraically?)
+    ext, rw [coeff_sub, coeff_C],
+    by_cases hij : i = j; simp [char_matrix, hij, coeff_X_pow];
+    simp only [coeff_C]; split_ifs; simp *, },
+  { congr, apply @subsingleton.elim _ (subsingleton_of_empty_left hn) _ _, },
+end
+
+@[simp] lemma zmod.char_poly_pow_card (M : matrix n n (zmod p)) :
+  char_poly (M ^ p) = char_poly M :=
+by { have h := finite_field.char_poly_pow_card M, rwa zmod.card at h, }
+
+lemma finite_field.trace_pow_card {K : Type*} [field K] [fintype K] [nonempty n] (M : matrix n n K) :
+  trace n K K (M ^ (fintype.card K)) = (trace n K K M) ^ (fintype.card K) :=
+by rw [trace_eq_neg_char_poly_coeff, trace_eq_neg_char_poly_coeff,
+       finite_field.char_poly_pow_card, finite_field.pow_card]
+
+lemma zmod.trace_pow_card {p:ℕ} [fact p.prime] [nonempty n] (M : matrix n n (zmod p)) :
+  trace n (zmod p) (zmod p) (M ^ p) = (trace n (zmod p) (zmod p) M)^p :=
+by { have h := finite_field.trace_pow_card M, rwa zmod.card at h, }