Eigenvectors and eigenvalues

This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized counterparts. We follow Axler's approach [Axl15] 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
• https://en.wikipedia.org/wiki/Eigenvalues_and_eigenvectors

Tags

eigenspace, eigenvector, eigenvalue, eigen

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

The submodule unifEigenspace 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 = ∞.

Equations

• f.unifEigenspace μ = { toFun := fun (k : ℕ∞) => ⨆ (l : ℕ), ⨆ (_ : ↑l ≤ k), LinearMap.ker ((f - μ • 1) ^ l), monotone' := ⋯ }

theorem Module.End.mem_unifEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} {x : M} : x ∈ (f.unifEigenspace μ) k ↔ ∃ (l : ℕ), ↑l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

theorem Module.End.unifEigenspace_directed {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} : Directed (fun (x1 x2 : Submodule R M) => x1 ≤ x2) fun (l : { l : ℕ // ↑l ≤ k }) => (f.unifEigenspace μ) ↑↑l

theorem Module.End.mem_unifEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} {x : M} : x ∈ (f.unifEigenspace μ) ↑k ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

theorem Module.End.mem_unifEigenspace_top {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} : x ∈ (f.unifEigenspace μ) ⊤ ↔ ∃ (k : ℕ), x ∈ LinearMap.ker ((f - μ • 1) ^ k)

theorem Module.End.unifEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} : (f.unifEigenspace μ) ↑k = LinearMap.ker ((f - μ • 1) ^ k)

theorem Module.End.unifEigenspace_eq_iSup_unifEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ∞) : (f.unifEigenspace μ) k = ⨆ (l : { l : ℕ // ↑l ≤ k }), (f.unifEigenspace μ) ↑↑l

theorem Module.End.unifEigenspace_top {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : (f.unifEigenspace μ) ⊤ = ⨆ (k : ℕ), (f.unifEigenspace μ) ↑k

theorem Module.End.unifEigenspace_one {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} : (f.unifEigenspace μ) 1 = LinearMap.ker (f - μ • 1)

@[simp]

theorem Module.End.mem_unifEigenspace_one {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} : x ∈ (f.unifEigenspace μ) 1 ↔ f x = μ • x

theorem Module.End.mem_unifEigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} : x ∈ (f.unifEigenspace μ) 0 ↔ x = 0

@[simp]

theorem Module.End.unifEigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} : (f.unifEigenspace μ) 0 = ⊥

@[simp]

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

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

Let M be an R-module, and f an R-linear endomorphism of M, and let μ : R and k : ℕ∞ be given. Then x : M satisfies HasUnifEigenvector f μ k x if x ∈ f.unifEigenspace μ k and x ≠ 0.

For k = 1, this means that x is an eigenvector of f with eigenvalue μ.

Equations

• f.HasUnifEigenvector μ k x = (x ∈ (f.unifEigenspace μ) k ∧ x ≠ 0)

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

Let M be an R-module, and f an R-linear endomorphism of M. Then μ : R and k : ℕ∞ satisfy HasUnifEigenvalue f μ k if f.unifEigenspace μ k ≠ ⊥.

For k = 1, this means that μ is an eigenvalue of f.

Equations

• f.HasUnifEigenvalue μ k = ((f.unifEigenspace μ) k ≠ ⊥)

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

Let M be an R-module, and f an R-linear endomorphism of M. For k : ℕ∞, we define UnifEigenvalues f k to be the type of all μ : R that satisfy f.HasUnifEigenvalue μ k.

For k = 1 this is the type of all eigenvalues of f.

Equations

• f.UnifEigenvalues k = { μ : R // f.HasUnifEigenvalue μ k }

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

The underlying value of a bundled eigenvalue.

Equations

• ↑f k = Subtype.val

instance Module.End.UnifEigenvalues.instCoeOut {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (k : ℕ∞) : CoeOut (f.UnifEigenvalues k) R

Equations

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

instance Module.End.UnivEigenvalues.instDecidableEq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq R] (f : Module.End R M) (k : ℕ∞) : DecidableEq (f.UnifEigenvalues k)

Equations

• Module.End.UnivEigenvalues.instDecidableEq f k = inferInstanceAs (DecidableEq { x : R // f.HasUnifEigenvalue x k })

theorem Module.End.HasUnifEigenvector.hasUnifEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} {x : M} (h : f.HasUnifEigenvector μ k x) : f.HasUnifEigenvalue μ k

theorem Module.End.HasUnifEigenvector.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.HasUnifEigenvector μ 1 x) : f x = μ • x

theorem Module.End.HasUnifEigenvector.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.HasUnifEigenvector μ 1 v) (n : ℕ) : (f ^ n) v = μ ^ n • v

theorem Module.End.HasUnifEigenvalue.exists_hasUnifEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} (hμ : f.HasUnifEigenvalue μ k) : ∃ (v : M), f.HasUnifEigenvector μ k v

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

theorem Module.End.HasUnifEigenvalue.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.HasUnifEigenvalue μ 1) : IsNilpotent μ

A nilpotent endomorphism has nilpotent eigenvalues.

See also LinearMap.isNilpotent_trace_of_isNilpotent.

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

theorem Module.End.hasUnifEigenvalue_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.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f

theorem Module.End.HasUnifEigenvalue.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.HasUnifEigenvalue μ 1

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

theorem Module.End.unifEigenspace_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.unifEigenspace (a / b)) 1 = LinearMap.ker (b • f - a • 1)

def Module.End.unifEigenrange {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 if k is a natural number, or the infimum of these ranges if k = ∞.

Equations

• f.unifEigenrange μ k = ⨅ (l : ℕ), ⨅ (_ : ↑l ≤ k), LinearMap.range ((f - μ • 1) ^ l)

theorem Module.End.unifEigenrange_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ} : f.unifEigenrange μ ↑k = LinearMap.range ((f - μ • 1) ^ k)

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

The exponent of a generalized eigenvalue is never 0.

noncomputable def Module.End.maxUnifEigenspaceIndex {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.maxUnifEigenspaceIndex μ = monotonicSequenceLimitIndex ((f.unifEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)

theorem Module.End.unifEigenspace_top_eq_maxUnifEigenspaceIndex {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [h : IsNoetherian R M] (f : Module.End R M) (μ : R) : (f.unifEigenspace μ) ⊤ = (f.unifEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

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.unifEigenspace_le_unifEigenspace_maxUnifEigenspaceIndex {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) (k : ℕ∞) : (f.unifEigenspace μ) k ≤ (f.unifEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

theorem Module.End.unifEigenspace_eq_unifEigenspace_maxUnifEigenspaceIndex_of_le {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) {k : ℕ} (hk : f.maxUnifEigenspaceIndex μ ≤ k) : (f.unifEigenspace μ) ↑k = (f.unifEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

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

theorem Module.End.HasUnifEigenvalue.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.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m

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

theorem Module.End.HasUnifEigenvalue.lt {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} {m : ℕ∞} (hm : 0 < m) (hk : f.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m

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

@[simp]

theorem Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} (hk : 0 < k) : f.HasUnifEigenvalue μ k ↔ f.HasUnifEigenvalue μ 1

Generalized eigenvalues are actually just eigenvalues.

theorem Module.End.maxUnifEigenspaceIndex_le_finrank {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) : f.maxUnifEigenspaceIndex μ ≤ Module.finrank K V

theorem Module.End.unifEigenspace_le_unifEigenspace_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.unifEigenspace μ) k ≤ (f.unifEigenspace μ) ↑(Module.finrank K V)

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

theorem Module.End.unifEigenspace_eq_unifEigenspace_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.unifEigenspace μ) ↑k = (f.unifEigenspace μ) ↑(Module.finrank K V)

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

theorem Module.End.mapsTo_unifEigenspace_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.unifEigenspace μ) k) ↑((f.unifEigenspace μ) k)

theorem Module.End.isNilpotent_restrict_unifEigenspace_nat {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 - μ • 1) ↑((f.unifEigenspace μ) ↑k) ↑((f.unifEigenspace μ) ↑k)) ⋯) : IsNilpotent (LinearMap.restrict (f - μ • 1) h)

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

theorem Module.End.isNilpotent_restrict_unifEigenspace_top {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 - μ • 1) ↑((f.unifEigenspace μ) ⊤) ↑((f.unifEigenspace μ) ⊤)) ⋯) : IsNilpotent (LinearMap.restrict (f - μ • 1) h)

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

@[reducible, inline]

abbrev 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 [Axl15])

Equations

• f.eigenspace μ = (f.unifEigenspace μ) 1

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 - μ • 1)

@[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

@[reducible, inline]

abbrev 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 [Axl15])

Equations

• f.HasEigenvector μ x = f.HasUnifEigenvector μ 1 x

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

@[reducible, inline]

abbrev 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 [Axl15])

Equations

• f.HasEigenvalue a = f.HasUnifEigenvalue a 1

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 μ ≠ ⊥

@[reducible, inline]

abbrev 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 = f.UnifEigenvalues 1

@[reducible, inline]

abbrev 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 = ↑f 1

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 [Axl15]). 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 : ℕ) => (f.unifEigenspace μ) ↑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 - μ • 1) ^ 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)

@[reducible, inline]

abbrev 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 [Axl15])

Equations

• f.HasGenEigenvector μ k x = f.HasUnifEigenvector μ (↑k) x

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 ∈ (f.genEigenspace μ) k ∧ x ≠ 0

@[reducible, inline]

abbrev 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.HasUnifEigenvalue μ ↑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 ≠ ⊥

@[reducible, inline]

abbrev 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 = f.unifEigenrange μ ↑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 - μ • 1) ^ 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.

@[reducible, inline]

abbrev 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 μ = (f.unifEigenspace μ) ⊤

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

@[reducible, inline]

noncomputable abbrev 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 μ = f.maxUnifEigenspaceIndex μ

theorem Module.End.maxGenEigenspace_eq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [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 [Axl15])

@[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.iSup_genEigenspace_eq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) : ⨆ (k : ℕ), (f.genEigenspace μ) k = (f.unifEigenspace μ) ⊤

theorem Module.End.mapsTo_maxGenEigenspace_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 ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)

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_maxGenEigenspace_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)) μ) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)) ⋯) : 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.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_unifEigenspace {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.unifEigenspace μ₁) k) ((f.unifEigenspace μ₂) l)

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_maxGenEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) : CompleteLattice.Independent f.maxGenEigenspace

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 [Axl15])

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 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