How to reason about eigenvectors for a LinearMap

Stream: new members

[Ryan Smith]

I'm trying to prove a bunch of results involving the trace of a finite dimension representation over \C, and they usually involve reasoning one eigenvalue at a time. I've been contorting into more and more awkward constructions to do this and they all seem like I must be going about it the wrong way.

import Mathlib
universe u
open Group Module Module.End

variable {G: Type} [Group G] [Finite G]
variable [g : G] [V : FDRep \C G]

#check Module.End.Eigenvalues (V.ρ g)  -- this is the type of all eigenvectors correct?
#check Module.End.Eigenvalues.val (V.ρ g)  -- this takes an instance of the previous type to \C ?

We can assert for a specific (z: \C) that it's an eigenvalue with End.HasEigenvalue (V.ρ g) z, but how do we even express to lean that the trace of V.ρ g is the sum of all eigenvalues? When Module.End.Eigenvalues is a type and not a set, even saying that is not well defined.

I'd considered taking the linear map, converting it to a matrix, using a result which says that the trace is the sum of the roots of the characteristic polynomial and trying to work with those roots but the version of the fundamental theorem of algebra in lean isn't structured in terms of a sequence of roots of anything like that so it seems like that gets bogged down.

The mounting complexity and work arounds to work arounds suggest I'm not framing the problem correctly. As an example of where we're trying to go, I can get a bound on each individual eigenvalue so the next lemma is a bound on the trace.

[Kevin Buzzard]

Can you write a #mwe of a statement that you would like to prove? That's the best way of asking a question of this nature.

And why are you using category theory? Are you sure you want to also introduce this extra layer of complexity? My instinct for basic representation theory is to prove everything for Representation first and deduce it for FDRep later using the Representation work.

[Ryan Smith]

@Kevin Buzzard
Ultimate goal: prove Burnsides theorem.

Ultimate reason: I remember it fondly from grad school and it's a warmup for contributing other stuff.

Here is a snippet with one lemma which I can prove, and two which were going to use the first lemma that I can't. I have more theorems sketched out but in some cases I can't even express the statement properly yet such as "V.character g is an algebraic integer within ℂ", and "the set of irreducible characters of G form a basis for the space ℂ-linear functions from conjugacy classes of G to ℂ".

import Mathlib

open ComplexConjugate Module Module.End
variable {G : Type} [Group G] [Finite G]

lemma eigenvalue_norm_one (V: FDRep ℂ G) (g : G) (μ : ℂ) (h : HasEigenvalue (V.ρ g) μ) : ‖μ‖ = 1 := by
  sorry  -- have working proof just skipping the details here

lemma char_norm_bound (V: FDRep ℂ G) (g : G) : ‖V.character g‖ ≤ ‖V.character 1‖ := by
  sorry  -- stuck

lemma char_inv_conj (V: FDRep ℂ G) (g : G) : V.character g⁻¹ = conj V.character g := by
  sorry  -- stuck

Proving results about individual eigenvalues wasn't too difficult so far, but to connect that to a result about the trace is where I'm fighting with lean. Naively I'd say something like "let S be the finite set of eigenvectors of V.ρ g, then trace V.ρ g is the sum of the elements of that set and we can make an inequality from there to prove our result about V.character g".

I think most of the results here wouldn't apply for a general Representation since they require finite dimension. A lot of the results could be proved for a field of char 0 with sufficient roots of unity I suppose. Brauer characters would be more general (and cool) but that's a different project.

[Ruben Van de Velde]

Which trace is that?

[Kevin Buzzard]

@Ryan Smith your claim in comments is incorrect because sets only contain elements with "multiplicity 1" by definition of a set, and you need to keep track of multiplicities to push this through. For example if $g$ is the identity then $S=\{1\}$ so the sum is 1 regardless of the dimension of the rep. You either want to use Multisets (where multiplicities can be finite, but this is enough for you) or a sum of generalised eigenvalues $\mu_i$ over an index type $I$ where $i$ runs through the elements (which allows $\mu_1=\mu_2$ which also solves the multiplicity problem). Part of the art of formalisation is choosing the most painless path to go down, so it's probably worth looking at the API for docs#LinearMap.trace to see what is already there.

[Ryan Smith]

Do you have an opinion as to what route do you think is a better path for making arguments about the trace of a linear map if the facts we know are some statements about each eigenvalue? I realize there are multiple ways we could go about formalizing these arguments.

[Kevin Buzzard]

I'm having trouble getting mathlib cache at the minute but you're asking the right question. My instinct is to look through the library to find theorems relating traces of linear maps or matrices to sums of (generalised) eigenvalues but to my great surprise I'm finding very little; I'm sure I'm missing something.

[Ryan Smith]

I went looking and didn't find a lot of the stuff I'd expect, but mathlib is still a wild jungle to me. So far the only thing I've found a result that the trace of a matrix is the sum of the roots of the charpoly, which is nice but not really what I need.

[Matt Diamond]

@loogle "eigenvalue", "trace"

[loogle]

:search: LinearMap.IsSymmetric.trace_eq_sum_eigenvalues, LinearMap.IsSymmetric.re_trace_eq_sum_eigenvalues, and 1 more

[Matt Diamond]

hm

[Kevin Buzzard]

These are all theorems of the form "if a linear map satisfies some condition which makes it diagonalisable, then the trace is the sum of the eigenvalues when presented as a list (of the size we expect)".

[Kevin Buzzard]

Do we have things like "trace is - coefficient of $X^{n-1}$ in char poly" and "sum of multiset Polynomial.roots is - coefficient of $X^{n-1}$ for a monic polynomial which Polynomial.Splits" and "every root of char poly is an eigenvalue"? That might be the most painless way to proceed.

[Ruben Van de Velde]

We have docs#Matrix.trace_eq_neg_charpoly_coeff

[Ryan Smith]

Something like Matrix.IsHermitian.eigenvalues for more general matrices would be perfect, it would make it easy to reason about the trace. I wonder why this doesn't exist in the same way.

Edit: might need a hypothesis on the field but otherwise I don't see why this is only a special case

[Ryan Smith]

Kevin Buzzard said:

Do we have things like "trace is - coefficient of $X^{n-1}$ in char poly" and "sum of multiset Polynomial.roots is - coefficient of $X^{n-1}$ for a monic polynomial which Polynomial.Splits" and "every root of char poly is an eigenvalue"? That might be the most painless way to proceed.

The second result seems to be the missing part. We have https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Eigenspace/Minpoly.html#Module.End.hasEigenvalue_of_isRoot connecting roots with eigenvalues but I haven't found anything about a deg n polynomial having a multiset of roots with n elements counting multiplicities

[Kevin Buzzard]

Ryan Smith said:

Something like Matrix.IsHermitian.eigenvalues for more general matrices would be perfect, it would make it easy to reason about the trace. I wonder why this doesn't exist in the same way.

eigenvalues and generalisedEigenvalues are different for a nonHermitian matrix, and perhaps we should have both.

[Kevin Buzzard]

It is not even clear to me what the type of eigenvalues should be for a non-diagonalisable matrix. What is the indexing type? It might have size smaller than the dimension.

[Ryan Smith]

If there were a hypothesis that the characteristic polynomial split then the index would be the dimension and we could have the same api.

[Kevin Buzzard]

I don't really understand what you mean. The char poly of (1,1;0,1) is $(X-1)^2$ which splits but this isn't diagonalisable.

Of course any endomorphism of finite order over a char 0 field is diagonalisable so this should not be a concern for you. Maybe working with the multiset of roots of the char poly is just easier in this situation?

[Kevin Buzzard]

Vaguely related: do we not have this?

def Representation.det {R G V : Type*} [CommSemiring R] [Monoid G]
    [AddCommMonoid V] [Module R V] [Module.Finite R V] [Module.Free R V]
    (ρ : Representation R G V) : Representation R G R := sorry

[Ryan Smith]

Good question, I don't know why we don't have that. I also noticed that in RepresentationTheory/Character we have

theorem char_tensor (V W : FDRep k G) : (V ⊗ W).character = V.character * W.character := by
  ext g; convert trace_tensorProduct' (V.ρ g) (W.ρ g)

but no direct sum

Maybe you're right and a multiset of roots would be the way to go. Polynomial.exists_multiset_roots seems promising

[Kevin Buzzard]

Re direct sums: I think that the idea was just to get straight to "distinct irred characters are orthogonal" and for that one slick way is to define tensor product rep. We're not formalising textbooks here -- we're typically formalising "the stuff I need to do the project I'm working on" so sometimes what's there is a bit haphazard.

[Kevin Buzzard]

noncomputable def Representation.det {R G V : Type*} [CommRing R] [Monoid G]
    [AddCommGroup V] [Module R V] (ρ : Representation R G V) : Representation R G R :=
  ((DistribMulAction.toModuleEnd R R).comp (LinearMap.det)).comp ρ

[Lawrence Wu (llllvvuu)]

Ryan Smith said:

Kevin Buzzard said:

Do we have things like "trace is - coefficient of $X^{n-1}$ in char poly" and "sum of multiset Polynomial.roots is - coefficient of $X^{n-1}$ for a monic polynomial which Polynomial.Splits" and "every root of char poly is an eigenvalue"? That might be the most painless way to proceed.

The second result seems to be the missing part. We have https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Eigenspace/Minpoly.html#Module.End.hasEigenvalue_of_isRoot connecting roots with eigenvalues but I haven't found anything about a deg n polynomial having a multiset of roots with n elements counting multiplicities

Porting that result over to matrices: #29481 (with docs#Module.End.hasEigenvalue_iff_mem_spectrum)
For the charpoly (which is deg n, per docs#Matrix.charpoly_degree_eq_dim), it can be derived directly: #29478
Regarding multiplicities, the algebraic multiplicity is definitional, but we can relate the geometric multiplicity: #29428
We have the things about X^{n-1}: docs#Matrix.trace_eq_sum_roots_charpoly_of_splits, docs#Matrix.coeff_charpolyRev_eq_neg_trace

You can prove your original lemmas using docs#LinearMap.trace_eq_matrix_trace and docs#LinearMap.charpoly_toMatrix

[Lawrence Wu (llllvvuu)]

needs cleanup, but:

import Mathlib

-- #29478
theorem Matrix.mem_spectrum_of_isRoot_charpoly.{u_1, u_2} {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R]
    {B : Matrix n n R} [Nontrivial R] {r : R} (hr : B.charpoly.IsRoot r) : r ∈ spectrum R B := by
  sorry

-- #29481
theorem LinearMap.spectrum_toMatrix.{u_1, u_3, u_4} {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} {M : Type u_4}
    [CommRing R] [AddCommGroup M] [Module R M] (b : Module.Basis n R M) (A : M →ₗ[R] M) :
    spectrum R ((LinearMap.toMatrix b b) A) = spectrum R A := by
  sorry

open ComplexConjugate Module Module.End
variable {G : Type} [Group G] [Finite G]

lemma eigenvalue_norm_one (V: FDRep ℂ G) (g : G) (μ : ℂ) (h : HasEigenvalue (V.ρ g) μ) : ‖μ‖ = 1 := by
  sorry  -- have working proof just skipping the details here

lemma char_norm_bound (V: FDRep ℂ G) (g : G) : ‖V.character g‖ ≤ ‖V.character 1‖ := by
  let b := Module.Free.chooseBasis ℂ V.V
  simp only [FDRep.character, LinearMap.trace_eq_matrix_trace ℂ b]
  grw [Matrix.trace_eq_sum_roots_charpoly, norm_multiset_sum_le]
  set S := ((LinearMap.toMatrix b b) (V.ρ g)).charpoly.roots
  calc
    _ = (S.map fun _ => (1 : ℝ)).sum := by
      congr 1
      apply Multiset.map_congr rfl
      intro r hr
      apply eigenvalue_norm_one V g r
      rw [Module.End.hasEigenvalue_iff_mem_spectrum, ← LinearMap.spectrum_toMatrix b]
      apply Matrix.mem_spectrum_of_isRoot_charpoly
      apply Polynomial.isRoot_of_mem_roots
      exact hr
    _ ≤ _ := by
      suffices S.card ≤ Fintype.card (Free.ChooseBasisIndex ℂ ↑V.V) by simpa
      grw [Polynomial.card_roots', Matrix.charpoly_natDegree_eq_dim]

[Lawrence Wu (llllvvuu)]

Can save a line or two if we transport some results from Matrix to LinearMap:

import Mathlib

-- Not in Mathlib
theorem LinearMap.trace_eq_sum_roots_charpoly {K G : Type*} [Field K] [AddCommGroup G]
    [Module K G] [Module.Finite K G] [Module.Free K G] (f : Module.End K G) (hf : Polynomial.Splits (RingHom.id K) f.charpoly) :
    LinearMap.trace K G f = f.charpoly.roots.sum := by
  unfold LinearMap.charpoly at hf ⊢
  set b := Module.Free.chooseBasis K G
  rw [LinearMap.trace_eq_matrix_trace K b, Matrix.trace_eq_sum_roots_charpoly_of_splits hf]

-- #29478
theorem Module.End.hasEigenvalue_iff_isRoot_charpoly {K G : Type*} [Field K] [AddCommGroup G]
    [Module K G] [Module.Finite K G] [Module.Free K G] (f : Module.End K G) (μ : K) :
    f.HasEigenvalue μ ↔ f.charpoly.IsRoot μ := by
  sorry

open ComplexConjugate Module Module.End
variable {G : Type} [Group G] [Finite G]

lemma eigenvalue_norm_one (V: FDRep ℂ G) (g : G) (μ : ℂ) (h : HasEigenvalue (V.ρ g) μ) : ‖μ‖ = 1 := by
  sorry  -- have working proof just skipping the details here

lemma char_norm_bound (V: FDRep ℂ G) (g : G) : ‖V.character g‖ ≤ ‖V.character 1‖ := by
  unfold FDRep.character
  grw [LinearMap.trace_eq_sum_roots_charpoly, norm_multiset_sum_le]
  set S := (V.ρ g).charpoly.roots
  calc
    _ = (S.map fun _ => (1 : ℝ)).sum := by
      congr 1
      apply Multiset.map_congr rfl
      intro r hr
      apply eigenvalue_norm_one V g r
      rw [Module.End.hasEigenvalue_iff_isRoot_charpoly]
      apply Polynomial.isRoot_of_mem_roots
      exact hr
    _ ≤ _ := by
      suffices S.card ≤ finrank ℂ ↑V.V by simpa
      grw [Polynomial.card_roots', LinearMap.charpoly_natDegree]