Eigenmodules 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.eigenmodules-linear-endomaps-left-modules-commutative-rings where
Imports 
open import commutative-algebra.commutative-rings

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.difference-linear-maps-left-modules-commutative-rings
open import linear-algebra.kernels-linear-maps-left-modules-commutative-rings
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 linear-algebra.scalar-multiplication-linear-maps-left-modules-commutative-rings
open import linear-algebra.subsets-left-modules-commutative-rings

Idea

Given a linear endomap f of a left module M over a commutative ring R, the eigenmodule of r : R is the subset of elements of M with the eigenvalue r. This subset is a submodule of M.

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)
  (r : type-Commutative-Ring R)
  where

  eigenmodule-linear-endo-left-module-Commutative-Ring :
    left-submodule-Commutative-Ring l2 R M
  eigenmodule-linear-endo-left-module-Commutative-Ring =
    kernel-linear-map-left-module-Commutative-Ring R M M
      ( diff-linear-map-left-module-Commutative-Ring R M M
        ( f)
        ( linear-endo-mul-left-module-Commutative-Ring R M r))

  subset-eigenmodule-linear-endo-left-module-Commutative-Ring :
    subset-left-module-Commutative-Ring l2 R M
  subset-eigenmodule-linear-endo-left-module-Commutative-Ring =
    subset-left-submodule-Commutative-Ring
      ( R)
      ( M)
      ( eigenmodule-linear-endo-left-module-Commutative-Ring)

  left-module-eigenmodule-linear-endo-left-module-Commutative-Ring :
    left-module-Commutative-Ring l2 R
  left-module-eigenmodule-linear-endo-left-module-Commutative-Ring =
    left-module-left-submodule-Commutative-Ring
      ( R)
      ( M)
      ( eigenmodule-linear-endo-left-module-Commutative-Ring)

See also

Recent changes