Eigenspaces of semisimple linear endomorphisms

This file contains basic results relevant to the study of eigenspaces of semisimple linear endomorphisms.

Main definitions / results

• Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace: for a semisimple endomorphism, a generalized eigenspace is an eigenspace.
• Module.End.IsSemisimple.iSup_eigenspace_eq_top: over an algebraically closed field, the eigenspaces of a semisimple endomorphism span the whole space.
• Module.End.IsSemisimple.eq_zero_iff_forall_eigenvalue: a semisimple endomorphism over an algebraically closed field is zero iff all eigenvalues are zero.

theorem Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f g : End R M} {μ : R} {k : ℕ∞} {m : M} (hm : m ∈ (f.genEigenspace μ) k) (hfg : Commute f g) (hss : g.IsFinitelySemisimple) (hnil : IsNilpotent (f - g)) : g m = μ • m

theorem Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (hf : f.IsFinitelySemisimple) (μ : R) {k : ℕ∞} (hk : 0 < k) : (f.genEigenspace μ) k = f.eigenspace μ

theorem Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (hf : f.IsFinitelySemisimple) (μ : R) : f.maxGenEigenspace μ = f.eigenspace μ

theorem Module.End.IsSemisimple.iSup_eigenspace_eq_top {K : Type u_3} {V : Type u_4} [Field K] [IsAlgClosed K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} (hf : f.IsSemisimple) : ⨆ (μ : K), f.eigenspace μ = ⊤

theorem Module.End.IsSemisimple.eq_zero_iff_forall_eigenvalue {K : Type u_3} {V : Type u_4} [Field K] [IsAlgClosed K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} (hf : f.IsSemisimple) : f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0