feat: nilpotent matrices have nilpotent trace (#6588)

Also some related results
    
Co-authored-by: damiano <adomani@gmail.com>

Mathlib/Algebra/GeomSum.lean

@@ -189,10 +189,24 @@ theorem geom_sum₂_mul [CommRing α] (x y : α) (n : ℕ) :
   (Commute.all x y).geom_sum₂_mul n
 #align geom_sum₂_mul geom_sum₂_mul
 
+theorem Commute.sub_dvd_pow_sub_pow [Ring α] {x y : α} (h : Commute x y) (n : ℕ) :
+    x - y ∣ x ^ n - y ^ n :=
+  Dvd.intro _ $ h.mul_geom_sum₂ _
+
 theorem sub_dvd_pow_sub_pow [CommRing α] (x y : α) (n : ℕ) : x - y ∣ x ^ n - y ^ n :=
-  Dvd.intro_left _ (geom_sum₂_mul x y n)
+  (Commute.all x y).sub_dvd_pow_sub_pow n
 #align sub_dvd_pow_sub_pow sub_dvd_pow_sub_pow
 
+theorem one_sub_dvd_one_sub_pow [Ring α] (x : α) (n : ℕ) :
+    1 - x ∣ 1 - x ^ n := by
+  conv_rhs => rw [← one_pow n]
+  exact (Commute.one_left x).sub_dvd_pow_sub_pow n
+
+theorem sub_one_dvd_pow_sub_one [Ring α] (x : α) (n : ℕ) :
+    x - 1 ∣ x ^ n - 1 := by
+  conv_rhs => rw [← one_pow n]
+  exact (Commute.one_right x).sub_dvd_pow_sub_pow n
+
 theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n := by
   cases' le_or_lt y x with h h
   · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _

Mathlib/Data/Fintype/Card.lean

@@ -549,6 +549,7 @@ theorem card_pos [h : Nonempty α] : 0 < card α :=
   card_pos_iff.mpr h
 #align fintype.card_pos Fintype.card_pos
 
+@[simp]
 theorem card_ne_zero [Nonempty α] : card α ≠ 0 :=
   _root_.ne_of_gt card_pos
 #align fintype.card_ne_zero Fintype.card_ne_zero

Mathlib/Data/Polynomial/Basic.lean

@@ -682,10 +682,14 @@ theorem coeff_zero (n : ℕ) : coeff (0 : R[X]) n = 0 :=
   rfl
 #align polynomial.coeff_zero Polynomial.coeff_zero
 
+theorem coeff_one {n : ℕ} : coeff (1 : R[X]) n = if n = 0 then 1 else 0 := by
+  simp_rw [eq_comm (a := n) (b := 0)]
+  exact coeff_monomial
+#align polynomial.coeff_one Polynomial.coeff_one
+
 @[simp]
 theorem coeff_one_zero : coeff (1 : R[X]) 0 = 1 := by
-  rw [← monomial_zero_one, coeff_monomial]
-  simp
+  simp [coeff_one]
 #align polynomial.coeff_one_zero Polynomial.coeff_one_zero
 
 @[simp]

Mathlib/Data/Polynomial/Coeff.lean

@@ -37,10 +37,6 @@ variable [Semiring R] {p q r : R[X]}
 
 section Coeff
 
-theorem coeff_one (n : ℕ) : coeff (1 : R[X]) n = if 0 = n then 1 else 0 :=
-  coeff_monomial
-#align polynomial.coeff_one Polynomial.coeff_one
-
 @[simp]
 theorem coeff_add (p q : R[X]) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n := by
   rcases p with ⟨⟩

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark
 -/
 import Mathlib.Data.Polynomial.Expand
-import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
 import Mathlib.Data.Polynomial.Laurent
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
+import Mathlib.RingTheory.Polynomial.Nilpotent
 
 #align_import linear_algebra.matrix.charpoly.coeff from "leanprover-community/mathlib"@"9745b093210e9dac443af24da9dba0f9e2b6c912"
 
@@ -23,6 +24,7 @@ We give methods for computing coefficients of the characteristic polynomial.
 - `Matrix.trace_eq_neg_charpoly_coeff` proves that the trace is the negative of the (d-1)th
   coefficient of the characteristic polynomial, where d is the dimension of the matrix.
   For a nonzero ring, this is the second-highest coefficient.
+- `Matrix.charpolyRev` the reverse of the characteristic polynomial.
 - `Matrix.reverse_charpoly` characterises the reverse of the characteristic polynomial.
 
 -/
@@ -124,7 +126,7 @@ theorem charpoly_degree_eq_dim [Nontrivial R] (M : Matrix n n R) :
   apply h
 #align matrix.charpoly_degree_eq_dim Matrix.charpoly_degree_eq_dim
 
-theorem charpoly_natDegree_eq_dim [Nontrivial R] (M : Matrix n n R) :
+@[simp] theorem charpoly_natDegree_eq_dim [Nontrivial R] (M : Matrix n n R) :
     M.charpoly.natDegree = Fintype.card n :=
   natDegree_eq_of_degree_eq_some (charpoly_degree_eq_dim M)
 #align matrix.charpoly_nat_degree_eq_dim Matrix.charpoly_natDegree_eq_dim
@@ -151,6 +153,7 @@ theorem charpoly_monic (M : Matrix n n R) : M.charpoly.Monic := by
   apply h
 #align matrix.charpoly_monic Matrix.charpoly_monic
 
+/-- See also `Matrix.coeff_charpolyRev_eq_neg_trace`. -/
 theorem trace_eq_neg_charpoly_coeff [Nonempty n] (M : Matrix n n R) :
     trace M = -M.charpoly.coeff (Fintype.card n - 1) := by
   rw [charpoly_coeff_eq_prod_coeff_of_le _ le_rfl, Fintype.card,
@@ -262,28 +265,32 @@ theorem coeff_charpoly_mem_ideal_pow {I : Ideal R} (h : ∀ i j, M i j ∈ I) (k
 
 end Ideal
 
+namespace Matrix
+
 section reverse
 
 open Polynomial
 open LaurentPolynomial hiding C
 
-/-- The right hand side of the equality in this lemma statement is sometimes called the
-"characteristic power series" of a matrix.
+/-- The reverse of the characteristic polynomial of a matrix.
 
 It has some advantages over the characteristic polynomial, including the fact that it can be
-extended to infinite dimensions (for appropriate operators). -/
-lemma Matrix.reverse_charpoly (M : Matrix n n R) :
-    M.charpoly.reverse = det (1 - (X : R[X]) • C.mapMatrix M) := by
+extended to infinite dimensions (for appropriate operators). In such settings it is known as the
+"characteristic power series". -/
+def charpolyRev (M : Matrix n n R) : R[X] := det (1 - (X : R[X]) • M.map C)
+
+lemma reverse_charpoly (M : Matrix n n R) :
+    M.charpoly.reverse = M.charpolyRev := by
   nontriviality R
   let t : R[T;T⁻¹] := T 1
   let t_inv : R[T;T⁻¹] := T (-1)
-  let p : R[T;T⁻¹] := det (scalar n t - LaurentPolynomial.C.mapMatrix M)
-  let q : R[T;T⁻¹] := det (1 - scalar n t * LaurentPolynomial.C.mapMatrix M)
+  let p : R[T;T⁻¹] := det (scalar n t - M.map LaurentPolynomial.C)
+  let q : R[T;T⁻¹] := det (1 - scalar n t * M.map LaurentPolynomial.C)
   have ht : t_inv * t = 1 := by rw [← T_add, add_left_neg, T_zero]
   have hp : toLaurentAlg M.charpoly = p := by
     simp [charpoly, charmatrix, AlgHom.map_det, map_sub, map_smul']
-  have hq : toLaurentAlg (det (1 - (X : R[X]) • C.mapMatrix M)) = q := by
-    simp [AlgHom.map_det, map_sub, map_smul']
+  have hq : toLaurentAlg M.charpolyRev = q := by
+    simp [charpolyRev, AlgHom.map_det, map_sub, map_smul']
   suffices : t_inv ^ Fintype.card n * p = invert q
   · apply toLaurent_injective
     rwa [toLaurent_reverse, ← coe_toLaurentAlg, hp, hq, ← involutive_invert.injective.eq_iff,
@@ -292,4 +299,50 @@ lemma Matrix.reverse_charpoly (M : Matrix n n R) :
   rw [← det_smul, smul_sub, coe_scalar, ← smul_assoc, smul_eq_mul, ht, one_smul, invert.map_det]
   simp [map_smul']
 
+@[simp] lemma eval_charpolyRev :
+    eval 0 M.charpolyRev = 1 := by
+  rw [charpolyRev, ← coe_evalRingHom, RingHom.map_det, ← det_one (R := R) (n := n)]
+  have : (1 - (X : R[X]) • M.map C).map (eval 0) = 1 := by
+    ext i j; cases' eq_or_ne i j with hij hij <;> simp [hij]
+  congr
+
+@[simp] lemma coeff_charpolyRev_eq_neg_trace (M : Matrix n n R) :
+    coeff M.charpolyRev 1 = - trace M := by
+  nontriviality R
+  cases isEmpty_or_nonempty n; simp [charpolyRev, coeff_one]
+  simp [trace_eq_neg_charpoly_coeff M, ← M.reverse_charpoly, nextCoeff]
+
+lemma isUnit_charpolyRev_of_IsNilpotent (hM : IsNilpotent M) :
+    IsUnit M.charpolyRev := by
+  obtain ⟨k, hk⟩ := hM
+  replace hk : 1 - (X : R[X]) • M.map C ∣ 1 := by
+    convert one_sub_dvd_one_sub_pow ((X : R[X]) • M.map C) k
+    rw [← C.mapMatrix_apply, smul_pow, ← map_pow, hk, map_zero, smul_zero, sub_zero]
+  apply isUnit_of_dvd_one
+  rw [← det_one (R := R[X]) (n := n)]
+  exact map_dvd detMonoidHom hk
+
+lemma isNilpotent_trace_of_isNilpotent (hM : IsNilpotent M) :
+    IsNilpotent (trace M) := by
+  cases isEmpty_or_nonempty n; simp
+  suffices IsNilpotent (coeff (charpolyRev M) 1) by simpa using this
+  exact (isUnit_iff_coeff_isUnit_isNilpotent.mp (isUnit_charpolyRev_of_IsNilpotent hM)).2
+    _ one_ne_zero
+
+lemma isNilpotent_charpoly_sub_pow_of_isNilpotent (hM : IsNilpotent M) :
+    IsNilpotent (M.charpoly - X ^ (Fintype.card n)) := by
+  nontriviality R
+  let p : R[X] := M.charpolyRev
+  have hp : p - 1 = X * (p /ₘ X) := by
+    conv_lhs => rw [← modByMonic_add_div p monic_X]
+    simp [modByMonic_X]
+  have : IsNilpotent (p /ₘ X) :=
+    (Polynomial.isUnit_iff'.mp (isUnit_charpolyRev_of_IsNilpotent hM)).2
+  have aux : (M.charpoly - X ^ (Fintype.card n)).natDegree ≤ M.charpoly.natDegree :=
+    le_trans (natDegree_sub_le _ _) (by simp)
+  rw [← isNilpotent_reflect_iff aux, reflect_sub, ← reverse, M.reverse_charpoly]
+  simpa [hp]
+
 end reverse
+
+end Matrix

Mathlib/LinearAlgebra/Matrix/Charpoly/FiniteField.lean

@@ -53,7 +53,7 @@ theorem ZMod.charpoly_pow_card {p : ℕ} [Fact p.Prime] (M : Matrix n n (ZMod p)
 theorem FiniteField.trace_pow_card {K : Type*} [Field K] [Fintype K] (M : Matrix n n K) :
     trace (M ^ Fintype.card K) = trace M ^ Fintype.card K := by
   cases isEmpty_or_nonempty n
-  · simp [Matrix.trace]; rw [zero_pow Fintype.card_pos]
+  · simp [Matrix.trace]
   rw [Matrix.trace_eq_neg_charpoly_coeff, Matrix.trace_eq_neg_charpoly_coeff,
     FiniteField.Matrix.charpoly_pow_card, FiniteField.pow_card]
 #align finite_field.trace_pow_card FiniteField.trace_pow_card

Mathlib/LinearAlgebra/Matrix/Trace.lean

@@ -51,6 +51,9 @@ theorem trace_zero : trace (0 : Matrix n n R) = 0 :=
 
 variable {n R}
 
+@[simp]
+lemma trace_eq_zero_of_isEmpty [IsEmpty n] (A : Matrix n n R) : trace A = 0 := by simp [trace]
+
 @[simp]
 theorem trace_add (A B : Matrix n n R) : trace (A + B) = trace A + trace B :=
   Finset.sum_add_distrib
@@ -183,7 +186,6 @@ with `Matrix.det_fin_two` etc.
 -/
 
 
-@[simp]
 theorem trace_fin_zero (A : Matrix (Fin 0) (Fin 0) R) : trace A = 0 :=
   rfl
 #align matrix.trace_fin_zero Matrix.trace_fin_zero

Mathlib/RingTheory/Polynomial/Nilpotent.lean

@@ -79,14 +79,18 @@ protected lemma isNilpotent_iff :
   · cases' i with i; simp
     simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i
 
-@[simp] lemma isNilpotent_reverse_iff :
-    IsNilpotent P.reverse ↔ IsNilpotent P := by
+@[simp] lemma isNilpotent_reflect_iff {P : R[X]} {N : ℕ} (hN : P.natDegree ≤ N):
+    IsNilpotent (reflect N P) ↔ IsNilpotent P := by
   simp only [Polynomial.isNilpotent_iff, coeff_reverse]
-  refine' ⟨fun h i ↦ _, fun h i ↦ _⟩ <;> cases' le_or_lt i P.natDegree with hi hi
-  · simpa [tsub_tsub_cancel_of_le hi] using h (P.natDegree - i)
-  · simp [coeff_eq_zero_of_natDegree_lt hi]
-  · simpa only [hi, revAt_le] using h (P.natDegree - i)
-  · simpa only [revAt_eq_self_of_lt hi] using h i
+  refine' ⟨fun h i ↦ _, fun h i ↦ _⟩ <;> cases' le_or_lt i N with hi hi
+  · simpa [tsub_tsub_cancel_of_le hi] using h (N - i)
+  · simp [coeff_eq_zero_of_natDegree_lt $ lt_of_le_of_lt hN hi]
+  · simpa [hi, revAt_le] using h (N - i)
+  · simpa [revAt_eq_self_of_lt hi] using h i
+
+@[simp] lemma isNilpotent_reverse_iff :
+    IsNilpotent P.reverse ↔ IsNilpotent P :=
+  isNilpotent_reflect_iff (le_refl _)
 
 /-- Let `P` be a polynomial over `R`. If its constant term is a unit and its other coefficients are
 nilpotent, then `P` is a unit.

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -1807,17 +1807,12 @@ theorem trunc_zero (n) : trunc n (0 : PowerSeries R) = 0 :=
 @[simp]
 theorem trunc_one (n) : trunc (n + 1) (1 : PowerSeries R) = 1 :=
   Polynomial.ext fun m => by
-    rw [coeff_trunc, coeff_one]
-    split_ifs with H H' <;> rw [Polynomial.coeff_one]
-    · subst m
-      rw [if_pos rfl]
-    · symm
-      exact if_neg (Ne.elim (Ne.symm H'))
-    · symm
-      refine' if_neg _
-      rintro rfl
-      apply H
-      exact Nat.zero_lt_succ _
+    rw [coeff_trunc, coeff_one, Polynomial.coeff_one]
+    split_ifs with h _ h'
+    · rfl
+    · rfl
+    · subst h'; simp at h
+    · rfl
 #align power_series.trunc_one PowerSeries.trunc_one
 
 @[simp]

test/ComputeDegree.lean

@@ -60,7 +60,7 @@ example [Ring R] : coeff (1 : R[X]) 0 = 1 := by compute_degree!
 
 example [Ring R] : coeff (1 : R[X]) 2 = 0 := by compute_degree!
 
-example [Ring R] : coeff (1 : R[X]) n = if 0 = n then 1 else 0 := by compute_degree!
+example [Ring R] : coeff (1 : R[X]) n = if n = 0 then 1 else 0 := by compute_degree!
 
 example [Ring R] (h : (0 : R) = 6) : coeff (1 : R[X]) 1 = 6 := by compute_degree!