LinearMap_sum_roots_charpoly_map_pow_eq_trace_pow.lean

theorem trace_pow_restrict_maxGenEigenspace (S : Module.End E W) (μ : E) (n : ℕ) :
    LinearMap.trace E _ ((S ^ n).restrict
      (S.mapsTo_maxGenEigenspace_of_comm (Commute.refl S |>.pow_right n) μ)) =
      μ ^ n * (finrank E (S.maxGenEigenspace μ) : E)

theorem sum_roots_pow_eq_trace_pow [IsAlgClosed E] (S : Module.End E W) (n : ℕ) :
    ((S.charpoly).roots.map (fun z => z ^ n)).sum = LinearMap.trace E W (S ^ n) := by
  classical
  have hind := S.independent_maxGenEigenspace
  have htop := S.iSup_maxGenEigenspace_eq_top
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top hind htop
  have h_fin : {μ : E | S.maxGenEigenspace μ ≠ ⊥}.Finite :=
    WellFoundedGT.finite_ne_bot_of_iSupIndep hind
  have hf : ∀ μ : E, Set.MapsTo (S ^ n) ↑(S.maxGenEigenspace μ) ↑(S.maxGenEigenspace μ) :=
    fun μ => S.mapsTo_maxGenEigenspace_of_comm (Commute.refl S |>.pow_right n) μ
  rw [LinearMap.trace_eq_sum_trace_restrict' hds h_fin hf]
  simp_rw [trace_pow_restrict_maxGenEigenspace]
  rw [Finset.sum_multiset_map_count]
  have hset : S.charpoly.roots.toFinset = h_fin.toFinset := by
    ext μ
    rw [Multiset.mem_toFinset, Set.Finite.mem_toFinset, Set.mem_ofPred_eq,
      mem_roots (S.charpoly_monic).ne_zero, ne_eq, ← Submodule.finrank_eq_zero,
      LinearMap.finrank_maxGenEigenspace_eq, ← ne_eq, ← Nat.pos_iff_ne_zero, rootMultiplicity_pos']
    exact ⟨fun h => ⟨(S.charpoly_monic).ne_zero, h⟩, fun h => h.2⟩
  rw [hset]
  refine Finset.sum_congr rfl fun μ _ => ?_
  rw [count_roots, ← LinearMap.finrank_maxGenEigenspace_eq, nsmul_eq_mul, mul_comm]

theorem sum_roots_charpoly_map_pow_eq_trace_pow {L : Type*} [Field L] {V : Type*} [AddCommGroup V]
    [Module L V] [FiniteDimensional L V] (E : Type*) [Field E] [Algebra L E] [IsAlgClosed E]
    (T : V →ₗ[L] V) (n : ℕ) :
    (((T.charpoly).map (algebraMap L E)).roots.map (fun z => z ^ n)).sum =
      algebraMap L E (LinearMap.trace L V (T ^ n)) := by
  rw [← LinearMap.charpoly_baseChange, sum_roots_pow_eq_trace_pow, ← LinearMap.baseChange_pow,
    LinearMap.trace_baseChange]

theorem _root_.LinearMap.sum_roots_charpoly_map_pow_eq_trace_pow {L : Type*} [Field L] {V : Type*}
    [AddCommGroup V] [Module L V] [FiniteDimensional L V] (E : Type*) [Field E] [Algebra L E]
    [IsAlgClosed E] (T : V →ₗ[L] V) (n : ℕ) :
    (((T.charpoly).map (algebraMap L E)).roots.map (fun z => z ^ n)).sum =
      algebraMap L E (LinearMap.trace L V (T ^ n)) :=
  P2mC2H1.sum_roots_charpoly_map_pow_eq_trace_pow E T n