Eigenvalues, Eigenvectors and Spectrum for Matrices

This file collects results about eigenvectors, eigenvalues and spectrum specific to matrices over a nontrivial commutative ring, nontrivial commutative ring without zero divisors, or field.

Tags

eigenspace, eigenvector, eigenvalue, spectrum, matrix

theorem hasEigenvector_toLin_diagonal {R : Type u_1} {n : Type u_2} {M : Type u_3} [DecidableEq n] [Fintype n] [CommRing R] [Nontrivial R] [AddCommGroup M] [Module R M] (d : n → R) (i : n) (b : Basis n R M) : Module.End.HasEigenvector ((Matrix.toLin b b) (Matrix.diagonal d)) (d i) (b i)

Basis vectors are eigenvectors of associated diagonal linear operator.

theorem hasEigenvector_toLin'_diagonal {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] [Nontrivial R] (d : n → R) (i : n) : Module.End.HasEigenvector (Matrix.toLin' (Matrix.diagonal d)) (d i) ((Pi.basisFun R n) i)

Standard basis vectors are eigenvectors of any associated diagonal linear operator.

theorem hasEigenvalue_toLin_diagonal_iff {R : Type u_1} {n : Type u_2} {M : Type u_3} [DecidableEq n] [Fintype n] [CommRing R] [Nontrivial R] [AddCommGroup M] [Module R M] (d : n → R) {μ : R} [NoZeroSMulDivisors R M] (b : Basis n R M) : Module.End.HasEigenvalue ((Matrix.toLin b b) (Matrix.diagonal d)) μ ↔ ∃ (i : n), d i = μ

Eigenvalues of a diagonal linear operator are the diagonal entries.

theorem hasEigenvalue_toLin'_diagonal_iff {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] [Nontrivial R] [NoZeroDivisors R] (d : n → R) {μ : R} : Module.End.HasEigenvalue (Matrix.toLin' (Matrix.diagonal d)) μ ↔ ∃ (i : n), d i = μ

Eigenvalues of a diagonal linear operator with respect to standard basis are the diagonal entries.

theorem spectrum_diagonal {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Field R] (d : n → R) : spectrum R (Matrix.diagonal d) = Set.range d

The spectrum of the diagonal operator is the range of the diagonal viewed as a function.