Beginnings of complex character theory

Stream: maths

[Geno Racklin Asher]

I'm currently trying to prove that the character f of a complex representation of a finite group satisfies f(g^-1) = f(g)*. Here's what I have so far:

import Mathlib.RepresentationTheory.Character
import Mathlib.LinearAlgebra.Trace
import Mathlib.Tactic
import Mathlib.Analysis.Complex.Polynomial
import Mathlib.Algebra.Star.Basic
import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs

variable (G : Type _) [Group G] [Fintype G] (g : G)
variable (V : FdRep ℂ G)

lemma conjAe_sum (s : Multiset ℂ) : Complex.conjAe s.sum = (s.map Complex.conjAe).sum := by
  apply AddMonoidHom.map_multiset_sum (α := ℂ) (β := ℂ) (starAddEquiv (R := ℂ))

theorem char_inv_eq_conj : FdRep.character V g⁻¹ = Complex.conjAe (FdRep.character V g) := by
  unfold FdRep.character
  have b := FiniteDimensional.finBasis ℂ V
  rw [LinearMap.trace_eq_matrix_trace ℂ b (FdRep.ρ V g⁻¹),
    LinearMap.trace_eq_matrix_trace ℂ b (FdRep.ρ V g)]
  rw [Matrix.trace_eq_sum_roots_charpoly, Matrix.trace_eq_sum_roots_charpoly]
  rw [conjAe_sum]
  congr
  ext x
  rw [Polynomial.count_roots]
  sorry

But I'm not sure how to proceed from here. Any help would be much appreciated.

[Kevin Buzzard]

Do you know the maths proof or are you asking about the maths proof? all you've done so far is unfolded everything without using the key fact that g has finite order (the result is false in general if g has infinite order)

[Kevin Buzzard]

Really this is a theorem about automorphisms of a complex finite-dimensional vector space of finite order

[Kevin Buzzard]

I am assuming we have the multiset of eigenvalues of an endomorphism of a finite-dimensional vector space. I would be tempted to prove (1) trace is sum of eigenvalues (which presumably we have) and (2) eigenvalues of inverse equals inverse of eigenvalues and (3) eigenvalues of finite order automorphism are roots of 1 and (4) conjugate of a root of unity (and more generally a complex number of norm 1) is its inverse. These feel like they're the building blocks for the result and it might be better to establish these first and then put them together to get the result you want, rather than just running straight at the result you want with what seems to be little idea about the direction you want to go.

[Kevin Buzzard]

Formalisation works best if you have a plan.

[Geno Racklin Asher]

I know the maths proof - putting the trace in terms of the roots of polys was a first step on that front

[Geno Racklin Asher]

I think what I've been struggling with is finding appropriate theorems for some of those intermediate results

[Geno Racklin Asher]

In particular, that taking the inverses of eigenvalues corresponds to the char poly of the inverse matrix

[Geno Racklin Asher]

Apologies if I didn't make it clear, I think where I got stuck in this instance is trying to get from Multiset.map conjAe ... into the roots of a new polynomial which I then want to show is the char poly of the appropriate matrix

[Geno Racklin Asher]

But yes, I think you're right that I need to break down the result much more to make some progress

[Kevin Buzzard]

So you first want to formalise the statement of what you want, and then if it's not in the library you want to start a new lemma proving it rather than just arguing in one big proof