Eigenvalues of matrices: Trace Determinants and others

Stream: new members

[MohanadAhmed]

Hello Everyone,

What I am trying to do?

I am trying to formalize matrix identities that are related to eigenvalues. Two examples here are: Trace of a matrix is the sum of eigenvalues and determinant of matrix is product of eigenvalues.

For Hermitian case I was able to make use of the is_hermitian lemmas to do most of the work. docs#matrix.is_hermitian.eigenvalues. In the case of non-hermitian matrices there seems to be still a disconnect in mathlib. Eigenvalues are defined for Endomorphisms in docs#module.End.eigenvalues. These are defined in such a way that they would even work for infinite dimensions. But for finite matrices they may not be the best. One particular issue is the information about multiplicity is lost, which makes talking about Trace and Determinant identities more difficult.

The plan I have in mind is as follows:

1. Define eigenvalue multiplicity as the multiplicity of the root of the characteristic polynomial.
2. Similar to docs#polynomial.exists_multiset_root we define exists_multiset_eigs which says that there is a multiset of eigenvalues with the correct multiplicities.
3. By classical.some we get a handle on one such set. This is defined as eigs.
4. Show that every eigenvalue in the multiset is also satisfies module.End.has_eigenvalue (matrix.to_lin' A) μ
5. Show that the whole set of elements in (eigenvalues.fintype (matrix.to_lin' A)).elems

Then get to the proofs of det_eq_prod_eigs and trace_eq_sum_eigs. Before diving into this plan, I thought I would get some opinions on it.

Big Question

Does this plan sound reasonable?
Is it just completely wrong?
If it is not just that bad :sweat_smile: , any suggestions on easier, simpler ways to do this?

Smaller Problems:

1. Cannot get μ ∈ eigenvaluesA to type check. The type of eigenvalues is finset(eigenvalues ...). The full error message is

failed to synthesize type class instance for
n : Type u_1,
_inst_1 : fintype n,
_inst_2 : decidable_eq n,
_inst_3 : nonempty n,
A : matrix n n ℂ,
μ : ℂ,
eigenvaluesA : finset (eigenvalues (⇑to_lin' A)) := fintype.elems (eigenvalues (⇑to_lin' A))
⊢ has_mem ℂ (finset (eigenvalues (⇑to_lin' A)))

This seems to make sense ℂ and eigenvalues (⇑to_lin' A) are not the same thing. But how do I convince lean to convert them. From docs docs#module.End.has_coe should do some conversion, but I don't know how to use it.

2. How would one show that the nth - 1 coefficient is the sum of all the roots.

The lean code I have so far is below

import linear_algebra.matrix.spectrum
import linear_algebra.eigenspace
import data.complex.basic
import linear_algebra.matrix.charpoly.coeff

variables {n: Type*}[fintype n][decidable_eq n][nonempty n]

open matrix polynomial
open module.End
open_locale classical
open_locale matrix big_operators

noncomputable def eig_multiplicity (A: matrix n n ℂ) (μ: ℂ) : ℕ :=
  polynomial.root_multiplicity μ (matrix.charpoly A)

lemma exists_multiset_eigs {A : matrix n n ℂ}  (hp : A ≠ 0) :
  ∃ s : multiset ℂ, (s.card : with_bot ℕ) ≤ fintype.card n ∧ ∀ μ, s.count μ = eig_multiplicity A μ
  :=
begin
  unfold eig_multiplicity,
  have p_nz : matrix.charpoly A ≠ 0, {
    by_contra, replace h := congr_arg nat_degree h, simp only [nat_degree_zero] at h,
    have p_deg := matrix.charpoly_nat_degree_eq_dim A, rw p_deg at h,
    have hn: fintype.card n ≠ 0, {exact fintype.card_ne_zero,},
    exact hn h,
  },
  have Adeg := matrix.charpoly_degree_eq_dim A,
  let zeta := exists_multiset_roots p_nz,
  rw ← Adeg,
  exact zeta,
end

noncomputable def eigs (A: matrix n n ℂ): multiset ℂ :=
  if h : A = 0  then ∅
  else classical.some (exists_multiset_eigs h)

lemma eig_is_eigenvalue (A: matrix n n ℂ) (μ: ℂ) :
  μ ∈ eigs A ↔  module.End.has_eigenvalue (matrix.to_lin' A) μ := sorry

lemma eigs_are_eigenvalues (A: matrix n n ℂ) : ∀(μ : ℂ),
  let eigenvaluesA := (eigenvalues.fintype (matrix.to_lin' A)).elems in
  μ ∈ eigenvaluesA ↔ μ ∈ eigs A  := sorry

/-Useful Lemmas -/
lemma det_eq_prod_eigs (A: matrix n n ℂ): A.det = (eigs A).prod := sorry
lemma trace_eq_sum_eigs (A: matrix n n ℂ) {hn: nonempty n}: A.trace = (eigs A).sum := --sorry
begin
  by_cases hAz: A = 0, rw hAz, rw trace_zero, rw eigs,
  simp only [multiset.empty_eq_zero, dif_pos, multiset.sum_zero],

  -- A ≠ 0 Case
  rw trace_eq_neg_charpoly_coeff A,
  -- have:
end

[Kevin Buzzard]

In the finite rank case the natural definition would be the multiset of eigenvalues of an endomorphism, defined as the multiset of roots of the char poly, which would make sense if the base ring is an integral domain. You don't necessarily need to carry around the multiplicities, you can just sum over the multiset.

[MohanadAhmed]

Do you mean something like in this line:

lemma trace_eq_sum_eigs (A: matrix n n ℂ) {hn: nonempty n}: A.trace = (eigs A).sum

• If what I understand is correct the multiset carries the multiplicities around, hence when it is constructed, we need to provide that piece of information right?

[Kevin Buzzard]

Yes sorry! I glanced at your code but didn't grok that you were doing exactly what I had in mind already! Sorry.

[Kevin Buzzard]

You shouldn't need nonempty n and you shouldn't need to work over the complexes (the theorem is true in characteristic p for example, it's pure algebra not analysis)

[Kevin Buzzard]

I don't really see why you're not just using the multiset of roots of the polynomial rather than using the axiom of choice in this artificial way

[Kevin Buzzard]

Do we not have the multiset of roots of a polynomial? (Guessing docs#polynomial.roots)

[Kevin Buzzard]

Yeah it's there already, you don't have to make it again

[Kevin Buzzard]

And it correctly has just the assumption that R is an integral domain. Just apply that to the char poly.

[Kevin Buzzard]

Furthermore I'd suggest that you don't work with matrices but instead focus on endomorphisms of finite rank modules for as long as possible. There is absolutely no need to pick a basis here.

[Kevin Buzzard]

docs#linear_map.charpoly should be the generality (plus R an integral domain so that you can take the multiset of roots)

[Eric Wieser]

Kevin Buzzard said:

Furthermore I'd suggest that you don't work with matrices but instead focus on endomorphisms of finite rank modules for as long as possible. There is absolutely no need to pick a basis here.

Though note that both trace and determinant are defined on endomorphisms via matrices, so it might be marginally easier to prove results about those on matrices first

[Eric Wieser]

Cannot get μ ∈ eigenvaluesA to type check. The type of eigenvalues is finset(eigenvalues ...).

You need to use μ ∈ eigenvaluesA.image coe, which converts the RHS into finset complex

[MohanadAhmed]

For now it seems lean is convinced that the trace is the sum of eigenvalues and determinant is the product of eigenvalues. However I still did not link the eigenvalues defined as roots of charpoly to the eigenvalues as defined in mathlib (which is the root of the minpoly). I am struggling with proving that the root of a characteristic polynomial is also the root of a minimal polymial. Any help or pointers to what lemmas in mathlib to use appreciated.

import linear_algebra.matrix.spectrum
import linear_algebra.eigenspace
import linear_algebra.charpoly.basic
import linear_algebra.matrix.charpoly.coeff
import linear_algebra.charpoly.to_matrix
import linear_algebra.matrix.charpoly.minpoly
import data.complex.basic
import analysis.complex.polynomial

variables {n: Type*}[fintype n][decidable_eq n][nonempty n]
variables {R: Type*}[field R][is_alg_closed R]

open matrix polynomial
open linear_map module.End
open_locale matrix big_operators

noncomputable def eigs (A: matrix n n R): multiset R :=
  polynomial.roots (matrix.charpoly A)

lemma is_root_minpoly_iff_is_root_charpoly (A: matrix n n ℂ) (μ: ℂ) :
  is_root (matrix.charpoly A) μ ↔ is_root (minpoly ℂ A) μ :=
begin
  split,
  intro h,
  set mp := minpoly ℂ A,
  sorry, -- HERE is where I am out of attempts!!!

  intro h,
  apply is_root.dvd h,
  exact matrix.minpoly_dvd_charpoly A,
end


lemma det_eq_prod_eigs (A: matrix n n R):
  A.det = (eigs A).prod :=
begin
  rw eigs,
  by_cases hn: nonempty n, {
    rw det_eq_sign_charpoly_coeff,
    have hdeg := charpoly_nat_degree_eq_dim A,
    rw ← hdeg,
    rw polynomial.prod_roots_eq_coeff_zero_of_monic_of_split,
    rw ← mul_assoc, rw ← pow_two,
    rw ← pow_mul,
    by_cases h2: ring_char R ≠ 2, {
      have hstupid: -1 ≠ (1:R),
        {exact ring.neg_one_ne_one_of_char_ne_two h2,},
      have hs2 : even(A.charpoly.nat_degree*2),
        {simp only [even.mul_left, even_two],},
        rw (neg_one_pow_eq_one_iff_even hstupid).2 hs2, rw one_mul,
    },{
      rw [ne.def, not_not] at h2,
      rw neg_one_eq_one_iff.2 h2, rw one_pow, rw one_mul,
    },
    apply matrix.charpoly_monic,
    exact is_alg_closed.splits A.charpoly,
  }, {
    rw not_nonempty_iff at hn,
    rw matrix.charpoly,
    repeat {rw det_eq_one_of_card_eq_zero (fintype.card_eq_zero_iff.2 hn)},
    rw polynomial.roots_one,
    simp only [multiset.empty_eq_zero, multiset.prod_zero],
  }
end

lemma trace_eq_sum_eigs (A: matrix n n R) : A.trace = (eigs A).sum := --sorry
begin
  rw eigs,
  by_cases hn: (nonempty n), {
    apply_fun (has_neg.neg),
    rw ← polynomial.sum_roots_eq_next_coeff_of_monic_of_split ,
    rw trace_eq_neg_charpoly_coeff, rw next_coeff,
    rw neg_neg, rw charpoly_nat_degree_eq_dim,
    have fn: 0 < fintype.card n, by apply (fintype.card_pos),
    have fne := ne_of_lt fn,
    symmetry' at fne, rw ne.def at fne,
    split_ifs, refl,
    apply matrix.charpoly_monic,
    exact is_alg_closed.splits A.charpoly,
    rintros a x hax, rwa neg_inj at hax,
  }, {
    rw not_nonempty_iff at hn,
    rw matrix.trace,
    rw fintype.sum_empty _, rotate, exact hn,
    rw matrix.charpoly,
    rw det_eq_one_of_card_eq_zero (fintype.card_eq_zero_iff.2 hn),
    rw polynomial.roots_one,
    simp only [multiset.empty_eq_zero, multiset.sum_zero],
  },
end

[Mauricio Collares]

docs#module.End.is_root_of_has_eigenvalue

[Mauricio Collares]

Maybe not actually helpful, since I couldn't find API for the connection between eigenvalues and roots of the characteristic polynomial

[MohanadAhmed]

Hello @Mauricio Collares .
The link I am missing is between the roots of characteristic polynomial and the minimal polynomial. I can show that a root of the minimal polynomial is a root of the characeristic polynomial, using docs#is_root.dvd and docs#matrix.minpoly_dvd_charpoly. However I cannot go back. If I know the root of the characteristic I am not able to prove that it is the root of the minimal

Perhaps to make it clearer here is a diagram of where I am missing
Picture1.png
eigs <---> charpoly.roots ????? minpoly.roots <------> has_eigenvalue

[MohanadAhmed]

The red arrow is the one I am missing

[Eric Wieser]

This post and this one may be of interest