Eigenvectors and eigenvalues

This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized counterparts. We follow Axler's approach [axler2015] because it allows us to derive many properties without choosing a basis and without using matrices.

An eigenspace of a linear map f for a scalar μ is the kernel of the map (f - μ • id). The nonzero elements of an eigenspace are eigenvectors x. They have the property f x = μ • x. If there are eigenvectors for a scalar μ, the scalar μ is called an eigenvalue.

There is no consensus in the literature whether 0 is an eigenvector. Our definition of HasEigenvector permits only nonzero vectors. For an eigenvector x that may also be 0, we write x ∈ f.eigenspace μ.

A generalized eigenspace of a linear map f for a natural number k and a scalar μ is the kernel of the map (f - μ • id) ^ k. The nonzero elements of a generalized eigenspace are generalized eigenvectors x. If there are generalized eigenvectors for a natural number k and a scalar μ, the scalar μ is called a generalized eigenvalue.

The fact that the eigenvalues are the roots of the minimal polynomial is proved in LinearAlgebra.Eigenspace.Minpoly.

The existence of eigenvalues over an algebraically closed field (and the fact that the generalized eigenspaces then span) is deferred to LinearAlgebra.Eigenspace.IsAlgClosed.

References

• [Sheldon Axler, Linear Algebra Done Right][axler2015]
• https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors

Tags

eigenspace, eigenvector, eigenvalue, eigen

def Module.End.eigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : Submodule R M

The submodule eigenspace f μ for a linear map f and a scalar μ consists of all vectors x such that f x = μ • x. (Def 5.36 of [axler2015])

Equations

• f.eigenspace μ = LinearMap.ker (f - (algebraMap R (Module.End R M)) μ)

theorem Module.End.eigenspace_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : f.eigenspace μ = LinearMap.ker (f - (algebraMap R (Module.End R M)) μ)

@[simp]

theorem Module.End.eigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) : f.eigenspace 0 = LinearMap.ker f

def Module.End.HasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (x : M) : Prop

A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015])

Equations

• f.HasEigenvector μ x = (x ∈ f.eigenspace μ ∧ x ≠ 0)

theorem Module.End.hasEigenvector_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} : f.HasEigenvector μ x ↔ x ∈ f.eigenspace μ ∧ x ≠ 0

def Module.End.HasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (a : R) : Prop

A scalar μ is an eigenvalue for a linear map f if there are nonzero vectors x such that f x = μ • x. (Def 5.5 of [axler2015])

Equations

• f.HasEigenvalue a = (f.eigenspace a ≠ ⊥)

theorem Module.End.hasEigenvalue_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : f.HasEigenvalue μ ↔ f.eigenspace μ ≠ ⊥

def Module.End.Eigenvalues {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) : Type v

The eigenvalues of the endomorphism f, as a subtype of R.

Equations

• f.Eigenvalues = { μ : R // f.HasEigenvalue μ }

def Module.End.Eigenvalues.val {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) : f.Eigenvalues → R

Equations

• ↑f = Subtype.val

instance Module.End.Eigenvalues.instCoeOut {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : CoeOut f.Eigenvalues R

Equations

• Module.End.Eigenvalues.instCoeOut = { coe := ↑f }

instance Module.End.Eigenvalues.instDecidableEq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq R] (f : Module.End R M) : DecidableEq f.Eigenvalues

Equations

• Module.End.Eigenvalues.instDecidableEq f = inferInstanceAs (DecidableEq { x : R // f.HasEigenvalue x })

theorem Module.End.hasEigenvalue_of_hasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} (h : f.HasEigenvector μ x) : f.HasEigenvalue μ

theorem Module.End.mem_eigenspace_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} : x ∈ f.eigenspace μ ↔ f x = μ • x

theorem Module.End.HasEigenvector.apply_eq_smul {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} (hx : f.HasEigenvector μ x) : f x = μ • x

theorem Module.End.HasEigenvector.pow_apply {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {v : M} (hv : f.HasEigenvector μ v) (n : ℕ) : (f ^ n) v = μ ^ n • v

theorem Module.End.HasEigenvalue.exists_hasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : f.HasEigenvalue μ) : ∃ (v : M), f.HasEigenvector μ v

theorem Module.End.HasEigenvalue.pow {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (h : f.HasEigenvalue μ) (n : ℕ) : (f ^ n).HasEigenvalue (μ ^ n)

theorem Module.End.HasEigenvalue.isNilpotent_of_isNilpotent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {f : Module.End R M} (hfn : IsNilpotent f) {μ : R} (hf : f.HasEigenvalue μ) : IsNilpotent μ

A nilpotent endomorphism has nilpotent eigenvalues.

See also LinearMap.isNilpotent_trace_of_isNilpotent.

theorem Module.End.HasEigenvalue.mem_spectrum {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : f.HasEigenvalue μ) : μ ∈ spectrum R f

theorem Module.End.hasEigenvalue_iff_mem_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : f.HasEigenvalue μ ↔ μ ∈ spectrum K f

theorem Module.End.HasEigenvalue.of_mem_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} : μ ∈ spectrum K f → f.HasEigenvalue μ

Alias of the reverse direction of Module.End.hasEigenvalue_iff_mem_spectrum.

theorem Module.End.eigenspace_div {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (a : K) (b : K) (hb : b ≠ 0) : f.eigenspace (a / b) = LinearMap.ker (b • f - (algebraMap K (Module.End K V)) a)

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

The generalized eigenspace for a linear map f, a scalar μ, and an exponent k ∈ ℕ is the kernel of (f - μ • id) ^ k. (Def 8.10 of [axler2015]). Furthermore, a generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

Equations

• f.genEigenspace μ = { toFun := fun (k : ℕ) => LinearMap.ker ((f - (algebraMap R (Module.End R M)) μ) ^ k), monotone' := ⋯ }

theorem Module.End.genEigenspace_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) : (f.genEigenspace μ) k = LinearMap.ker ((f - (algebraMap R (Module.End R M)) μ) ^ k)

@[simp]

theorem Module.End.mem_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) (m : M) : m ∈ (f.genEigenspace μ) k ↔ ((f - μ • 1) ^ k) m = 0

@[simp]

theorem Module.End.genEigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (k : ℕ) : (f.genEigenspace 0) k = LinearMap.ker (f ^ k)

def Module.End.HasGenEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) (x : M) : Prop

A nonzero element of a generalized eigenspace is a generalized eigenvector. (Def 8.9 of [axler2015])

Equations

• f.HasGenEigenvector μ k x = (x ≠ 0 ∧ x ∈ (f.genEigenspace μ) k)

theorem Module.End.hasGenEigenvector_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} {x : M} : f.HasGenEigenvector μ k x ↔ x ≠ 0 ∧ x ∈ (f.genEigenspace μ) k

def Module.End.HasGenEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) : Prop

A scalar μ is a generalized eigenvalue for a linear map f and an exponent k ∈ ℕ if there are generalized eigenvectors for f, k, and μ.

Equations

• f.HasGenEigenvalue μ k = ((f.genEigenspace μ) k ≠ ⊥)

theorem Module.End.hasGenEigenvalue_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) : f.HasGenEigenvalue μ k ↔ (f.genEigenspace μ) k ≠ ⊥

def Module.End.genEigenrange {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) : Submodule R M

The generalized eigenrange for a linear map f, a scalar μ, and an exponent k ∈ ℕ is the range of (f - μ • id) ^ k.

Equations

• f.genEigenrange μ k = LinearMap.range ((f - (algebraMap R (Module.End R M)) μ) ^ k)

theorem Module.End.genEigenrange_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) : f.genEigenrange μ k = LinearMap.range ((f - (algebraMap R (Module.End R M)) μ) ^ k)

theorem Module.End.exp_ne_zero_of_hasGenEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} (h : f.HasGenEigenvalue μ k) : k ≠ 0

The exponent of a generalized eigenvalue is never 0.

def Module.End.maxGenEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : Submodule R M

The union of the kernels of (f - μ • id) ^ k over all k.

Equations

• f.maxGenEigenspace μ = ⨆ (k : ℕ), (f.genEigenspace μ) k

theorem Module.End.maxGenEigenspace_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : f.maxGenEigenspace μ = ⨆ (k : ℕ), (f.genEigenspace μ) k

theorem Module.End.genEigenspace_le_maximal {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) : (f.genEigenspace μ) k ≤ f.maxGenEigenspace μ

@[simp]

theorem Module.End.mem_maxGenEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (m : M) : m ∈ f.maxGenEigenspace μ ↔ ∃ (k : ℕ), ((f - μ • 1) ^ k) m = 0

noncomputable def Module.End.maxGenEigenspaceIndex {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : ℕ

If there exists a natural number k such that the kernel of (f - μ • id) ^ k is the maximal generalized eigenspace, then this value is the least such k. If not, this value is not meaningful.

Equations

• f.maxGenEigenspaceIndex μ = monotonicSequenceLimitIndex (f.genEigenspace μ)

theorem Module.End.maxGenEigenspace_eq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [h : IsNoetherian R M] (f : Module.End R M) (μ : R) : f.maxGenEigenspace μ = (f.genEigenspace μ) (f.maxGenEigenspaceIndex μ)

For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel (f - μ • id) ^ k for some k.

theorem Module.End.hasGenEigenvalue_of_hasGenEigenvalue_of_le {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} {m : ℕ} (hm : k ≤ m) (hk : f.HasGenEigenvalue μ k) : f.HasGenEigenvalue μ m

A generalized eigenvalue for some exponent k is also a generalized eigenvalue for exponents larger than k.

theorem Module.End.eigenspace_le_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} (hk : 0 < k) : f.eigenspace μ ≤ (f.genEigenspace μ) k

The eigenspace is a subspace of the generalized eigenspace.

theorem Module.End.hasGenEigenvalue_of_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} (hk : 0 < k) (hμ : f.HasEigenvalue μ) : f.HasGenEigenvalue μ k

All eigenvalues are generalized eigenvalues.

theorem Module.End.hasEigenvalue_of_hasGenEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} (hμ : f.HasGenEigenvalue μ k) : f.HasEigenvalue μ

All generalized eigenvalues are eigenvalues.

@[simp]

theorem Module.End.hasGenEigenvalue_iff_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} (hk : 0 < k) : f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ

Generalized eigenvalues are actually just eigenvalues.

theorem Module.End.genEigenspace_le_genEigenspace_finrank {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) (k : ℕ) : (f.genEigenspace μ) k ≤ (f.genEigenspace μ) (Module.finrank K V)

Every generalized eigenvector is a generalized eigenvector for exponent finrank K V. (Lemma 8.11 of [axler2015])

@[simp]

theorem Module.End.iSup_genEigenspace_eq_genEigenspace_finrank {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) : ⨆ (k : ℕ), (f.genEigenspace μ) k = (f.genEigenspace μ) (Module.finrank K V)

theorem Module.End.genEigenspace_eq_genEigenspace_finrank_of_le {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) {k : ℕ} (hk : Module.finrank K V ≤ k) : (f.genEigenspace μ) k = (f.genEigenspace μ) (Module.finrank K V)

Generalized eigenspaces for exponents at least finrank K V are equal to each other.

theorem Module.End.mapsTo_genEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {g : Module.End R M} (h : Commute f g) (μ : R) (k : ℕ) : Set.MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)

theorem Module.End.mapsTo_iSup_genEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {g : Module.End R M} (h : Commute f g) (μ : R) : Set.MapsTo ⇑g ↑(⨆ (k : ℕ), (f.genEigenspace μ) k) ↑(⨆ (k : ℕ), (f.genEigenspace μ) k)

theorem Module.End.isNilpotent_restrict_sub_algebraMap {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ) (h : optParam (Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)) ⋯) : IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)

The restriction of f - μ • 1 to the k-fold generalized μ-eigenspace is nilpotent.

theorem Module.End.isNilpotent_restrict_iSup_sub_algebraMap {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) (h : optParam (Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑(⨆ (k : ℕ), (f.genEigenspace μ) k) ↑(⨆ (k : ℕ), (f.genEigenspace μ) k)) ⋯) : IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)

The restriction of f - μ • 1 to the generalized μ-eigenspace is nilpotent.

theorem Module.End.disjoint_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) {μ₁ : R} {μ₂ : R} (hμ : μ₁ ≠ μ₂) (k : ℕ) (l : ℕ) : Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)

theorem Module.End.disjoint_iSup_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) {μ₁ : R} {μ₂ : R} (hμ : μ₁ ≠ μ₂) : Disjoint (⨆ (k : ℕ), (f.genEigenspace μ₁) k) (⨆ (k : ℕ), (f.genEigenspace μ₂) k)

theorem Module.End.injOn_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) : Set.InjOn (fun (x : R) => ⨆ (k : ℕ), (f.genEigenspace x) k) {μ : R | ⨆ (k : ℕ), (f.genEigenspace μ) k ≠ ⊥}

theorem Module.End.independent_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) : CompleteLattice.Independent fun (μ : R) => ⨆ (k : ℕ), (f.genEigenspace μ) k

theorem Module.End.eigenspaces_independent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) : CompleteLattice.Independent f.eigenspace

The eigenspaces of a linear operator form an independent family of subspaces of M. That is, any eigenspace has trivial intersection with the span of all the other eigenspaces.

theorem Module.End.eigenvectors_linearIndependent' {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} [NoZeroSMulDivisors R M] (f : Module.End R M) (μ : ι → R) (hμ : Function.Injective μ) (v : ι → M) (h_eigenvec : ∀ (i : ι), f.HasEigenvector (μ i) (v i)) : LinearIndependent R v

Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent.

theorem Module.End.eigenvectors_linearIndependent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) (μs : Set R) (xs : ↑μs → M) (h_eigenvec : ∀ (μ : ↑μs), f.HasEigenvector (↑μ) (xs μ)) : LinearIndependent (ι := ↑μs) R xs

Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent. (Lemma 5.10 of [axler2015])

We use the eigenvalues as indexing set to ensure that there is only one eigenvector for each eigenvalue in the image of xs. See Module.End.eigenvectors_linearIndependent' for an indexed variant.

theorem Module.End.genEigenspace_restrict {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (p : Submodule R M) (k : ℕ) (μ : R) (hfp : ∀ x ∈ p, f x ∈ p) : (Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k = Submodule.comap p.subtype ((f.genEigenspace μ) k)

If f maps a subspace p into itself, then the generalized eigenspace of the restriction of f to p is the part of the generalized eigenspace of f that lies in p.

theorem Submodule.inf_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (p : Submodule R M) {k : ℕ} {μ : R} (hfp : ∀ x ∈ p, f x ∈ p) : p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype ((Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k)

theorem Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} {μ : ι → R} (f : ι → Module.End R M) (p : Submodule R M) (hfp : ∀ (i : ι), Set.MapsTo ⇑(f i) ↑p ↑p) : p ⊓ ⨅ (i : ι), (f i).maxGenEigenspace (μ i) = Submodule.map p.subtype (⨅ (i : ι), Module.End.maxGenEigenspace (LinearMap.restrict (f i) ⋯) (μ i))

Given a family of endomorphisms i ↦ f i, a family of candidate eigenvalues i ↦ μ i, and a submodule p which is invariant wrt every f i, the intersection of p with the simultaneous maximal generalised eigenspace (taken over all i), is the same as the simultaneous maximal generalised eigenspace of the f i restricted to p.

theorem Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_1} {μ : ι → R} (i : ι) (f : ι → Module.End R M) (h : ∀ (j : ι), Set.MapsTo ⇑(f j) ↑((f i).maxGenEigenspace (μ i)) ↑((f i).maxGenEigenspace (μ i))) : Submodule.map ((f i).maxGenEigenspace (μ i)).subtype (⨅ (j : ι), (fun (j : ι) => Module.End.maxGenEigenspace (LinearMap.restrict (f j) ⋯) (μ j)) j) = ⨅ (j : ι), (f j).maxGenEigenspace (μ j)

Given a family of endomorphisms i ↦ f i, a family of candidate eigenvalues i ↦ μ i, and a distinguished index i whose maximal generalised μ i-eigenspace is invariant wrt every f j, taking simultaneous maximal generalised eigenspaces is unaffected by first restricting to the distinguished generalised μ i-eigenspace.

theorem Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} (f : Module.End R M) (g : Module.End R M) (hf : Set.MapsTo ⇑f ↑p ↑p) (hg : Set.MapsTo ⇑g ↑p ↑p) {μ₁ : R} {μ₂ : R} (h : Set.MapsTo ⇑f ↑(g.maxGenEigenspace μ₁) ↑(g.maxGenEigenspace μ₂)) : Set.MapsTo ⇑(LinearMap.restrict f hf) ↑(Module.End.maxGenEigenspace (LinearMap.restrict g hg) μ₁) ↑(Module.End.maxGenEigenspace (LinearMap.restrict g hg) μ₂)

theorem Module.End.eigenspace_restrict_le_eigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) (μ : R) : Submodule.map p.subtype (Module.End.eigenspace (LinearMap.restrict f hfp) μ) ≤ f.eigenspace μ

If p is an invariant submodule of an endomorphism f, then the μ-eigenspace of the restriction of f to p is a submodule of the μ-eigenspace of f.

theorem Module.End.generalized_eigenvec_disjoint_range_ker {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) : Disjoint (f.genEigenrange μ (Module.finrank K V)) ((f.genEigenspace μ) (Module.finrank K V))

Generalized eigenrange and generalized eigenspace for exponent finrank K V are disjoint.

theorem Module.End.eigenspace_restrict_eq_bot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) {μ : R} (hμp : Disjoint (f.eigenspace μ) p) : Module.End.eigenspace (LinearMap.restrict f hfp) μ = ⊥

If an invariant subspace p of an endomorphism f is disjoint from the μ-eigenspace of f, then the restriction of f to p has trivial μ-eigenspace.

theorem Module.End.pos_finrank_genEigenspace_of_hasEigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {k : ℕ} {μ : K} (hx : f.HasEigenvalue μ) (hk : 0 < k) : 0 < Module.finrank K ↥((f.genEigenspace μ) k)

The generalized eigenspace of an eigenvalue has positive dimension for positive exponents.

theorem Module.End.map_genEigenrange_le {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {μ : K} {n : ℕ} : Submodule.map f (f.genEigenrange μ n) ≤ f.genEigenrange μ n

A linear map maps a generalized eigenrange into itself.

theorem Module.End.iSup_genEigenspace_le_smul {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (t : R) : ⨆ (k : ℕ), (f.genEigenspace μ) k ≤ ⨆ (k : ℕ), ((t • f).genEigenspace (t * μ)) k

theorem Module.End.iSup_genEigenspace_inf_le_add {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f₁ : Module.End R M) (f₂ : Module.End R M) (μ₁ : R) (μ₂ : R) (h : Commute f₁ f₂) : (⨆ (k : ℕ), (f₁.genEigenspace μ₁) k) ⊓ ⨆ (k : ℕ), (f₂.genEigenspace μ₂) k ≤ ⨆ (k : ℕ), ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) k

theorem Module.End.map_smul_of_iInf_genEigenspace_ne_bot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {L : Type u_1} {F : Type u_2} [SMul R L] [FunLike F L (Module.End R M)] [MulActionHomClass F R L (Module.End R M)] (f : F) (μ : L → R) (h_ne : ⨅ (x : L), ⨆ (k : ℕ), ((f x).genEigenspace (μ x)) k ≠ ⊥) (t : R) (x : L) : μ (t • x) = t • μ x

theorem Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {L : Type u_1} {F : Type u_2} [Add L] [FunLike F L (Module.End R M)] [AddHomClass F L (Module.End R M)] (f : F) (μ : L → R) (h_ne : ⨅ (x : L), ⨆ (k : ℕ), ((f x).genEigenspace (μ x)) k ≠ ⊥) (h : ∀ (x y : L), Commute (f x) (f y)) (x : L) (y : L) : μ (x + y) = μ x + μ y