feat(Analysis/InnerProductSpace): transfer lemmas about charpoly/eigenvalues from matrix to linear map (#37325)

These are some lemmas existing for matrix but missing for linear map.

Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>

Author: wwylele

Mathlib/Analysis/InnerProductSpace/Spectrum.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.InnerProductSpace.Rayleigh
 public import Mathlib.Analysis.Normed.Group.Submodule
 public import Mathlib.Analysis.Normed.Operator.FredholmAlternative
+public import Mathlib.LinearAlgebra.Eigenspace.Charpoly
 public import Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap
 public import Mathlib.LinearAlgebra.Eigenspace.Minpoly
 public import Mathlib.Data.Fin.Tuple.Sort
@@ -343,6 +344,53 @@ theorem eigenvectorBasis_apply_self_apply (hT : T.IsSymmetric) (hn : Module.finr
   intro a
   rw [smul_smul, mul_comm, ofLp_toLp]
 
+theorem toMatrix_eigenvectorBasis (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) :
+    letI b := (hT.eigenvectorBasis hn).toBasis
+    T.toMatrix b b = Matrix.diagonal (RCLike.ofReal ∘ hT.eigenvalues hn) := by
+  ext i j
+  simp [toMatrix_apply, Matrix.diagonal_apply, RCLike.real_smul_eq_coe_mul]
+  grind
+
+open Polynomial in
+theorem charpoly_eq (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) :
+    T.charpoly = ∏ i, (X - C (hT.eigenvalues hn i : 𝕜)) := by
+  simp [← T.charpoly_toMatrix (hT.eigenvectorBasis hn).toBasis, toMatrix_eigenvectorBasis,
+    Matrix.charpoly_diagonal]
+
+theorem roots_charpoly_eq_eigenvalues (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) :
+    T.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hT.eigenvalues hn) Finset.univ.val := by
+  rw [← charpoly_toMatrix _ (hT.eigenvectorBasis hn).toBasis, toMatrix_eigenvectorBasis,
+    Matrix.charpoly_diagonal, Polynomial.roots_prod _ _ (by
+      simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero])]
+  simp
+
+theorem sort_roots_charpoly_eq_eigenvalues (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) :
+    (T.charpoly.roots.map RCLike.re).sort (· ≥ ·) = List.ofFn (hT.eigenvalues hn) := by
+  simp_rw [hT.roots_charpoly_eq_eigenvalues, Fin.univ_val_map, Multiset.map_coe, List.map_ofFn,
+    Function.comp_def, RCLike.ofReal_re, Multiset.coe_sort]
+  have := hn.symm
+  convert List.mergeSort_of_pairwise ?_
+  simp_rw [decide_eq_true_eq, ← List.sortedGE_iff_pairwise]
+  convert (hT.eigenvalues_antitone hn).sortedGE_ofFn
+
+theorem eigenvalues_eq_eigenvalues_iff {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E']
+    [FiniteDimensional 𝕜 E'] {T' : E' →ₗ[𝕜] E'} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
+    (hT' : T'.IsSymmetric) (hn' : Module.finrank 𝕜 E' = n) :
+    hT.eigenvalues hn = hT'.eigenvalues hn' ↔ T.charpoly = T'.charpoly where
+  mp h := by rw [hT.charpoly_eq hn, hT'.charpoly_eq hn', h]
+  mpr h := by
+    rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues, ← sort_roots_charpoly_eq_eigenvalues,
+      h]
+
+theorem splits_charpoly (hT : T.IsSymmetric) : T.charpoly.Splits := by
+  refine Polynomial.splits_iff_card_roots.mpr ?_
+  simp [hT.roots_charpoly_eq_eigenvalues rfl, LinearMap.charpoly_natDegree]
+
+theorem det_eq_prod_eigenvalues (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) :
+    T.det = ∏ i, (hT.eigenvalues hn i : 𝕜) := by
+  simp [det_eq_prod_roots_charpoly_of_splits hT.splits_charpoly,
+    hT.roots_charpoly_eq_eigenvalues hn, List.prod_ofFn]
+
 end Version2
 
 end IsSymmetric

Mathlib/Analysis/InnerProductSpace/Trace.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.InnerProductSpace.PiL2
 public import Mathlib.Analysis.InnerProductSpace.Spectrum
-public import Mathlib.LinearAlgebra.Trace
+public import Mathlib.LinearAlgebra.Eigenspace.Charpoly
 
 /-!
 # Traces in inner product spaces
@@ -38,12 +38,8 @@ variable {n : ℕ} (hn : Module.finrank 𝕜 E = n)
 
 lemma IsSymmetric.trace_eq_sum_eigenvalues {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
     T.trace 𝕜 E = ∑ i, hT.eigenvalues hn i := by
-  let b := hT.eigenvectorBasis hn
-  rw [T.trace_eq_sum_inner b, RCLike.ofReal_sum]
-  apply Fintype.sum_congr
-  intro i
-  rw [hT.apply_eigenvectorBasis, inner_smul_real_right, inner_self_eq_norm_sq_to_K, b.norm_eq_one]
-  simp [RCLike.ofReal_alg]
+  simp [Module.End.trace_eq_sum_roots_charpoly_of_splits hT.splits_charpoly,
+    hT.roots_charpoly_eq_eigenvalues hn, List.sum_ofFn]
 
 lemma IsSymmetric.re_trace_eq_sum_eigenvalues {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :
     RCLike.re (T.trace 𝕜 E) = ∑ i, hT.eigenvalues hn i := by

Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.LinearAlgebra.Charpoly.BaseChange
 public import Mathlib.LinearAlgebra.Charpoly.ToMatrix
 public import Mathlib.LinearAlgebra.Eigenspace.Basic
+public import Mathlib.LinearAlgebra.Trace
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
 
 /-!
 # Eigenvalues are the roots of the characteristic polynomial.
@@ -44,6 +46,17 @@ lemma mem_spectrum_iff_isRoot_charpoly (f : End K V) (μ : K) :
     μ ∈ spectrum K f ↔ f.charpoly.IsRoot μ := by
   rw [← hasEigenvalue_iff_mem_spectrum, hasEigenvalue_iff_isRoot_charpoly]
 
+lemma det_eq_prod_roots_charpoly_of_splits {f : End K V} (h : f.charpoly.Splits) :
+    f.det = f.charpoly.roots.prod := by
+  rw [← det_toMatrix (Module.Free.chooseBasis K V),
+    Matrix.det_eq_prod_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
+
+lemma trace_eq_sum_roots_charpoly_of_splits {f : End K V} (h : f.charpoly.Splits) :
+    f.trace K V = f.charpoly.roots.sum := by
+  let b := Module.Free.chooseBasis K V
+  rw [trace_eq_matrix_trace K (Module.Free.chooseBasis K V),
+    Matrix.trace_eq_sum_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
+
 end End
 
 end Module