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.

References

• [Sheldon Axler, Linear Algebra Done Right][axler2015]
• https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors

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_genEigenspace_eq_top {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] {f : End R M} (k : ℕ∞) (hf : ⨆ (μ : R), (f.genEigenspace μ) k = ⊤) : ∃ (μ : R), f.HasEigenvalue μ

@[deprecated Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top (since := "2024-10-11")]

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 : 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 : End K V) : ∃ (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} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : End K V) : Inhabited f.Eigenvalues

Equations

• f.instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial = { default := ⟨⋯.choose, ⋯⟩ }

theorem Module.End.iSup_maxGenEigenspace_eq_top {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] (f : End K V) : ⨆ (μ : K), f.maxGenEigenspace μ = ⊤

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

@[deprecated Module.End.iSup_maxGenEigenspace_eq_top (since := "2024-10-11")]

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 : 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 : ∀ x ∈ p, f x ∈ p) (k : ℕ∞) : p ⊓ ⨆ (μ : K), (f.genEigenspace μ) 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] (k : ℕ∞) (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ (μ : K), (f.genEigenspace μ) k = ⊤) : p = ⨆ (μ : K), p ⊓ (f.genEigenspace μ) k

theorem Module.End.genEigenspace_restrict_eq_top {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {p : Submodule K V} {f : End K V} [FiniteDimensional K V] {k : ℕ∞} (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ (μ : K), (f.genEigenspace μ) k = ⊤) : ⨆ (μ : K), (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.

@[deprecated Module.End.genEigenspace_restrict_eq_top (since := "2024-10-11")]

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 : End K V} [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ (μ : K), ⨆ (k : ℕ), (f.genEigenspace μ) ↑k = ⊤) : ⨆ (μ : K), ⨆ (k : ℕ), (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.