# Triangularizable linear endomorphisms #

This file contains basic results relevant to the triangularizability of linear endomorphisms.

## Main definitions / results #

• Module.End.exists_eigenvalue: in finite dimensions, over an algebraically closed field, every linear endomorphism has an eigenvalue.
• Module.End.iSup_genEigenspace_eq_top: in finite dimensions, over an algebraically closed field, the generalized eigenspaces of any linear endomorphism span the whole space.
• Module.End.iSup_genEigenspace_restrict_eq_top: in finite dimensions, if the generalized eigenspaces of a linear endomorphism span the whole space then the same is true of its restriction to any invariant submodule.

## TODO #

Define triangularizable endomorphisms (e.g., as existence of a maximal chain of invariant subspaces) and prove that in finite dimensions over a field, this is equivalent to the property that the generalized eigenspaces span the whole space.

## Tags #

eigenspace, eigenvector, eigenvalue, eigen

theorem Module.End.exists_hasEigenvalue_of_iSup_genEigenspace_eq_top {R : Type u_3} {M : Type u_4} [] [] [Module R M] [] {f : } (hf : ⨆ (μ : R), ⨆ (k : ), (f.genEigenspace μ) k = ) :
∃ (μ : R), f.HasEigenvalue μ
theorem Module.End.exists_eigenvalue {K : Type u_1} {V : Type u_2} [] [] [Module K V] [] [] [] (f : ) :
∃ (c : K), f.HasEigenvalue c

In finite dimensions, over an algebraically closed field, every linear endomorphism has an eigenvalue.

noncomputable instance Module.End.instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial {K : Type u_1} {V : Type u_2} [] [] [Module K V] [] [] [] (f : ) :
Inhabited f.Eigenvalues
Equations
• f.instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial = { default := .choose, }
theorem Module.End.iSup_genEigenspace_eq_top {K : Type u_1} {V : Type u_2} [] [] [Module K V] [] [] (f : ) :
⨆ (μ : K), ⨆ (k : ), (f.genEigenspace μ) k =

In finite dimensions, over an algebraically closed field, the generalized eigenspaces of any linear endomorphism span the whole space.

theorem Submodule.inf_iSup_genEigenspace {K : Type u_1} {V : Type u_2} [] [] [Module K V] {p : } {f : } [] (h : xp, f x p) :
p ⨆ (μ : K), ⨆ (k : ), (f.genEigenspace μ) k = ⨆ (μ : K), ⨆ (k : ), p (f.genEigenspace μ) k
theorem Submodule.eq_iSup_inf_genEigenspace {K : Type u_1} {V : Type u_2} [] [] [Module K V] {p : } {f : } [] (h : xp, f x p) (h' : ⨆ (μ : K), ⨆ (k : ), (f.genEigenspace μ) k = ) :
p = ⨆ (μ : K), ⨆ (k : ), p (f.genEigenspace μ) k
theorem Module.End.iSup_genEigenspace_restrict_eq_top {K : Type u_1} {V : Type u_2} [] [] [Module K V] {p : } {f : } [] (h : xp, f x p) (h' : ⨆ (μ : K), ⨆ (k : ), (f.genEigenspace μ) k = ) :
⨆ (μ : K), ⨆ (k : ), () k =

In finite dimensions, if the generalized eigenspaces of a linear endomorphism span the whole space then the same is true of its restriction to any invariant submodule.