Documentation

Mathlib.LinearAlgebra.Eigenspace.Triangularizable

Triangularizable linear endomorphisms #

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

Main definitions / results #

References #

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} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] {f : Module.End R M} (hf : ⨆ (μ : R), ⨆ (k : ), (f.genEigenspace μ) k = ) :
∃ (μ : R), f.HasEigenvalue μ
theorem Module.End.exists_eigenvalue {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) :
∃ (c : K), f.HasEigenvalue c

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

Equations
  • f.instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial = { default := .choose, }
theorem Module.End.iSup_genEigenspace_eq_top {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] (f : Module.End K V) :
⨆ (μ : 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} [Field K] [AddCommGroup V] [Module K V] {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] (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} [Field K] [AddCommGroup V] [Module K V] {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] (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} [Field K] [AddCommGroup V] [Module K V] {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] (h : xp, f x p) (h' : ⨆ (μ : K), ⨆ (k : ), (f.genEigenspace μ) k = ) :
⨆ (μ : K), ⨆ (k : ), (Module.End.genEigenspace (LinearMap.restrict f h) μ) 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.