Eigenspaces 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.eigenspaces-linear-endomaps-vector-spaces where
Imports 
open import commutative-algebra.heyting-fields

open import foundation.subtypes
open import foundation.universe-levels

open import linear-algebra.linear-endomaps-vector-spaces
open import linear-algebra.subspaces-vector-spaces
open import linear-algebra.vector-spaces

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

Idea

Given a linear endomap f of a vector space V over a Heyting field F, the eigenspace of c : F is the subspace of V of vectors with eigenvalue c.

Definition

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

  eigenspace-linear-endo-Vector-Space : subspace-Vector-Space l2 F V
  eigenspace-linear-endo-Vector-Space =
    eigenmodule-linear-endo-left-module-Commutative-Ring
      ( commutative-ring-Heyting-Field F)
      ( V)
      ( f)
      ( c)

  vector-space-eigenspace-linear-endo-Vector-Space : Vector-Space l2 F
  vector-space-eigenspace-linear-endo-Vector-Space =
    left-module-eigenmodule-linear-endo-left-module-Commutative-Ring
      ( commutative-ring-Heyting-Field F)
      ( V)
      ( f)
      ( c)

See also

Recent changes