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.IsSemisimple.genEigenspace_eq_eigenspace: for a semisimple endomorphism, a generalized eigenspace is an eigenspace.
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 : Module.End R M}
{μ : R}
{k : ℕ∞}
{m : M}
(hm : m ∈ (f.genEigenspace μ) k)
(hfg : Commute f g)
(hss : g.IsFinitelySemisimple)
(hnil : IsNilpotent (f - g))
:
theorem
Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
{f : Module.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 : Module.End R M}
(hf : f.IsFinitelySemisimple)
(μ : R)
:
f.maxGenEigenspace μ = f.eigenspace μ