Eigenvalues and eigenelements of linear endomaps of left modules over commutative rings

Content created by Louis Wasserman.

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

module spectral-theory.eigenvalues-eigenelements-linear-endomaps-left-modules-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings

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

open import linear-algebra.left-modules-commutative-rings
open import linear-algebra.left-submodules-commutative-rings
open import linear-algebra.linear-endomaps-left-modules-commutative-rings

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

Idea

Given a linear endomap f on a left module M over a commutative ring R, an element v : M is an eigenelement of f with eigenvalue c : R is an element of the eigenmodule associated with c, that is, an element of the kernel of the map v ↦ (f v - c * v).

Definition

module _
  {l1 l2 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (f : linear-endo-left-module-Commutative-Ring R M)
  where

  is-eigenelement-eigenvalue-prop-linear-endo-left-module-Commutative-Ring :
    type-Commutative-Ring R → type-left-module-Commutative-Ring R M → Prop l2
  is-eigenelement-eigenvalue-prop-linear-endo-left-module-Commutative-Ring =
    subset-eigenmodule-linear-endo-left-module-Commutative-Ring R M f

  is-eigenelement-eigenvalue-linear-endo-left-module-Commutative-Ring :
    type-Commutative-Ring R → type-left-module-Commutative-Ring R M → UU l2
  is-eigenelement-eigenvalue-linear-endo-left-module-Commutative-Ring c v =
    type-Prop
      ( is-eigenelement-eigenvalue-prop-linear-endo-left-module-Commutative-Ring
        ( c)
        ( v))

Properties

Zero is an eigenelement with every eigenvalue

module _
  {l1 l2 : Level}
  (R : Commutative-Ring l1)
  (M : left-module-Commutative-Ring l2 R)
  (f : linear-endo-left-module-Commutative-Ring R M)
  where

  abstract
    is-eigenelement-zero-linear-endo-left-module-Commutative-Ring :
      (r : type-Commutative-Ring R) →
      is-eigenelement-eigenvalue-linear-endo-left-module-Commutative-Ring
        ( R)
        ( M)
        ( f)
        ( r)
        ( zero-left-module-Commutative-Ring R M)
    is-eigenelement-zero-linear-endo-left-module-Commutative-Ring r =
      contains-zero-left-submodule-Commutative-Ring R M
        ( eigenmodule-linear-endo-left-module-Commutative-Ring R M f r)

See also

Recent changes