[Merged by Bors] - feat(linear_algebra/char_poly/coeff,*): prerequisites for friendship theorem

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,22 @@ 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 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,
+  have h' : commute (x - y) y, rw [commute, semiconj_by, sub_mul, mul_sub, h.eq],
+  rw [eq_sub_iff_add_eq, ← add_pow_char_of_commute _ _ _ h'], simp, repeat {apply_instance},
 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 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 _ _)
+
 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,7 +137,7 @@ 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}
 

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,10 @@ 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 :=
+⟨λ h, by { inhabit n, rw [← scalar_apply_eq r (arbitrary n), ← scalar_apply_eq s (arbitrary n), h] },
+  by rintro rfl; refl⟩
+
 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 :=
+{ cast_eq_zero_iff :=
+  begin
+    intro k, rw ← char_p.cast_eq_zero_iff R p k,
+    rw ← nat.cast_zero, rw ← (scalar n).map_nat_cast,
+    convert scalar_inj, simp, assumption,
+  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 := by rw [commute, semiconj_by, 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 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 : ℕ) :=
@@ -258,3 +266,17 @@ 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
+
+/-- A variation on Fermat's little theorem. See `zmod.fermat_little` -/
+@[simp] lemma zmod.pow_card {p : ℕ} [fact p.prime] (x : zmod p) : x ^ p = x :=
+by { have h := finite_field.pow_card x, rw zmod.card p at h, rw h }
+
+open polynomial
+
+lemma zmod.expand_p {p : ℕ} [fact p.prime] (f : polynomial (zmod p)) :
+  expand (zmod p) p f = f ^ p :=
+begin
+  apply f.induction_on', intros a b ha hb, rw add_pow_char, simp [ha, hb],
+  intros n a, rw polynomial.expand_monomial, repeat {rw single_eq_C_mul_X},
+  rw [mul_pow, ← C.map_pow, zmod.pow_card a], ring_exp,
+end

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.basic
 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,35 @@ 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]
+
+lemma zmod.char_poly_pow_card_of_nonempty [nonempty n] (M : matrix n n (zmod p)) :
+  char_poly (M ^ p) = char_poly M :=
+begin
+  apply frobenius_inj (polynomial (zmod p)) p, repeat {rw frobenius_def},
+  rw ← zmod.expand_p,
+  unfold char_poly, rw [alg_hom.map_det, ← det_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, sub_pow_char_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 *,
+end
+
+lemma zmod.char_poly_pow_card (M : matrix n n (zmod p)) :
+  char_poly (M ^ p) = char_poly M :=
+begin
+  classical,
+  by_cases hn : nonempty n, letI := hn, apply zmod.char_poly_pow_card_of_nonempty,
+  swap, { congr, apply @subsingleton.elim _ (subsingleton_of_empty_left hn) _ _, },
+end
+
+lemma zmod.trace_pow_p {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 rw [trace_eq_neg_char_poly_coeff, trace_eq_neg_char_poly_coeff,
+  zmod.char_poly_pow_card, zmod.pow_card]

src/linear_algebra/determinant.lean

@@ -102,6 +102,9 @@ instance : is_monoid_hom (det : matrix n n R → R) :=
 { map_one := det_one,
   map_mul := det_mul }
 
+lemma det_pow (k : ℕ) (M : matrix n n R) : (M ^ k).det = (M.det) ^ k :=
+by induction k; simp [pow_succ, *]
+
 /-- Transposing a matrix preserves the determinant. -/
 @[simp] lemma det_transpose (M : matrix n n R) : Mᵀ.det = M.det :=
 begin