Structure theory of endomorphisms

• Eigenvalue
• Eigenvector

DefinitionInvariant subspaces of an endomorphism#

Given an endomorphism, f of some module, this is the sublattice of all f-invariant submodules.

Module.End.invtSubmodule.{u_1, u_2} {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M]
  [_root_.Module R M] (f : Module.End R M) : Sublattice (Submodule R M)

Sources

• Mathlib documentation: Module.End.invtSubmodule
• Source of Module.End.invtSubmodule in Mathlib/Algebra/Module/Submodule/Invariant.lean
• Mathlib undergraduate list: Linear algebra › Structure theory of endomorphisms

MathlibModule.End.invtSubmodule

Uses 2

Statement usesLinear map · Sum of subspaces

DefinitionGeneralized eigenspaces#

The submodule genEigenspace f μ k for a linear map f, a scalar μ, and a number k : ℕ∞ is the kernel of (f - μ • id) ^ k if k is a natural number, or the union of all these kernels if k = ∞. (k = ∞ corresponds to Def 8.19 of axler2024.) A generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

Module.End.genEigenspace.{v, w} {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M]
  [_root_.Module R M] (f : Module.End R M) (μ : R) : ℕ∞ →o Submodule R M

Sources

• Mathlib documentation: Module.End.genEigenspace
• Source of Module.End.genEigenspace in Mathlib/LinearAlgebra/Eigenspace/Basic.lean
• Mathlib undergraduate list: Linear algebra › Structure theory of endomorphisms

MathlibModule.End.genEigenspace

Uses 3 · Used by 4

Statement usesInteger · Kernel of a linear map · Sum of subspaces

Used byDiagonalization of self-adjoint endomorphisms · Eigenvalue · Eigenvector · Lie's theorem

TheoremJordan-Chevalley-Dunford decomposition#

Jordan-Chevalley-Dunford decomposition: an endomorphism of a finite-dimensional vector space over a perfect field may be written as a sum of nilpotent and semisimple endomorphisms. Moreover these nilpotent and semisimple components are polynomial expressions in the original endomorphism.

Module.End.exists_isNilpotent_isSemisimple.{u_1, u_2} {K : Type u_1} {V : Type u_2} [Field K]
  [AddCommGroup V] [_root_.Module K V] {f : Module.End K V} [FiniteDimensional K V]
  [PerfectField K] : ∃ n ∈ K[f], ∃ s ∈ K[f], IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Sources

• Mathlib documentation: Module.End.exists_isNilpotent_isSemisimple
• Source of Module.End.exists_isNilpotent_isSemisimple in Mathlib/LinearAlgebra/JordanChevalley.lean
• Mathlib undergraduate list: Linear algebra › Structure theory of endomorphisms

MathlibModule.End.exists_isNilpotent_isSemisimple

Uses 8

Statement usesAlgebra of endomorphisms of a vector space · Finite-dimensionality · Irreducible element · Separable polynomial · Sum of subspaces

Proof usesBasis · Minimal polynomial · The Fundamental Theorem of Arithmetic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.