Matrix trace

Stream: new members

[Hbz]

C is a matrix over the real number field ℝ. How should I show that all eigenvalues of C lie in the complex number field, and then use the theorem Matrix.trace_eq_sum_roots_charpoly_of_splits to prove that the sum of all its eigenvalues is equal to its trace? Or is there any other method?

import Mathlib

open Matrix Module

noncomputable section

lemma M (C : Matrix (Fin 2) (Fin 2) ℝ): C.trace = ((C.charpoly.map (algebraMap ℝ ℂ)).roots).sum := by
  let D : Matrix (Fin 2) (Fin 2) ℂ := C.map (algebraMap ℝ ℂ)
  have hd : D = C.map (algebraMap ℝ ℂ) := by exact rfl
  have h0 : D.trace = C.trace := by
    rw[hd]
    sorry
  sorry

This is my way,but i can't solve it.
Or in fact,my problem self is wrong?

[Damiano Testa]

You can conclude as follows:

lemma M (C : Matrix (Fin 2) (Fin 2) ℝ): C.trace = ((C.charpoly.map (algebraMap ℝ ℂ)).roots).sum := by
  let D : Matrix (Fin 2) (Fin 2) ℂ := C.map (algebraMap ℝ ℂ)
  have hd : D = C.map (algebraMap ℝ ℂ) := rfl
  have h0 : D.trace = C.trace := by
    rw[hd]
    -- The `erw` suggests that either I do not know the correct lemma, or one is missing
    erw [← AddMonoidHom.map_trace]
    simp
  convert D.trace_eq_sum_roots_charpoly
  · exact h0.symm
  · simp_all only [Complex.coe_algebraMap]
    rw [← hd, charpoly_map]

[Hbz]

Dude, you're amazing. I have another question. How did you find a theorem like AddMonoidHom.map_trace? Have you used it before, or did you infer that it must exist? Every time I encounter problems like this type conversion, I can't find the relevant theorems.

[Damiano Testa]

I was expecting a map_trace lemma to exist, so I typed something like apply map_trace[Ctrl-space] and looked at the autocompletion suggestions.

[Damiano Testa]

Btw, I found some of the other lemmas by looking at the output of rw? at various places in the proof.

[Hbz]

ok :+1: