Nilpotent implies trace zero

Stream: Is there code for X?

[Oliver Nash]

I don't suppose anyone has a proof of this lying around:

import Mathlib.RingTheory.Nilpotent
import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
import Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
import Mathlib.LinearAlgebra.Trace

-- Fairly sure `IsReduced` suffices (at least in commutative case) but I'll settle for a proof
-- over a field.
lemma Matrix.trace_eq_zero_of_isNilpotent
    (R : Type _) [CommRing R] [IsReduced R] {ι : Type _} [DecidableEq ι] [Fintype ι]
    {A : Matrix ι ι R} (h : IsNilpotent A) : A.trace = 0 := by
  sorry

The informal proofs I know actually require stronger assumptions on R but I expect the above is true.

[Antoine Chambert-Loir]

(Reduced is necessary, as the case of a 1x1 matrix shows.)

[Antoine Chambert-Loir]

(It also suffices: then the intersection of all prime ideals P is zero, it suffices to check mod such P, but R/P is a domain, hence we're back to the classic case of fields. )

[Antoine Chambert-Loir]

(The case of a companion matrix is already nice: if P is a monic polynomial and M is the corresponding companion matrix, then M is nilpotent iff there exists n such that P divides X^n. Write X^n=P·Q and consider the reverted polynomials P*=P(1/X) X^p, Q*=Q(1/X) X^q, with p, q the degrees of P, Q and n=p+q. Then 1=P· Q. Then all coefficients of P* are nilpotent, but the constant one which is 1. On a reduced ring, you get P=X^p.)

[Antoine Chambert-Loir]

(Unfortunately, I know his to use this over fields to get the result you need, but not directly over a reduced field)

[Damiano Testa]

I wonder if you could use docs#Polynomial.isUnit_iff to show that all the coefficients of the characteristic polynomial of a nilpotent matrix are nilpotent, except for the leading one.

This would probably make the assumption IsReduced only appear when you go from "trace is nilpotent" to "trace is zero".

[Riccardo Brasca]

I guess you mean docs#Polynomial.isUnit_iff_coeff_isUnit_isNilpotent

[Damiano Testa]

Yes, that is probably a better form! Btw, I do not know that the characteristic polynomial $\chi$ of a nilpotent matrix satisfies $\chi ^ N = X ^ M$, for some $N > 0$. However, if true, then it would be a fun fact that I learn thanks to Lean!

[Riccardo Brasca]

Hmm, indeed over a general ring looks like a nontrivial question

[Damiano Testa]

Maybe you could still argue "the wrong way": quotient by the radical of the ring, do the reduction to domains, deduce that the characteristic polynomial is $X^M$ up to radical and conclude.

My hope was that there might be a direct way to argue this, without doing the various reduction steps. :shrug:

[Arend Mellendijk]

Damiano Testa said:

Yes, that is probably a better form! Btw, I do not know that the characteristic polynomial $\chi$ of a nilpotent matrix satisfies $\chi ^ N = X ^ M$, for some $N > 0$. However, if true, then it would be a fun fact that I learn thanks to Lean!

This could only hold for R reduced, right? Consider $R=\mathbb{Q}[\epsilon]/(\epsilon^2)$ with 1x1 matrix $\epsilon$. Then $\chi^N=X^N-N\epsilon X^{N-1}$.

[Damiano Testa]

Arend, yes, that statement is not true. I still wonder whether the statement that the characteristic polynomial has all its coefficients nilpotent, except for the leading one.

[Damiano Testa]

How about this?

Start with $I = I - (tA)^{N+1} = (I - tA)(I + tA + \cdots + (tA)^N)$.

Compute determinants on both sides and use that the determinant of a product is the product of the determinants.

Deduce that the determinant of $(I - tA)$ is an invertible polynomial. Therefore all its coefficients of positive degree are nilpotents.

Is this right? If only I had a proof assistant at hand...

[Antoine Chambert-Loir]

Riccardo Brasca said:

Hmm, indeed over a general ring looks like a nontrivial question

Over a general ring, it is true. If $a$ is a nilpotent element, then the characteristic polynomial of the matrix $[a]$ is $T - a$.
It holds over a reduced ring by the arguments I gave above.

[Antoine Chambert-Loir]

Damiano Testa said:

How about this?

Start with $I = I - (tA)^{N+1} = (I - tA)(I + tA + \cdots + (tA)^N)$.

Compute determinants on both sides and use that the determinant of a product is the product of the determinants.

Deduce that the determinant of $(I - tA)$ is an invertible polynomial. Therefore all its coefficients of positive degree are nilpotents.

Is this right? If only I had a proof assistant at hand...

This is a cool proof.

[Antoine Chambert-Loir]

Thanks to the work of Riccardo's students, that should make a nice proof in mathlib.

[Antoine Chambert-Loir]

On the other hand, proving that if a polynomial $P$ is a unit then its constant coefficient is a unit and all other are nilpotents can be done right away once one has the characterization of nilpotent elements: mod out a prime ideal $p$, the polynomial $P$ is a unit, but since $R / p$ is a domain, this implies that $P$ has degree $0$ mod $p$, so all of its nonconstant coefficients belong to $p$. Then all nonconstant coefficients of $P$ are nilpotent.

[Damiano Testa]

I agree: the hardest part is the fact about invertible polynomials, which I find is a very elegant result.

[Damiano Testa]

I couldn't help myself and I formalized the proof that, for a nilpotent matrix, the "revcharpoly" is a unit!

The proof is simply a transliteration of the proof above: I have made no effort to simplify it.

import Mathlib.Data.Polynomial.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant

--  I could only find the commutative version of this lemma, though it likely is already in mathlib
theorem _root_.Commute.sub_dvd_pow_dvd_pow_of [Ring R] {a b : R} (h : Commute a b) {n : ℕ} :
    a - b ∣ a ^ n - b ^ n :=
Dvd.intro _ (h.mul_geom_sum₂ _)

variable {R : Type u} [CommRing R]

variable {n : Type v} [DecidableEq n] [Fintype n]

namespace Matrix

open Polynomial

variable (M : Matrix n n R)

noncomputable section

def revcharmatrix : Matrix n n R[X] :=
  1 - Matrix.scalar n (X : R[X]) * (C : R →+* R[X]).mapMatrix M

def revcharpoly : R[X] := det (revcharmatrix M)

--  why did I not find this lemma already?
theorem map_pow (N : ℕ) : map (M ^ N) C = map M C ^ N := by
  induction N with
    | zero => simp
    | succ N => simp [pow_succ, *]

theorem IsUnit_revcharpoly_of_IsNilpotent (hM : IsNilpotent M) : IsUnit (revcharpoly M) := by
  rcases hM with ⟨N, hM⟩
  apply isUnit_of_dvd_one
  have : 1 = 1 - (scalar n (X : R[X]) * (C : R →+* R[X]).mapMatrix M) ^ N := by
    simp [← map_pow, hM, smul_pow]
  apply_fun det at this
  rw [det_one] at this
  rw [this]
  obtain ⟨A, h⟩ : revcharmatrix M ∣ 1 - ((scalar n) X * (RingHom.mapMatrix C) M) ^ N := by
    rw [← one_pow N]
    exact Commute.sub_dvd_pow_dvd_pow_of (by simp)
  rw [h]
  simp [revcharpoly, revcharmatrix]

end

end Matrix

[Damiano Testa]

To get the statement that Oliver wants, one possible strategy would be to connect revcharpoly and charpoly (probably via docs#Polynomial.reverse) and finally that the trace of a matrix is a coefficient (I think that this is docs#Matrix.trace_eq_neg_charpoly_coeff).

[Oliver Nash]

I've been travelling for most of the last two days so I'm only properly catching up with this thread now. I'm amazed how fruitful this nerd sniping effort turned out to be, and also extremely grateful especially to @Antoine Chambert-Loir and @Damiano Testa . I'll PR a proof of this next week unless someone beats me to it.

[Oliver Nash]

I only care about the commutative case but of course there's still the non-commutative case: there's no characteristic polynomial but there is still a trace! I wonder what's true there?

[Antoine Chambert-Loir]

It seems it works. https://arxiv.org/abs/2002.01538

[Damiano Testa]

I just realized that the argument above can be split as

• the sum of a unit and a nilpotent element that commute is a unit (docs#Commute.IsNilpotent.add_isUnit);
• the image under a multiplicative homomorphism of a unit is a unit (docs#IsUnit.map).

This may shorten the proof quite a bit.

[Damiano Testa]

Trying to simplify the above, I ran into this issue.

import Mathlib.RingTheory.Nilpotent
import Mathlib.Data.Matrix.Basic

variable {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S]

variable {n : Type w} [DecidableEq n] [Fintype n]

namespace Matrix

example {M : Matrix n n R} (hM : IsNilpotent M) :
    IsNilpotent ((RingHom.mapMatrix (algebraMap R S)) M) := by
  convert IsNilpotent.map hM ((RingHom.mapMatrix (m := n) (algebraMap R S)))
  -- ⊢ IsNilpotent (↑(RingHom.mapMatrix (algebraMap R S)) M) ↔
  --   IsNilpotent (↑(RingHom.mapMatrix (algebraMap R S)) M)
  sorry
  -- 3 more goals
-- I could not get `apply/refine IsNilpotent.map` to work either

Am I missing something? I do not understand even if an instance is missing or whether I am doing something that is not expected to work.

[Damiano Testa]

I have not gotten there yet, but I am getting closer!

import Mathlib.Data.Polynomial.Laurent
import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

local notation:9000 R "[T;T⁻¹]" => LaurentPolynomial R
universe u

namespace LaurentPolynomial

open Polynomial

variable {R : Type u} [Semiring R] {z : ℤ} {n : ℕ} {f g : R[X]}

theorem T_eq_pow_of_nat : (T n : R[T;T⁻¹]) = (T 1) ^ n := by
  simp only [T_pow, mul_one]

@[simp]
theorem map_add : (toLaurent f + toLaurent g) z = toLaurent f z + toLaurent g z := rfl

theorem toLaurent_apply_eq_coeff : toLaurent f n = f.coeff n := by
  refine f.induction_on' ?_ ?_
  · intros p q hp hq
    simp [← hp, ← hq, toLaurent.map_add]
  · intros m a
    simp only [toLaurent_C_mul_T, ← single_eq_C_mul_T, Finsupp.single_apply, Nat.cast_inj,
      coeff_monomial]

theorem toLaurent_apply_eq_zero_of_neg (h : z < 0) : toLaurent f z = 0 := by
  refine f.induction_on' ?_ ?_
  · intro f g f0 g0
    simp [f0, g0]
  · intros n a
    rw [toLaurent_C_mul_T, ← single_eq_C_mul_T, Finsupp.single_apply_eq_zero]
    rintro rfl
    exfalso
    exact Iff.mp (Int.negSucc_not_nonneg n) h

end LaurentPolynomial

--  I could only find the commutative version of this lemma, though it likely is already in mathlib
theorem _root_.Commute.sub_dvd_pow_dvd_pow_of [Ring R] {a b : R} (h : Commute a b) {n : ℕ} :
    a - b ∣ a ^ n - b ^ n :=
Dvd.intro _ (h.mul_geom_sum₂ _)

variable {R : Type u} [CommRing R] {S : Type w} [CommRing S] [Algebra R S]

variable {n : Type v} [DecidableEq n] [Fintype n]

namespace Matrix

open Polynomial

variable (M : Matrix n n R) (s : S)

noncomputable section

def revcharmatrix_apply : Matrix n n S :=
  1 - Matrix.scalar n s * (algebraMap R S).mapMatrix M

def revcharpoly_apply : S := det (revcharmatrix_apply M s)

open LaurentPolynomial

theorem scalar_apply_ite (a : R) (i j : n) :
    (scalar n) a i j = ite (i = j) a 0 := by
  split_ifs with h
  · subst h
    exact scalar_apply_eq a i
  · exact scalar_apply_ne _ _ _ h

theorem T_mul_revcharmatrix_apply_eq_charmatrix :
    T (R := R) 1 • (revcharmatrix_apply M (T (-1)) : Matrix n n R[T;T⁻¹]) =
      toLaurent.mapMatrix (charmatrix M) := by
  rw [revcharmatrix_apply, smul_sub]
  trans (scalar n (T 1) - (algebraMap R R[T;T⁻¹]).mapMatrix M)
  · simp only [coe_scalar, RingHom.mapMatrix_apply, AddMonoidAlgebra.coe_algebraMap,
      Algebra.id.map_eq_id, Algebra.smul_mul_assoc, one_mul, ← smul_assoc, smul_eq_mul, ← T_add,
      add_right_neg, T_zero, one_smul]
  trans ((scalar n) (toLaurent X) - ((toLaurent.comp Polynomial.C).mapMatrix) M)
  · ext
    simp
  simp only [RingHom.mapMatrix_apply, RingHom.coe_comp, map_sub,
    map_map, sub_left_inj, charmatrix]
  ext i j : 2
  rw [scalar_apply_ite, map_apply, scalar_apply_ite]
  split_ifs <;> simp

theorem T_pow_mul_revcharpoly_T_neg_one_eq_charpoly :
    T (Fintype.card n) * (revcharpoly_apply M (T (-1)) : R[T;T⁻¹]) =
      toLaurent (charpoly M) := by
  rw [revcharpoly_apply, T_eq_pow_of_nat, ← det_smul, T_mul_revcharmatrix_apply_eq_charmatrix,
    ← RingHom.map_det, charpoly, charmatrix]

--  oops the exponents have the wrong sign!
example [Nonempty n] : trace M = - ((revcharpoly_apply M (T (-1)) : R[T;T⁻¹]) : ℤ →₀ R) (-1) := by
  rw [← mul_one (revcharpoly_apply M (T (R := R) (-1))), ← T_zero,
     ← neg_add_self (Fintype.card n : ℤ), T_add, ← mul_assoc, ← T_mul, ← mul_assoc,
     T_pow_mul_revcharpoly_T_neg_one_eq_charpoly, T]
  rw [AddMonoidAlgebra.mul_single_apply, trace_eq_neg_charpoly_coeff]
  rw [mul_one, sub_eq_add_neg, add_comm, neg_neg, ← sub_eq_add_neg, neg_inj]
  convert toLaurent_apply_eq_coeff.symm
  rw [← Nat.succ_pred (Fintype.card_ne_zero (α := n))]
  simp

[Damiano Testa]

I am probably not going to have time to finish this up.

If anyone else wants to take over, feel free to do so! In particular, the proofs are completely unoptimized and there are surely plenty of golfing opportunities, locally and globally!

[Oliver Nash]

I opened PR #6450 today which I claim contains all the results about nilpotency that are needed for Damiano's very nice argument. I intend to open a second PR which actually implements the argument tomorrow and proves:

lemma Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
    {R n : Type _} [DecidableEq n] [Fintype n] (M : Matrix n n R) [CommRing R]
    (hM : IsNilpotent M) : IsNilpotent (M.charpoly - X^(Fintype.card n)) := by
  sorry