Eigenvectors and eigenvalues over algebraically closed fields.

• Every linear operator on a vector space over an algebraically closed field has an eigenvalue.
• The generalized eigenvectors span the entire vector space.

References

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

Tags

eigenspace, eigenvector, eigenvalue, eigen

theorem Module.End.exists_eigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) : ∃ c, Module.End.HasEigenvalue f c

Every linear operator on a vector space over an algebraically closed field has an eigenvalue.

noncomputable instance Module.End.instInhabitedEigenvaluesToCommRingToEuclideanDomain {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V) : Inhabited (Module.End.Eigenvalues f)

theorem Module.End.iSup_generalizedEigenspace_eq_top {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [IsAlgClosed K] [FiniteDimensional K V] (f : Module.End K V) : ⨆ (μ : K) (k : ℕ), ↑(Module.End.generalizedEigenspace f μ) k = ⊤

The generalized eigenvectors span the entire vector space (Lemma 8.21 of [axler2015]).