More challenges reasoning about traces of representations

Stream: new members

[Ryan Smith]

Following some discussion here I've been handling the eigenvalues of a FDRep as a Multiset and had some success proving various results using helper methods for connecting the IsEigenvalueMultiset definition back to the problem at hand. I don't know if the trouble I'm having proving results such as

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

are indicative of taking the wrong approach to formalizing the various theorems I'm working on for complex characters. The mathematical reason this is true is really obvious: for each eigenvector v of V.ρ g we have v = (V.ρ g^-1) (V.ρ g) v = (V.ρ g^-1) z v = z (V.ρ g^-1) v for some z. So for each eigenvalue z of the original we can deduce that z^-1 is an eigenvector of (V.ρ g^-1) easily enough. But we have can have multiplicity.

Do we argue that for each z in the Multiset of eigenvalues that d_i := dim of ker((V.ρ g) - z 1) must be the same as the dimension of corresponding kernel for V.ρ g^-1 by getting d_i independent vectors and arguing that each of them is an eigenvector V.ρ g^-1, therefore (X-z^{-1})^d_i | charpoly (V.ρ g^-1) and eventually argue that the product of all of those terms divides charpoly so we have equality?

I could see this maybe working eventually but it seems like we're getting really bogged down and are probably following some kind of bad design pattern. At this point we've also mostly forgotten about our Multiset idea and unfolded the definition to go back to the charpoly.

A similar theorem where it starts to get really bogged down in one direction after a while is

theorem char_g_eq_char_1_iff_g_mem_ker (V : FDRep ℂ G) (g : G) :
    V.character g = V.character 1 ↔ g ∈ V.ρ.ker := by sorry

In the second case we can show that in the →direction that all of the eigenvalues must be 1 that's not enough.

I'm not asking for proofs of either of those two results but rather whether I'm trying to prove these statements in ways that are making things harder than they need to be. Here is the setup for the problem and some helper results which have been built up along the way:

import Mathlib
universe u

open BigOperators Group ComplexConjugate
open Module Module.End
open Multiset
open Polynomial
open LinearMap
variable {G : Type} [Group G] [Finite G]

def IsEigenvalueMultiset (V : FDRep ℂ G) (g : G) (s : Multiset ℂ) :=
  ∀ (z : ℂ), count z s = rootMultiplicity z (charpoly (V.ρ g))

theorem mem_eigen_ms_eigenvalue {V : FDRep ℂ G} (g : G) (s : Multiset ℂ)
    (h : IsEigenvalueMultiset V g s) (z : ℂ) (hz : z ∈ s) : HasEigenvalue (V.ρ g) z := by sorry -- skipped here

lemma exists_char_eigenvalue_ms (V : FDRep ℂ G) (g : G) :
    ∃ (s : Multiset ℂ), IsEigenvalueMultiset V g s := by
  refine ⟨ _, fun and' => count_roots (_)⟩

theorem char_eq_eigenvalue_ms_sum (V : FDRep ℂ G) (g : G) (s : Multiset ℂ)
    (h : IsEigenvalueMultiset V g s) : V.character g = ∑ z ∈ s.toEnumFinset, z.1 := by sorry -- skipped here

lemma eigen_norm_one (V : FDRep ℂ G) (g : G) (μ : ℂ) (h : HasEigenvalue (V.ρ g) μ) : ‖μ‖ = 1 := by
  have : 0 < Nat.card G := Nat.card_pos
  exact Complex.norm_eq_one_of_pow_eq_one (eigenvalue_root_unity V g μ h) (by grind)

lemma eigen_ms_norm1 {V : FDRep ℂ G} (g : G) (s : Multiset ℂ)
    (h : IsEigenvalueMultiset V g s) (z : ℂ) (hz : z ∈ s) : ‖z‖ = 1 := by
  have := mem_eigen_ms_eigenvalue g s h z hz
  exact eigen_norm_one V g z this

-- etc etc

[Lawrence Wu (llllvvuu)]

Working with charpoly seems reasonable for this, though some missing API would need to be developed first:

• charpoly of inverse, and maybe its specialization to the case where it splits, i.e. (A^-1).charpoly = (A.charpoly.roots.map fun r => X - C r^-1).prod or something

[Lawrence Wu (llllvvuu)]

For the char_g_eq_char_1_iff_g_mem_ker lemma I believe you also need to show diagonalizability or something (e.g.). Only then does charpoly A = (x-1)^n imply A = 1 (which is not true in general). You can argue then that A = PDP^-1, and prod (x - d i) = charpoly(D) = charpoly(A) = (x-1)^n (docs#Matrix.charpoly_mul_comm or docs#Matrix.charpoly_units_conj), hence d i = 1 for all i, so D = I, so A = I.

[Lawrence Wu (llllvvuu)]

We don't have diagonalizability in the library yet. This could certainly be optimized but it's a start:

import Mathlib
universe u

open BigOperators Group ComplexConjugate
open Module Module.End
open Multiset
open Polynomial
open LinearMap
variable {G : Type} [Group G] [Finite G]

-- https://github.com/leanprover-community/mathlib4/pull/29428
section PR29428

variable {K M : Type*} [Field K] [AddCommGroup M]
variable [Module K M] [Module.Finite K M]

lemma finrank_maxGenEigenspace_eq (φ : Module.End K M) (μ : K) :
    finrank K (φ.maxGenEigenspace μ) = φ.charpoly.rootMultiplicity μ := by
  sorry

end PR29428

section MoreAPI

variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]

-- exercise for the reader
lemma Module.End.eigenspace_eq_top_iff {f : Module.End R M} {μ : R} :
    f.eigenspace μ = ⊤ ↔ f = μ • 1 := by
  sorry

theorem Module.End.isSemisimple_iff_minpoly_squarefree {K M : Type*} [AddCommGroup M] [Field K]
    [Module K M] {f : End K M} [FiniteDimensional K M] :
    f.IsSemisimple ↔ Squarefree (minpoly K f) :=
  ⟨IsSemisimple.minpoly_squarefree, (isSemisimple_of_squarefree_aeval_eq_zero · (minpoly.aeval ..))⟩

end MoreAPI

theorem char_g_eq_char_1_iff_g_mem_ker (V : FDRep ℂ G) (g : G) :
    V.character g = V.character 1 ↔ g ∈ V.ρ.ker := by
  constructor
  · intro h
    -- exercise for the reader
    have h0 : ∀ r ∈ (V.ρ g).charpoly.roots, r = 1 := sorry
    have h1 : (V.ρ g).charpoly = (X - C 1) ^ (finrank ℂ V.V) := by
      rw [Polynomial.eq_prod_roots_of_monic_of_splits_id
        ((V.ρ g).charpoly_monic) (IsAlgClosed.splits _)]
      suffices (V.ρ g).charpoly.roots = Multiset.replicate (finrank ℂ V.V) 1 by
        simp [this]
      have : (finrank ℂ ↑V.V) = (V.ρ g).charpoly.roots.card := by
        rw [Polynomial.splits_iff_card_roots.mp (IsAlgClosed.splits _), charpoly_natDegree]
      rw [this, Multiset.eq_replicate_card]
      exact h0
    have h2 : minpoly ℂ (V.ρ g) ∣ X ^ orderOf g - C 1 := by
      apply minpoly.dvd
      simp only [map_one, aeval_sub, map_pow, aeval_X]
      rw [← MonoidHom.map_pow, pow_orderOf_eq_one]
      simp
    -- exercise for the reader
    have h3 : Squarefree (X ^ orderOf g - C 1 : ℂ[X]) := sorry
    have h4 : Squarefree (minpoly ℂ (V.ρ g)) := h3.squarefree_of_dvd h2
    rw [← Module.End.isSemisimple_iff_minpoly_squarefree,
      ← Module.End.isFinitelySemisimple_iff_isSemisimple] at h4
    rw [MonoidHom.mem_ker, ← one_smul ℂ 1, ← Module.End.eigenspace_eq_top_iff,
      ← h4.maxGenEigenspace_eq_eigenspace]
    apply Submodule.eq_top_of_finrank_eq
    rw [finrank_maxGenEigenspace_eq, h1, Polynomial.rootMultiplicity_X_sub_C_pow]
  · simp_all [FDRep.character]

[Ryan Smith]

For charpoly of inverse, is there a way to bind variables to the coefficients of a polynomial defined by a non computable definition (such as charpoly)?

In other words, can we get variables a_i \in \C so that I can write the characteristic polynomial of my original matrix A as

$$\sum_{i=0}^n a_i A^i = 0$$

We could then get an expression for charpoly A^{-1} via algebraic manipulation. This is one way that lean is very different from a whiteboard where we could just say "let a_0, ..., a_n" be the coefficients and get to work.

[Lawrence Wu (llllvvuu)]

docs#Polynomial.ext would likely be used for that approach.

I also have an AI-generated (using Aristotle) proof of this theorem which I intend to clean up / golf and PR to mathlib. It uses docs#Matrix.reverse_charpoly:

import Mathlib

noncomputable section

open scoped Classical

def B {n R : Type*} [Fintype n] [CommRing R] (A : Matrix n n R) : Matrix n n (Polynomial R) := (@Polynomial.X R _) • A.map Polynomial.C

lemma charpoly_inv_step1 {n R : Type*} [Fintype n] [CommRing R] (A : Matrix n n R) (h : IsUnit A) : A⁻¹.charpoly = Polynomial.C (A⁻¹).det * (Matrix.det ((@Polynomial.X R _) • (A.map Polynomial.C) - 1)) := by
  simp only [inv_eq_one_div];
  -- Now use the fact that multiplication by a unit matrix preserves the determinant.
  have h_unit : (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A)).det = (Polynomial.C (1 / A).det) * ((Polynomial.C.mapMatrix A) * (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A))).det := by
    -- Since $A$ is invertible, we can factor out $A^{-1}$ from the expression $(X - A^{-1})$.
    have h_factor : (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A)) = Polynomial.C.mapMatrix (1 / A) * (Polynomial.C.mapMatrix A * (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A))) := by
      -- Since $A$ is invertible, we can simplify the expression using the property of matrix multiplication and inverses.
      have h_simp : A⁻¹.map (⇑Polynomial.C) * A.map (⇑Polynomial.C) = 1 := by
        rw [ ← Matrix.map_mul, Matrix.nonsing_inv_mul _ ];
        · ext i j; by_cases hi : i = j <;> aesop;
        · exact IsUnit.map ( Matrix.detMonoidHom ) h;
      simp ( config := { decide := Bool.true } ) [ ← mul_assoc, h_simp ];
    -- By the properties of determinants, we can factor out the determinant of $A^{-1}$ from the right-hand side.
    have h_det_factor : Matrix.det (Polynomial.C.mapMatrix (1 / A) * (Polynomial.C.mapMatrix A * (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A)))) = Matrix.det (Polynomial.C.mapMatrix (1 / A)) * Matrix.det (Polynomial.C.mapMatrix A * (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A))) := by
      rw [ Matrix.det_mul ];
    convert h_det_factor using 1;
    · exact?;
    · simp ( config := { decide := Bool.true } ) [ Matrix.det_apply' ];
  -- Since $A$ is invertible, $A.map C$ is also invertible, and multiplying by its inverse gives the identity matrix.
  have h_inv : A.map (Polynomial.C) * A⁻¹.map (Polynomial.C) = 1 := by
    rw [ ← Matrix.map_mul ];
    -- Since $A$ is invertible, $A * A⁻¹ = 1$, and applying the map function to the identity matrix gives the identity matrix.
    have h_id : A * A⁻¹ = 1 := by
      rw [ Matrix.mul_nonsing_inv _ _ ];
      exact h.map Matrix.detMonoidHom;
    aesop;
  -- By expanding both sides, we can see that they are indeed equal.
  have h_expand : A.map (Polynomial.C) * (Matrix.scalar n Polynomial.X - Polynomial.C.mapMatrix (1 / A)) = Matrix.scalar n Polynomial.X * A.map (Polynomial.C) - 1 := by
    simp ( config := { decide := Bool.true } ) [ mul_sub, sub_mul, h_inv ];
    ext i j; by_cases hi : i = j <;> simp ( config := { decide := Bool.true } ) [ hi ];
  convert h_unit using 2;
  norm_num +zetaDelta at *;
  rw [ ← Matrix.det_mul, h_expand, Matrix.smul_eq_diagonal_mul ]


lemma charpoly_inv_step2 {n R : Type*} [Fintype n] [CommRing R] (A : Matrix n n R) : Matrix.det ((@Polynomial.X R _) • A.map Polynomial.C - 1) = (-1) ^ Fintype.card n * A.charpoly.reverse := by
  have h_det_neg : Matrix.det ((Polynomial.X : (Polynomial R)) • (A.map Polynomial.C) - 1) = (-1) ^ (Fintype.card n) * Matrix.det (1 - (Polynomial.X : (Polynomial R)) • (A.map Polynomial.C)) := by
    -- By the property of determinants, $\det(-M) = (-1)^n \det(M)$ for any matrix $M$.
    have h_det_neg : ∀ (M : Matrix n n (Polynomial R)), Matrix.det (-M) = (-1 : Polynomial R) ^ (Fintype.card n) * Matrix.det M := by
      -- Apply the theorem that states the determinant of a matrix multiplied by -1 is (-1)^n times the determinant of the original matrix.
      intros M
      apply Matrix.det_neg;
    rw [ ← h_det_neg, neg_sub ];
  convert h_det_neg;
  -- Apply the lemma that states the reverse of the characteristic polynomial is equal to the determinant of (1 - X * A.map C).
  apply Matrix.reverse_charpoly


theorem charpoly_inv_formula {n R : Type*} [Fintype n] [CommRing R] (A : Matrix n n R) (h : IsUnit A) :
    A⁻¹.charpoly = Polynomial.C ((-1) ^ Fintype.card n * (A⁻¹).det) * A.charpoly.reverse := by
      -- By combining the results from `charpoly_inv_step1` and `charpoly_inv_step2`, we can conclude the proof.
      have h_combined : A⁻¹.charpoly = Polynomial.C (A⁻¹.det) * ((-1) ^ Fintype.card n * A.charpoly.reverse) := by
        rw [charpoly_inv_step1, charpoly_inv_step2];
        bound;
      -- By combining the results from `charpoly_inv_step1` and `charpoly_inv_step2`, we can conclude the proof using the properties of determinants and characteristic polynomials.
      rw [h_combined]
      simp [mul_assoc, mul_comm, mul_left_comm]

[Ryan Smith]

What's aristotle?

[Lawrence Wu (llllvvuu)]

https://leanprover.zulipchat.com/#narrow/channel/219941-Machine-Learning-for-Theorem-Proving/topic/Harmonic.3A.20IMO.20Livestream/near/531472433