Eigenvalues and eigenvectors of linear endomaps of vector spaces

Content created by Louis Wasserman.

Created on 2026-02-24.
Last modified on 2026-02-24.

module spectral-theory.eigenvalues-eigenvectors-linear-endomaps-vector-spaces where
Imports 
open import commutative-algebra.heyting-fields

open import foundation.propositions
open import foundation.universe-levels

open import linear-algebra.left-modules-rings
open import linear-algebra.linear-endomaps-vector-spaces
open import linear-algebra.vector-spaces

open import spectral-theory.eigenvalues-eigenelements-linear-endomaps-left-modules-commutative-rings

Idea

Given a linear endomap f on a vector space V over a Heyting field F, an vector v : V is an eigenvector of f with eigenvalue c : F if it is a member of the eigenspace associated with c, that is, it is in the kernel of the map v ↦ (f v - c * v).

Definition

module _
  {l1 l2 : Level}
  (F : Heyting-Field l1)
  (V : Vector-Space l2 F)
  (f : linear-endo-Vector-Space F V)
  where

  is-eigenvector-eigenvalue-prop-linear-endo-Vector-Space :
    type-Heyting-Field F → type-Vector-Space F V → Prop l2
  is-eigenvector-eigenvalue-prop-linear-endo-Vector-Space =
    is-eigenelement-eigenvalue-prop-linear-endo-left-module-Commutative-Ring
      ( commutative-ring-Heyting-Field F)
      ( V)
      ( f)

  is-eigenvector-eigenvalue-linear-endo-Vector-Space :
    type-Heyting-Field F → type-Vector-Space F V → UU l2
  is-eigenvector-eigenvalue-linear-endo-Vector-Space c v =
    type-Prop (is-eigenvector-eigenvalue-prop-linear-endo-Vector-Space c v)

See also

Recent changes