Mathlib.LinearAlgebra.Eigenspace.Basic

Module.End.genEigenspace definition

(f : End R M) (μ : R) : ℕ∞ →o Submodule R M

Full source

/-- 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
(see Def 8.10 of [axler2015]), or the union of all these kernels if `k = ∞`.
A generalized eigenspace for some exponent `k` is contained in
the generalized eigenspace for exponents larger than `k`. -/
def genEigenspace (f : End R M) (μ : R) : ℕ∞ℕ∞ →o Submodule R M where
  toFun k := ⨆ l : ℕ, ⨆ _ : l ≤ k, LinearMap.ker ((f - μ • 1) ^ l)
  monotone' _ _ hkl := biSup_mono fun _ hi ↦ hi.trans hkl

Generalized eigenspace of a linear endomorphism

Informal description

For a linear endomorphism $ f $ of an $ R $-module $ M $ and a scalar $ \mu \in R $, the generalized eigenspace $ \text{genEigenspace}\, f\, \mu\, k $ for an extended natural number $ k \in \mathbb{N}_\infty $ is defined as the kernel of $ (f - \mu \cdot \text{id})^l $ for some natural number $ l \leq k $ if $ k $ is finite, or the union of all such kernels if $ k = \infty $. More precisely, for each $ k $, the generalized eigenspace is the supremum (union) of the kernels $ \text{ker}((f - \mu \cdot \text{id})^l) $ over all natural numbers $ l \leq k $. The function $ k \mapsto \text{genEigenspace}\, f\, \mu\, k $ is monotone in $ k $, meaning that larger values of $ k $ yield larger generalized eigenspaces.

Module.End.mem_genEigenspace theorem

 {f : End R M} {μ : R} {k : ℕ∞} {x : M} : x ∈ f.genEigenspace μ k ↔ ∃ l : ℕ, l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l)

Full source

lemma mem_genEigenspace {f : End R M} {μ : R} {k : ℕ∞} {x : M} :
    x ∈ f.genEigenspace μ kx ∈ f.genEigenspace μ k ↔ ∃ l : ℕ, l ≤ k ∧ x ∈ LinearMap.ker ((f - μ • 1) ^ l) := by
  have : Nonempty {l : ℕ // l ≤ k} := ⟨⟨0, zero_le _⟩⟩
  have : Directed (ι := { i : ℕ // i ≤ k }) (· ≤ ·) fun i ↦ LinearMap.ker ((f - μ • 1) ^ (i : ℕ)) :=
    Monotone.directed_le fun m n h ↦ by simpa using (f - μ • 1).iterateKer.monotone h
  simp_rw [genEigenspace, OrderHom.coe_mk, LinearMap.mem_ker, iSup_subtype',
    Submodule.mem_iSup_of_directed _ this, LinearMap.mem_ker, Subtype.exists, exists_prop]

Characterization of Membership in Generalized Eigenspace: $x \in \text{genEigenspace}\, f\, \mu\, k \leftrightarrow \exists l \leq k, x \in \ker((f - \mu \cdot \text{id})^l)$

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k \in \mathbb{N}_\infty$ an extended natural number. For any $x \in M$, the element $x$ belongs to the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ if and only if there exists a natural number $l \leq k$ such that $x$ is in the kernel of $(f - \mu \cdot \text{id})^l$.

Module.End.genEigenspace_directed theorem

{f : End R M} {μ : R} {k : ℕ∞} : Directed (· ≤ ·) (fun l : { l : ℕ // l ≤ k } ↦ f.genEigenspace μ l)

Full source

lemma genEigenspace_directed {f : End R M} {μ : R} {k : ℕ∞} :
    Directed (· ≤ ·) (fun l : {l : ℕ // l ≤ k} ↦ f.genEigenspace μ l) := by
  have aux : Monotone ((↑) : {l : ℕ // l ≤ k} → ℕ∞) := fun x y h ↦ by simpa using h
  exact ((genEigenspace f μ).monotone.comp aux).directed_le

Directedness of Generalized Eigenspaces with Respect to Inclusion

Informal description

For a linear endomorphism $ f $ of an $ R $-module $ M $, a scalar $ \mu \in R $, and an extended natural number $ k \in \mathbb{N}_\infty $, the family of generalized eigenspaces $ \text{genEigenspace}\, f\, \mu\, l $ indexed by natural numbers $ l \leq k $ is directed with respect to the inclusion relation $ \subseteq $. That is, for any two natural numbers $ l_1, l_2 \leq k $, there exists a natural number $ l_3 \leq k $ such that both $ \text{genEigenspace}\, f\, \mu\, l_1 \subseteq \text{genEigenspace}\, f\, \mu\, l_3 $ and $ \text{genEigenspace}\, f\, \mu\, l_2 \subseteq \text{genEigenspace}\, f\, \mu\, l_3 $.

Module.End.mem_genEigenspace_nat theorem

{f : End R M} {μ : R} {k : ℕ} {x : M} : x ∈ f.genEigenspace μ k ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Full source

lemma mem_genEigenspace_nat {f : End R M} {μ : R} {k : ℕ} {x : M} :
    x ∈ f.genEigenspace μ kx ∈ f.genEigenspace μ k ↔ x ∈ LinearMap.ker ((f - μ • 1) ^ k) := by
  rw [mem_genEigenspace]
  constructor
  · rintro ⟨l, hl, hx⟩
    simp only [Nat.cast_le] at hl
    exact (f - μ • 1).iterateKer.monotone hl hx
  · intro hx
    exact ⟨k, le_rfl, hx⟩

Characterization of Membership in Finite-Dimensional Generalized Eigenspace: $x \in \text{genEigenspace}\, f\, \mu\, k \leftrightarrow (f - \mu \cdot \text{id})^k x = 0$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a natural number $k \in \mathbb{N}$, a vector $x \in M$ belongs to the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ if and only if $x$ is in the kernel of the linear map $(f - \mu \cdot \text{id})^k$, i.e., $(f - \mu \cdot \text{id})^k x = 0$.

Module.End.mem_genEigenspace_top theorem

{f : End R M} {μ : R} {x : M} : x ∈ f.genEigenspace μ ⊤ ↔ ∃ k : ℕ, x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Full source

lemma mem_genEigenspace_top {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ ⊤x ∈ f.genEigenspace μ ⊤ ↔ ∃ k : ℕ, x ∈ LinearMap.ker ((f - μ • 1) ^ k) := by
  simp [mem_genEigenspace]

Characterization of Vectors in the Generalized Eigenspace at Infinity

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a vector $x \in M$, the following are equivalent: 1. $x$ belongs to the generalized eigenspace of $f$ at $\mu$ with index $\infty$ (i.e., $x \in \text{genEigenspace}\, f\, \mu\, \infty$). 2. There exists a natural number $k$ such that $x$ is in the kernel of $(f - \mu \cdot \text{id})^k$.

Module.End.genEigenspace_nat theorem

{f : End R M} {μ : R} {k : ℕ} : f.genEigenspace μ k = LinearMap.ker ((f - μ • 1) ^ k)

Full source

lemma genEigenspace_nat {f : End R M} {μ : R} {k : ℕ} :
    f.genEigenspace μ k = LinearMap.ker ((f - μ • 1) ^ k) := by
  ext; simp [mem_genEigenspace_nat]

Generalized Eigenspace as Kernel of Power Map

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a natural number $k \in \mathbb{N}$, the generalized eigenspace of $f$ at $\mu$ for $k$ is equal to the kernel of the linear map $(f - \mu \cdot \text{id})^k$. That is, \[ \text{genEigenspace}\, f\, \mu\, k = \ker((f - \mu \cdot \text{id})^k). \]

Module.End.genEigenspace_eq_iSup_genEigenspace_nat theorem

(f : End R M) (μ : R) (k : ℕ∞) : f.genEigenspace μ k = ⨆ l : { l : ℕ // l ≤ k }, f.genEigenspace μ l

Full source

lemma genEigenspace_eq_iSup_genEigenspace_nat (f : End R M) (μ : R) (k : ℕ∞) :
    f.genEigenspace μ k = ⨆ l : {l : ℕ // l ≤ k}, f.genEigenspace μ l := by
  simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]

Generalized Eigenspace as Supremum of Finite-Dimensional Eigenspaces

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and an extended natural number $k \in \mathbb{N}_\infty$, the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ is equal to the supremum (union) of the generalized eigenspaces $\text{genEigenspace}(f, \mu, l)$ over all natural numbers $l \leq k$. That is, \[ \text{genEigenspace}(f, \mu, k) = \bigsqcup_{\substack{l \in \mathbb{N} \\ l \leq k}} \text{genEigenspace}(f, \mu, l). \]

Module.End.genEigenspace_top theorem

(f : End R M) (μ : R) : f.genEigenspace μ ⊤ = ⨆ k : ℕ, f.genEigenspace μ k

Full source

lemma genEigenspace_top (f : End R M) (μ : R) :
    f.genEigenspace μ ⊤ = ⨆ k : ℕ, f.genEigenspace μ k := by
  rw [genEigenspace_eq_iSup_genEigenspace_nat, iSup_subtype]
  simp only [le_top, iSup_pos, OrderHom.coe_mk]

Generalized Eigenspace at Infinity as Union of Finite-Dimensional Eigenspaces

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the generalized eigenspace of $f$ at $\mu$ for $k = \infty$ (denoted $\top$) is equal to the union of all generalized eigenspaces $\text{genEigenspace}(f, \mu, k)$ over all natural numbers $k \in \mathbb{N}$. That is, \[ \text{genEigenspace}(f, \mu, \infty) = \bigcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k). \]

Module.End.genEigenspace_one theorem

{f : End R M} {μ : R} : f.genEigenspace μ 1 = LinearMap.ker (f - μ • 1)

Full source

lemma genEigenspace_one {f : End R M} {μ : R} :
    f.genEigenspace μ 1 = LinearMap.ker (f - μ • 1) := by
  rw [← Nat.cast_one, genEigenspace_nat, pow_one]

Generalized Eigenspace for $k=1$ as Kernel of $f - \mu \cdot \text{id}$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the generalized eigenspace of $f$ at $\mu$ for $k = 1$ is equal to the kernel of the linear map $f - \mu \cdot \text{id}$. That is, \[ \text{genEigenspace}(f, \mu, 1) = \ker(f - \mu \cdot \text{id}). \]

Module.End.mem_genEigenspace_one theorem

{f : End R M} {μ : R} {x : M} : x ∈ f.genEigenspace μ 1 ↔ f x = μ • x

Full source

@[simp]
lemma mem_genEigenspace_one {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ 1x ∈ f.genEigenspace μ 1 ↔ f x = μ • x := by
  rw [genEigenspace_one, LinearMap.mem_ker, LinearMap.sub_apply,
    sub_eq_zero, LinearMap.smul_apply, Module.End.one_apply]

Characterization of Generalized Eigenspace for $k=1$: $x \in \text{genEigenspace}(f, \mu, 1) \leftrightarrow f(x) = \mu x$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a vector $x \in M$, the vector $x$ belongs to the generalized eigenspace of $f$ at $\mu$ for $k=1$ if and only if $f(x) = \mu \cdot x$.

Module.End.mem_genEigenspace_zero theorem

{f : End R M} {μ : R} {x : M} : x ∈ f.genEigenspace μ 0 ↔ x = 0

Full source

lemma mem_genEigenspace_zero {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ 0x ∈ f.genEigenspace μ 0 ↔ x = 0 := by
  rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]

Generalized Eigenspace for $k=0$ Contains Only Zero Vector

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a vector $x \in M$, the vector $x$ belongs to the generalized eigenspace of $f$ at $\mu$ for $k=0$ if and only if $x$ is the zero vector. That is, \[ x \in \text{genEigenspace}(f, \mu, 0) \leftrightarrow x = 0. \]

Module.End.genEigenspace_zero theorem

{f : End R M} {μ : R} : f.genEigenspace μ 0 = ⊥

Full source

@[simp]
lemma genEigenspace_zero {f : End R M} {μ : R} :
    f.genEigenspace μ 0 = ⊥ := by
  ext; apply mem_genEigenspace_zero

Generalized Eigenspace for k=0 is Trivial

Informal description

For any linear endomorphism $f$ of an $R$-module $M$ and any scalar $\mu \in R$, the generalized eigenspace of $f$ at $\mu$ for $k=0$ is the trivial submodule $\{0\}$. That is, \[ \text{genEigenspace}(f, \mu, 0) = 0. \]

Module.End.genEigenspace_zero_nat theorem

(f : End R M) (k : ℕ) : f.genEigenspace 0 k = LinearMap.ker (f ^ k)

Full source

@[simp]
lemma genEigenspace_zero_nat (f : End R M) (k : ℕ) :
    f.genEigenspace 0 k = LinearMap.ker (f ^ k) := by
  ext; simp [mem_genEigenspace_nat]

Generalized Eigenspace at Zero Equals Kernel of Power

Informal description

For any linear endomorphism $ f $ of an $ R $-module $ M $ and any natural number $ k $, the generalized eigenspace of $ f $ at the scalar $ 0 $ for $ k $ is equal to the kernel of $ f^k $. That is, \[ \text{genEigenspace}\, f\, 0\, k = \ker(f^k). \]

Module.End.HasUnifEigenvector definition

(f : End R M) (μ : R) (k : ℕ∞) (x : M) : Prop

Full source

/-- 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.genEigenspace μ k` and `x ≠ 0`.

For `k = 1`, this means that `x` is an eigenvector of `f` with eigenvalue `μ`. -/
def HasUnifEigenvector (f : End R M) (μ : R) (k : ℕ∞) (x : M) : Prop :=
  x ∈ f.genEigenspace μ kx ∈ f.genEigenspace μ k ∧ x ≠ 0

Uniform eigenvector of a linear endomorphism

Informal description

Given an $ R $-module $ M $, a linear endomorphism $ f $ of $ M $, a scalar $ \mu \in R $, and an extended natural number $ k \in \mathbb{N}_\infty $, a vector $ x \in M $ is called a *uniform eigenvector* of $ f $ with eigenvalue $ \mu $ and order $ k $ if $ x $ is a nonzero element of the generalized eigenspace $ \text{genEigenspace}\, f\, \mu\, k $. For $ k = 1 $, this means $ x $ is an eigenvector of $ f $ with eigenvalue $ \mu $, i.e., $ f x = \mu \cdot x $ and $ x \neq 0 $. For $ k > 1 $, $ x $ is a generalized eigenvector, meaning $ x $ is in the kernel of $ (f - \mu \cdot \text{id})^k $ but not necessarily in the kernel of $ (f - \mu \cdot \text{id}) $.

Module.End.HasUnifEigenvalue definition

(f : End R M) (μ : R) (k : ℕ∞) : Prop

Full source

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

For `k = 1`, this means that `μ` is an eigenvalue of `f`. -/
def HasUnifEigenvalue (f : End R M) (μ : R) (k : ℕ∞) : Prop :=
  f.genEigenspace μ k ≠ ⊥

Uniform eigenvalue condition for linear endomorphisms

Informal description

Given an $ R $-module $ M $ and a linear endomorphism $ f $ of $ M $, a scalar $ \mu \in R $ and an extended natural number $ k \in \mathbb{N}_\infty $ satisfy `HasUnifEigenvalue f μ k` if the generalized eigenspace $ \text{genEigenspace}\, f\, \mu\, k $ is nontrivial (i.e., not equal to the zero subspace). For $ k = 1 $, this means that $ \mu $ is an eigenvalue of $ f $, i.e., there exists a nonzero vector $ x \in M $ such that $ f x = \mu x $.

Module.End.UnifEigenvalues definition

(f : End R M) (k : ℕ∞) : Type _

Full source

/-- 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`. -/
def UnifEigenvalues (f : End R M) (k : ℕ∞) : Type _ :=
  { μ : R // f.HasUnifEigenvalue μ k }

Uniform eigenvalues of a linear endomorphism

Informal description

Given an $ R $-module $ M $ and a linear endomorphism $ f $ of $ M $, the type `UnifEigenvalues f k` consists of all scalars $ \mu \in R $ that satisfy the condition `HasUnifEigenvalue f μ k`, i.e., for which the generalized eigenspace of $ f $ at $ \mu $ with order $ k $ is nontrivial. For $ k = 1 $, this is precisely the type of eigenvalues of $ f $, meaning scalars $ \mu $ for which there exists a nonzero vector $ x \in M $ such that $ f x = \mu x $.

Module.End.UnifEigenvalues.val definition

(f : Module.End R M) (k : ℕ∞) : UnifEigenvalues f k → R

Full source

/-- The underlying value of a bundled eigenvalue. -/
@[coe]
def UnifEigenvalues.val (f : Module.End R M) (k : ℕ∞) : UnifEigenvalues f k → R := Subtype.val

Underlying scalar of a bundled eigenvalue

Informal description

The function maps a bundled eigenvalue $\mu$ of a linear endomorphism $f$ with respect to an extended natural number $k$ to its underlying scalar value in $R$. In other words, it extracts the scalar $\mu$ from the type `UnifEigenvalues f k`.

Module.End.UnifEigenvalues.instCoeOut instance

{f : Module.End R M} (k : ℕ∞) : CoeOut (UnifEigenvalues f k) R

Full source

instance UnifEigenvalues.instCoeOut {f : Module.End R M} (k : ℕ∞) :
    CoeOut (UnifEigenvalues f k) R where
  coe := UnifEigenvalues.val f k

Coercion from Uniform Eigenvalues to Scalars

Informal description

For any $R$-module $M$, linear endomorphism $f$ of $M$, and extended natural number $k \in \mathbb{N}_\infty$, there is a canonical way to view an element of the type `UnifEigenvalues f k` (uniform eigenvalues of $f$ of order $k$) as an element of $R$. Specifically, this instance provides the coercion from `UnifEigenvalues f k` to $R$, allowing uniform eigenvalues to be treated directly as scalars in $R$.

Module.End.UnivEigenvalues.instDecidableEq instance

[DecidableEq R] (f : Module.End R M) (k : ℕ∞) : DecidableEq (UnifEigenvalues f k)

Full source

instance UnivEigenvalues.instDecidableEq [DecidableEq R] (f : Module.End R M) (k : ℕ∞) :
    DecidableEq (UnifEigenvalues f k) :=
  inferInstanceAs (DecidableEq (Subtype (fun x : R ↦ f.HasUnifEigenvalue x k)))

Decidability of Equality for Uniform Eigenvalues of a Linear Endomorphism

Informal description

For any module $M$ over a ring $R$ with decidable equality, given a linear endomorphism $f$ of $M$ and an extended natural number $k \in \mathbb{N}_\infty$, the type of uniform eigenvalues of $f$ of order $k$ has decidable equality. That is, for any two uniform eigenvalues $\mu_1, \mu_2$ of $f$ of order $k$, it is decidable whether $\mu_1 = \mu_2$.

Module.End.HasUnifEigenvector.hasUnifEigenvalue theorem

{f : End R M} {μ : R} {k : ℕ∞} {x : M} (h : f.HasUnifEigenvector μ k x) : f.HasUnifEigenvalue μ k

Full source

lemma HasUnifEigenvector.hasUnifEigenvalue {f : End R M} {μ : R} {k : ℕ∞} {x : M}
    (h : f.HasUnifEigenvector μ k x) : f.HasUnifEigenvalue μ k := by
  rw [HasUnifEigenvalue, Submodule.ne_bot_iff]
  use x; exact h

Existence of Uniform Eigenvalue from Uniform Eigenvector

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. For a scalar $\mu \in R$ and an extended natural number $k \in \mathbb{N}_\infty$, if there exists a nonzero vector $x \in M$ such that $x$ is a uniform eigenvector of $f$ with eigenvalue $\mu$ and order $k$, then $\mu$ is a uniform eigenvalue of $f$ of order $k$. In other words, if $x \neq 0$ and $x$ belongs to the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$, then the generalized eigenspace is nontrivial.

Module.End.HasUnifEigenvector.apply_eq_smul theorem

{f : End R M} {μ : R} {x : M} (hx : f.HasUnifEigenvector μ 1 x) : f x = μ • x

Full source

lemma HasUnifEigenvector.apply_eq_smul {f : End R M} {μ : R} {x : M}
    (hx : f.HasUnifEigenvector μ 1 x) : f x = μ • x :=
  mem_genEigenspace_one.mp hx.1

Action of Linear Endomorphism on Uniform Eigenvector: $f(x) = \mu x$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, if $x$ is a uniform eigenvector of $f$ with eigenvalue $\mu$ and order $1$, then $f(x) = \mu \cdot x$.

Module.End.HasUnifEigenvector.pow_apply theorem

{f : End R M} {μ : R} {v : M} (hv : f.HasUnifEigenvector μ 1 v) (n : ℕ) : (f ^ n) v = μ ^ n • v

Full source

lemma HasUnifEigenvector.pow_apply {f : End R M} {μ : R} {v : M} (hv : f.HasUnifEigenvector μ 1 v)
    (n : ℕ) : (f ^ n) v = μ ^ n • v := by
  induction n <;> simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

Iterated Action on Eigenvector: $f^n(v) = \mu^n v$

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. If $v$ is a uniform eigenvector of $f$ with eigenvalue $\mu$ and order $1$, then for any natural number $n$, the $n$-th iterate of $f$ applied to $v$ equals $\mu^n$ times $v$, i.e., \[ f^n(v) = \mu^n \cdot v. \]

Module.End.HasUnifEigenvalue.exists_hasUnifEigenvector theorem

{f : End R M} {μ : R} {k : ℕ∞} (hμ : f.HasUnifEigenvalue μ k) : ∃ v, f.HasUnifEigenvector μ k v

Full source

theorem HasUnifEigenvalue.exists_hasUnifEigenvector
    {f : End R M} {μ : R} {k : ℕ∞} (hμ : f.HasUnifEigenvalue μ k) :
    ∃ v, f.HasUnifEigenvector μ k v :=
  Submodule.exists_mem_ne_zero_of_ne_bot hμ

Existence of Uniform Eigenvectors for Uniform Eigenvalues

Informal description

For any linear endomorphism $ f $ of an $ R $-module $ M $, if $ \mu $ is a uniform eigenvalue of $ f $ of order $ k \in \mathbb{N}_\infty $, then there exists a vector $ v \in M $ such that $ v $ is a uniform eigenvector of $ f $ with eigenvalue $ \mu $ and order $ k $.

Module.End.HasUnifEigenvalue.pow theorem

{f : End R M} {μ : R} (h : f.HasUnifEigenvalue μ 1) (n : ℕ) : (f ^ n).HasUnifEigenvalue (μ ^ n) 1

Full source

lemma HasUnifEigenvalue.pow {f : End R M} {μ : R} (h : f.HasUnifEigenvalue μ 1) (n : ℕ) :
    (f ^ n).HasUnifEigenvalue (μ ^ n) 1 := by
  rw [HasUnifEigenvalue, Submodule.ne_bot_iff]
  obtain ⟨m : M, hm⟩ := h.exists_hasUnifEigenvector
  exact ⟨m, by simpa [mem_genEigenspace_one] using hm.pow_apply n, hm.2⟩

Eigenvalues of Iterated Endomorphism: $\mu^n$ is an eigenvalue of $f^n$ if $\mu$ is an eigenvalue of $f$

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. If $\mu$ is an eigenvalue of $f$ (i.e., $f$ has a uniform eigenvalue $\mu$ of order 1), then for any natural number $n$, the scalar $\mu^n$ is an eigenvalue of the $n$-th iterate $f^n$ (i.e., $f^n$ has a uniform eigenvalue $\mu^n$ of order 1).

Module.End.HasUnifEigenvalue.isNilpotent_of_isNilpotent theorem

[NoZeroSMulDivisors R M] {f : End R M} (hfn : IsNilpotent f) {μ : R} (hf : f.HasUnifEigenvalue μ 1) : IsNilpotent μ

Full source

/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`. -/
lemma HasUnifEigenvalue.isNilpotent_of_isNilpotent [NoZeroSMulDivisors R M] {f : End R M}
    (hfn : IsNilpotent f) {μ : R} (hf : f.HasUnifEigenvalue μ 1) :
    IsNilpotent μ := by
  obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector
  obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn
  exact ⟨n, by simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n⟩

Nilpotency of Eigenvalues for Nilpotent Endomorphisms

Informal description

Let $M$ be a module over a ring $R$ with no zero scalar divisors, and let $f$ be a nilpotent $R$-linear endomorphism of $M$. If $\mu$ is an eigenvalue of $f$ (i.e., there exists a nonzero vector $v \in M$ such that $f(v) = \mu v$), then $\mu$ is a nilpotent element of $R$.

Module.End.HasUnifEigenvalue.mem_spectrum theorem

{f : End R M} {μ : R} (hμ : HasUnifEigenvalue f μ 1) : μ ∈ spectrum R f

Full source

lemma HasUnifEigenvalue.mem_spectrum {f : End R M} {μ : R} (hμ : HasUnifEigenvalue f μ 1) :
    μ ∈ spectrum R f := by
  refine spectrum.mem_iff.mpr fun h_unit ↦ ?_
  set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
  rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩
  refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))
  rw [hv.apply_eq_smul, sub_self]

Eigenvalues Belong to Spectrum: $\mu \in \text{spectrum}(f)$ if $\mu$ is an eigenvalue of $f$

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, if $\mu$ is an eigenvalue of $f$ (i.e., there exists a nonzero vector $v \in M$ such that $f(v) = \mu v$), then $\mu$ belongs to the spectrum of $f$ (i.e., the linear map $f - \mu \cdot \text{id}$ is not invertible).

Module.End.hasUnifEigenvalue_iff_mem_spectrum theorem

[FiniteDimensional K V] {f : End K V} {μ : K} : f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f

Full source

lemma hasUnifEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
    f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f := by
  rw [spectrum.mem_iff, IsUnit.sub_iff, LinearMap.isUnit_iff_ker_eq_bot,
    HasUnifEigenvalue, genEigenspace_one, ne_eq, not_iff_not]
  simp [Submodule.ext_iff, LinearMap.mem_ker]

Equivalence of Eigenvalues and Spectrum in Finite Dimensions: $\mu$ is an eigenvalue of $f$ if and only if $\mu \in \text{spectrum}(f)$

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f : V \to V$ be a linear endomorphism. For any scalar $\mu \in K$, the following are equivalent: 1. $\mu$ is an eigenvalue of $f$ (i.e., there exists a nonzero vector $v \in V$ such that $f(v) = \mu v$). 2. $\mu$ belongs to the spectrum of $f$ (i.e., the linear map $f - \mu \cdot \text{id}$ is not invertible).

Module.End.genEigenspace_div theorem

(f : End K V) (a b : K) (hb : b ≠ 0) : genEigenspace f (a / b) 1 = LinearMap.ker (b • f - a • 1)

Full source

lemma genEigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
    genEigenspace f (a / b) 1 = LinearMap.ker (b • f - a • 1) :=
  calc
    genEigenspace f (a / b) 1 = genEigenspace f (b⁻¹ * a) 1 := by rw [div_eq_mul_inv, mul_comm]
    _ = LinearMap.ker (f - (b⁻¹ * a) • 1)     := by rw [genEigenspace_one]
    _ = LinearMap.ker (f - b⁻¹ • a • 1)       := by rw [smul_smul]
    _ = LinearMap.ker (b • (f - b⁻¹ • a • 1)) := by rw [LinearMap.ker_smul _ b hb]
    _ = LinearMap.ker (b • f - a • 1)         := by rw [smul_sub, smul_inv_smul₀ hb]

Generalized Eigenspace for $\frac{a}{b}$ as Kernel of $b f - a \text{id}$

Informal description

Let $f$ be a linear endomorphism of a vector space $V$ over a field $K$, and let $a, b \in K$ with $b \neq 0$. The generalized eigenspace of $f$ corresponding to the eigenvalue $\frac{a}{b}$ and exponent $1$ is equal to the kernel of the linear map $b f - a \text{id}$. That is, \[ \text{genEigenspace}(f, \tfrac{a}{b}, 1) = \ker(b f - a \cdot \text{id}). \]

Module.End.genEigenrange definition

(f : End R M) (μ : R) (k : ℕ∞) : Submodule R M

Full source

/-- 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 = ∞`. -/
def genEigenrange (f : End R M) (μ : R) (k : ℕ∞) : Submodule R M :=
  ⨅ l : ℕ, ⨅ (_ : l ≤ k), LinearMap.range ((f - μ • 1) ^ l)

Generalized eigenrange of a linear endomorphism

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and an exponent $k \in \mathbb{N} \cup \{\infty\}$, the generalized eigenrange is defined as: - When $k \in \mathbb{N}$, it is the range of $(f - \mu \cdot \text{id})^k$ - When $k = \infty$, it is the infimum of the ranges of $(f - \mu \cdot \text{id})^l$ for all $l \in \mathbb{N}$

Module.End.genEigenrange_nat theorem

{f : End R M} {μ : R} {k : ℕ} : f.genEigenrange μ k = LinearMap.range ((f - μ • 1) ^ k)

Full source

lemma genEigenrange_nat {f : End R M} {μ : R} {k : ℕ} :
    f.genEigenrange μ k = LinearMap.range ((f - μ • 1) ^ k) := by
  ext x
  simp only [genEigenrange, Nat.cast_le, Submodule.mem_iInf, LinearMap.mem_range]
  constructor
  · intro h
    exact h _ le_rfl
  · rintro ⟨x, rfl⟩ i hi
    have : k = i + (k - i) := by omega
    rw [this, pow_add]
    exact ⟨_, rfl⟩

Generalized Eigenrange as Range of $(f - \mu \cdot \text{id})^k$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a natural number $k$, the generalized eigenrange of $f$ at $\mu$ with exponent $k$ is equal to the range of the linear map $(f - \mu \cdot \text{id})^k$.

Module.End.HasUnifEigenvalue.exp_ne_zero theorem

{f : End R M} {μ : R} {k : ℕ} (h : f.HasUnifEigenvalue μ k) : k ≠ 0

Full source

/-- The exponent of a generalized eigenvalue is never 0. -/
lemma HasUnifEigenvalue.exp_ne_zero {f : End R M} {μ : R} {k : ℕ}
    (h : f.HasUnifEigenvalue μ k) : k ≠ 0 := by
  rintro rfl
  simp [HasUnifEigenvalue, Nat.cast_zero, genEigenspace_zero] at h

Nonzero Exponent Property for Generalized Eigenvalues

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, scalar $\mu \in R$, and natural number $k$, if $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ (i.e., the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ is nontrivial), then $k \neq 0$.

Module.End.maxUnifEigenspaceIndex definition

(f : End R M) (μ : R)

Full source

/-- 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. -/
noncomputable def maxUnifEigenspaceIndex (f : End R M) (μ : R) :=
  monotonicSequenceLimitIndex <| (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom

Minimal exponent for maximal generalized eigenspace

Informal description

For a linear endomorphism $ f $ of an $ R $-module $ M $ and a scalar $ \mu \in R $, the function `maxUnifEigenspaceIndex f μ` returns the smallest natural number $ k $ such that the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is maximal (i.e., equal to $\text{genEigenspace}\, f\, \mu\, \infty$). If no such $ k $ exists, the result is still defined but has no meaningful interpretation.

Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex theorem

[IsNoetherian R M] (f : End R M) (μ : R) : genEigenspace f μ ⊤ = f.genEigenspace μ (maxUnifEigenspaceIndex f μ)

Full source

/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
`(f - μ • id) ^ k` for some `k`. -/
lemma genEigenspace_top_eq_maxUnifEigenspaceIndex [IsNoetherian R M] (f : End R M) (μ : R) :
    genEigenspace f μ ⊤ = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) := by
  have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <|
    (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom
  convert this using 1
  simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe,
    Function.comp_def]
  rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]
  congr
  aesop

Maximal Generalized Eigenspace Equals Minimal Exponent Eigenspace in Noetherian Modules

Informal description

Let $R$ be a ring and $M$ a Noetherian $R$-module. For any endomorphism $f$ of $M$ and scalar $\mu \in R$, the maximal generalized eigenspace $\text{genEigenspace}\, f\, \mu\, \infty$ (where $\infty$ denotes the top element of $\mathbb{N}_\infty$) equals the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ where $k$ is the minimal natural number such that $\text{genEigenspace}\, f\, \mu\, k$ is maximal (i.e., $\text{genEigenspace}\, f\, \mu\, k = \text{genEigenspace}\, f\, \mu\, \infty$).

Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex theorem

 [IsNoetherian R M] (f : End R M) (μ : R) (k : ℕ∞) :
  f.genEigenspace μ k ≤ f.genEigenspace μ (maxUnifEigenspaceIndex f μ)

Full source

lemma genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex [IsNoetherian R M] (f : End R M)
    (μ : R) (k : ℕ∞) :
    f.genEigenspace μ k ≤ f.genEigenspace μ (maxUnifEigenspaceIndex f μ) := by
  rw [← genEigenspace_top_eq_maxUnifEigenspaceIndex]
  exact (f.genEigenspace μ).monotone le_top

Generalized Eigenspace Containment in Maximal Eigenspace for Noetherian Modules

Informal description

Let $R$ be a ring and $M$ a Noetherian $R$-module. For any linear endomorphism $f$ of $M$, scalar $\mu \in R$, and extended natural number $k \in \mathbb{N}_\infty$, the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is contained in the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k_{\text{max}}$, where $k_{\text{max}}$ is the minimal natural number such that $\text{genEigenspace}\, f\, \mu\, k_{\text{max}}$ is maximal.

Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le theorem

 [IsNoetherian R M] (f : End R M) (μ : R) {k : ℕ} (hk : maxUnifEigenspaceIndex f μ ≤ k) :
  f.genEigenspace μ k = f.genEigenspace μ (maxUnifEigenspaceIndex f μ)

Full source

/-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other. -/
theorem genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le [IsNoetherian R M]
    (f : End R M) (μ : R) {k : ℕ} (hk : maxUnifEigenspaceIndex f μ ≤ k) :
    f.genEigenspace μ k = f.genEigenspace μ (maxUnifEigenspaceIndex f μ) :=
  le_antisymm
    (genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex _ _ _)
    ((f.genEigenspace μ).monotone <| by simpa using hk)

Stabilization of Generalized Eigenspaces for Exponents Above Critical Index

Informal description

Let $R$ be a ring and $M$ a Noetherian $R$-module. For any linear endomorphism $f$ of $M$, scalar $\mu \in R$, and natural number $k$ such that $k \geq \text{maxUnifEigenspaceIndex}\, f\, \mu$, the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ equals the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, (\text{maxUnifEigenspaceIndex}\, f\, \mu)$.

Module.End.HasUnifEigenvalue.le theorem

{f : End R M} {μ : R} {k m : ℕ∞} (hm : k ≤ m) (hk : f.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m

Full source

/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for exponents larger than `k`. -/
lemma HasUnifEigenvalue.le {f : End R M} {μ : R} {k m : ℕ∞}
    (hm : k ≤ m) (hk : f.HasUnifEigenvalue μ k) :
    f.HasUnifEigenvalue μ m := by
  unfold HasUnifEigenvalue at *
  contrapose! hk
  rw [← le_bot_iff, ← hk]
  exact (f.genEigenspace _).monotone hm

Generalized Eigenvalue Persistence: $\text{HasUnifEigenvalue}\, f\, \mu\, k \to k \leq m \to \text{HasUnifEigenvalue}\, f\, \mu\, m$

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k, m \in \mathbb{N}_\infty$ extended natural numbers. If $k \leq m$ and $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ (i.e., the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is nontrivial), then $\mu$ is also a generalized eigenvalue of $f$ with exponent $m$.

Module.End.HasUnifEigenvalue.lt theorem

{f : End R M} {μ : R} {k m : ℕ∞} (hm : 0 < m) (hk : f.HasUnifEigenvalue μ k) : f.HasUnifEigenvalue μ m

Full source

/-- A generalized eigenvalue for some exponent `k` is also
a generalized eigenvalue for positive exponents. -/
lemma HasUnifEigenvalue.lt {f : End R M} {μ : R} {k m : ℕ∞}
    (hm : 0 < m) (hk : f.HasUnifEigenvalue μ k) :
    f.HasUnifEigenvalue μ m := by
  apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)
  intro contra; apply hk
  rw [genEigenspace_one, LinearMap.ker_eq_bot] at contra
  rw [eq_bot_iff]
  intro x hx
  rw [mem_genEigenspace] at hx
  rcases hx with ⟨l, -, hx⟩
  rwa [LinearMap.ker_eq_bot.mpr] at hx
  rw [Module.End.coe_pow (f - μ • 1) l]
  exact Function.Injective.iterate contra l

Generalized Eigenvalue Persistence for Positive Exponents

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k, m \in \mathbb{N}_\infty$ extended natural numbers. If $m > 0$ and $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ (i.e., the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is nontrivial), then $\mu$ is also a generalized eigenvalue of $f$ with exponent $m$.

Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one theorem

{f : End R M} {μ : R} {k : ℕ∞} (hk : 0 < k) : f.HasUnifEigenvalue μ k ↔ f.HasUnifEigenvalue μ 1

Full source

/-- Generalized eigenvalues are actually just eigenvalues. -/
@[simp]
lemma hasUnifEigenvalue_iff_hasUnifEigenvalue_one {f : End R M} {μ : R} {k : ℕ∞} (hk : 0 < k) :
    f.HasUnifEigenvalue μ k ↔ f.HasUnifEigenvalue μ 1 :=
  ⟨HasUnifEigenvalue.lt zero_lt_one, HasUnifEigenvalue.lt hk⟩

Generalized Eigenvalues Coincide with Eigenvalues for Positive Exponents

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k \in \mathbb{N}_\infty$ an extended natural number with $k > 0$. Then $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ if and only if $\mu$ is an eigenvalue of $f$ (i.e., a generalized eigenvalue with exponent $1$).

Module.End.maxUnifEigenspaceIndex_le_finrank theorem

[FiniteDimensional K V] (f : End K V) (μ : K) : maxUnifEigenspaceIndex f μ ≤ finrank K V

Full source

lemma maxUnifEigenspaceIndex_le_finrank [FiniteDimensional K V] (f : End K V) (μ : K) :
    maxUnifEigenspaceIndex f μ ≤ finrank K V := by
  apply Nat.sInf_le
  intro n hn
  apply le_antisymm
  · exact (f.genEigenspace μ).monotone <| WithTop.coeOrderHom.monotone hn
  · show (f.genEigenspace μ) n ≤ (f.genEigenspace μ) (finrank K V)
    rw [genEigenspace_nat, genEigenspace_nat]
    apply ker_pow_le_ker_pow_finrank

Bound on Minimal Exponent for Maximal Generalized Eigenspace by Dimension

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f \colon V \to V$ be a linear endomorphism. For any scalar $\mu \in K$, the minimal natural number $k$ such that the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is maximal satisfies $k \leq \dim_K V$.

Module.End.genEigenspace_le_genEigenspace_finrank theorem

[FiniteDimensional K V] (f : End K V) (μ : K) (k : ℕ∞) : f.genEigenspace μ k ≤ f.genEigenspace μ (finrank K V)

Full source

/-- Every generalized eigenvector is a generalized eigenvector for exponent `finrank K V`.
(Lemma 8.11 of [axler2015]) -/
lemma genEigenspace_le_genEigenspace_finrank [FiniteDimensional K V] (f : End K V)
    (μ : K) (k : ℕ∞) : f.genEigenspace μ k ≤ f.genEigenspace μ (finrank K V) := by
  calc f.genEigenspace μ k
      ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
    _ ≤ f.genEigenspace μ (finrank K V) := by
      rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
      exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Generalized Eigenspace Containment by Dimension: $\text{genEigenspace}(f, \mu, k) \subseteq \text{genEigenspace}(f, \mu, \dim_K V)$

Informal description

Let $V$ be a finite-dimensional vector space over a division ring $K$, and let $f \colon V \to V$ be a linear endomorphism. For any scalar $\mu \in K$ and extended natural number $k \in \mathbb{N}_\infty$, the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ is contained in the generalized eigenspace $\text{genEigenspace}(f, \mu, \dim_K V)$. In other words, $\text{genEigenspace}(f, \mu, k) \subseteq \text{genEigenspace}(f, \mu, \dim_K V)$.

Module.End.genEigenspace_eq_genEigenspace_finrank_of_le theorem

 [FiniteDimensional K V] (f : End K V) (μ : K) {k : ℕ} (hk : finrank K V ≤ k) :
  f.genEigenspace μ k = f.genEigenspace μ (finrank K V)

Full source

/-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other. -/
theorem genEigenspace_eq_genEigenspace_finrank_of_le [FiniteDimensional K V]
    (f : End K V) (μ : K) {k : ℕ} (hk : finrank K V ≤ k) :
    f.genEigenspace μ k = f.genEigenspace μ (finrank K V) :=
  le_antisymm
    (genEigenspace_le_genEigenspace_finrank _ _ _)
    ((f.genEigenspace μ).monotone <| by simpa using hk)

Stabilization of Generalized Eigenspaces: $\text{genEigenspace}(f, \mu, k) = \text{genEigenspace}(f, \mu, \dim_K V)$ for $k \geq \dim_K V$

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f \colon V \to V$ be a linear endomorphism. For any scalar $\mu \in K$ and natural number $k \geq \dim_K V$, the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ is equal to the generalized eigenspace $\text{genEigenspace}(f, \mu, \dim_K V)$. In other words, once the exponent $k$ reaches the dimension of $V$, the generalized eigenspace stabilizes.

Module.End.mapsTo_genEigenspace_of_comm theorem

{f g : End R M} (h : Commute f g) (μ : R) (k : ℕ∞) : MapsTo g (f.genEigenspace μ k) (f.genEigenspace μ k)

Full source

lemma mapsTo_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) (k : ℕ∞) :
    MapsTo g (f.genEigenspace μ k) (f.genEigenspace μ k) := by
  intro x hx
  simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
  rcases hx with ⟨l, hl, hx⟩
  replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
    (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l
  use l, hl
  rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp,
    LinearMap.comp_apply, hx, map_zero]

Commuting Endomorphisms Preserve Generalized Eigenspaces

Informal description

Let $f$ and $g$ be commuting linear endomorphisms of an $R$-module $M$ (i.e., $f \circ g = g \circ f$). Then for any scalar $\mu \in R$ and extended natural number $k \in \mathbb{N}_\infty$, the endomorphism $g$ maps the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ into itself. In other words, if $x \in \text{genEigenspace}(f, \mu, k)$, then $g(x) \in \text{genEigenspace}(f, \mu, k)$.

Module.End.eigenspace abbrev

(f : End R M) (μ : R) : Submodule R M

Full source

/-- 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]). -/
abbrev eigenspace (f : End R M) (μ : R) : Submodule R M :=
  f.genEigenspace μ 1

Eigenspace of a Linear Endomorphism

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the eigenspace $\text{eigenspace}\, f\, \mu$ is the submodule of $M$ consisting of all vectors $x$ such that $f x = \mu \cdot x$. Equivalently, the eigenspace is the kernel of the linear map $f - \mu \cdot \text{id}$, where $\text{id}$ denotes the identity map on $M$.

Module.End.eigenspace_def theorem

{f : End R M} {μ : R} : f.eigenspace μ = LinearMap.ker (f - μ • 1)

Full source

lemma eigenspace_def {f : End R M} {μ : R} :
    f.eigenspace μ = LinearMap.ker (f - μ • 1) := by
  rw [eigenspace, genEigenspace_one]

Eigenspace as Kernel of $f - \mu \cdot \text{id}$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the eigenspace of $f$ corresponding to $\mu$ is equal to the kernel of the linear map $f - \mu \cdot \text{id}$. That is, \[ \text{eigenspace}(f, \mu) = \ker(f - \mu \cdot \text{id}). \]

Module.End.eigenspace_zero theorem

(f : End R M) : f.eigenspace 0 = LinearMap.ker f

Full source

@[simp]
theorem eigenspace_zero (f : End R M) : f.eigenspace 0 = LinearMap.ker f := by
  simp only [eigenspace, ← Nat.cast_one (R := ℕ∞), genEigenspace_zero_nat, pow_one]

Eigenspace at Zero Equals Kernel of Endomorphism

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, the eigenspace of $f$ corresponding to the eigenvalue $0$ is equal to the kernel of $f$. That is, \[ \text{eigenspace}\, f\, 0 = \ker f. \]

Module.End.HasEigenvector abbrev

(f : End R M) (μ : R) (x : M) : Prop

Full source

/-- A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015]) -/
abbrev HasEigenvector (f : End R M) (μ : R) (x : M) : Prop :=
  HasUnifEigenvector f μ 1 x

Definition of Eigenvector for a Linear Endomorphism

Informal description

Given an $R$-module $M$, a linear endomorphism $f$ of $M$, a scalar $\mu \in R$, and a vector $x \in M$, we say $x$ is an *eigenvector* of $f$ with eigenvalue $\mu$ if $x$ is nonzero and belongs to the eigenspace of $f$ corresponding to $\mu$, i.e., $x \neq 0$ and $f(x) = \mu \cdot x$.

Module.End.hasEigenvector_iff theorem

{f : End R M} {μ : R} {x : M} : f.HasEigenvector μ x ↔ x ∈ f.eigenspace μ ∧ x ≠ 0

Full source

lemma hasEigenvector_iff {f : End R M} {μ : R} {x : M} :
    f.HasEigenvector μ x ↔ x ∈ f.eigenspace μ ∧ x ≠ 0 := Iff.rfl

Characterization of Eigenvectors via Eigenspace Membership

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a vector $x \in M$, the following are equivalent: 1. $x$ is an eigenvector of $f$ with eigenvalue $\mu$ (i.e., $f(x) = \mu \cdot x$ and $x \neq 0$). 2. $x$ belongs to the eigenspace of $f$ corresponding to $\mu$ and $x$ is nonzero. In symbols: \[ \text{$x$ is an eigenvector of $f$ with eigenvalue $\mu$} \iff x \in \text{eigenspace}\, f\, \mu \text{ and } x \neq 0. \]

Module.End.HasEigenvalue abbrev

(f : End R M) (a : R) : Prop

Full source

/-- 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]). -/
abbrev HasEigenvalue (f : End R M) (a : R) : Prop :=
  HasUnifEigenvalue f a 1

Definition of Eigenvalue for Linear Endomorphisms

Informal description

A scalar $\mu$ is called an eigenvalue of a linear endomorphism $f$ of an $R$-module $M$ if there exists a nonzero vector $x \in M$ such that $f(x) = \mu \cdot x$. Equivalently, $\mu$ is an eigenvalue if the eigenspace of $f$ corresponding to $\mu$ is nontrivial (i.e., not equal to the zero subspace).

Module.End.hasEigenvalue_iff theorem

{f : End R M} {μ : R} : f.HasEigenvalue μ ↔ f.eigenspace μ ≠ ⊥

Full source

lemma hasEigenvalue_iff {f : End R M} {μ : R} :
    f.HasEigenvalue μ ↔ f.eigenspace μ ≠ ⊥ := Iff.rfl

Characterization of Eigenvalues via Nontrivial Eigenspace

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, $\mu$ is an eigenvalue of $f$ if and only if the eigenspace $\text{eigenspace}\, f\, \mu$ is nontrivial (i.e., not equal to the zero subspace $\{0\}$).

Module.End.Eigenvalues abbrev

(f : End R M) : Type _

Full source

/-- The eigenvalues of the endomorphism `f`, as a subtype of `R`. -/
abbrev Eigenvalues (f : End R M) : Type _ :=
  UnifEigenvalues f 1

Type of Eigenvalues of a Linear Endomorphism

Informal description

The type of eigenvalues of a linear endomorphism $f$ of an $R$-module $M$, defined as the subtype of $R$ consisting of all scalars $\mu$ for which there exists a nonzero vector $x \in M$ such that $f(x) = \mu \cdot x$.

Module.End.Eigenvalues.val abbrev

(f : Module.End R M) : Eigenvalues f → R

Full source

@[coe]
abbrev Eigenvalues.val (f : Module.End R M) : Eigenvalues f → R := UnifEigenvalues.val f 1

Extraction of Scalar Value from Eigenvalue Bundle

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, the function $\text{val}$ maps an eigenvalue $\mu$ in the type $\text{Eigenvalues}\, f$ to its underlying scalar value in $R$. In other words, it extracts the scalar $\mu$ from the bundled eigenvalue type.

Module.End.hasEigenvalue_of_hasEigenvector theorem

{f : End R M} {μ : R} {x : M} (h : HasEigenvector f μ x) : HasEigenvalue f μ

Full source

theorem hasEigenvalue_of_hasEigenvector {f : End R M} {μ : R} {x : M} (h : HasEigenvector f μ x) :
    HasEigenvalue f μ :=
  h.hasUnifEigenvalue

Existence of Eigenvalue from Eigenvector

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. For a scalar $\mu \in R$ and a vector $x \in M$, if $x$ is an eigenvector of $f$ with eigenvalue $\mu$ (i.e., $x \neq 0$ and $f(x) = \mu \cdot x$), then $\mu$ is an eigenvalue of $f$.

Module.End.mem_eigenspace_iff theorem

{f : End R M} {μ : R} {x : M} : x ∈ eigenspace f μ ↔ f x = μ • x

Full source

theorem mem_eigenspace_iff {f : End R M} {μ : R} {x : M} : x ∈ eigenspace f μx ∈ eigenspace f μ ↔ f x = μ • x :=
  mem_genEigenspace_one

Characterization of Eigenspace Membership: $x \in \text{eigenspace}(f, \mu) \leftrightarrow f(x) = \mu x$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a vector $x \in M$, the vector $x$ belongs to the eigenspace of $f$ at $\mu$ if and only if $f(x) = \mu \cdot x$.

Module.End.HasEigenvector.apply_eq_smul theorem

{f : End R M} {μ : R} {x : M} (hx : f.HasEigenvector μ x) : f x = μ • x

Full source

nonrec
theorem HasEigenvector.apply_eq_smul {f : End R M} {μ : R} {x : M} (hx : f.HasEigenvector μ x) :
    f x = μ • x :=
  hx.apply_eq_smul

Eigenvector Action: $f(x) = \mu x$

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. For a scalar $\mu \in R$ and a nonzero vector $x \in M$, if $x$ is an eigenvector of $f$ with eigenvalue $\mu$, then $f(x) = \mu \cdot x$.

Module.End.HasEigenvector.pow_apply theorem

{f : End R M} {μ : R} {v : M} (hv : f.HasEigenvector μ v) (n : ℕ) : (f ^ n) v = μ ^ n • v

Full source

nonrec
theorem HasEigenvector.pow_apply {f : End R M} {μ : R} {v : M} (hv : f.HasEigenvector μ v) (n : ℕ) :
    (f ^ n) v = μ ^ n • v :=
  hv.pow_apply n

Iterated Action on Eigenvector: $f^n(v) = \mu^n v$

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. For a scalar $\mu \in R$ and a nonzero vector $v \in M$, if $v$ is an eigenvector of $f$ with eigenvalue $\mu$, then for any natural number $n$, the $n$-th iterate of $f$ applied to $v$ satisfies \[ f^n(v) = \mu^n \cdot v. \]

Module.End.HasEigenvalue.exists_hasEigenvector theorem

{f : End R M} {μ : R} (hμ : f.HasEigenvalue μ) : ∃ v, f.HasEigenvector μ v

Full source

theorem HasEigenvalue.exists_hasEigenvector {f : End R M} {μ : R} (hμ : f.HasEigenvalue μ) :
    ∃ v, f.HasEigenvector μ v :=
  Submodule.exists_mem_ne_zero_of_ne_bot hμ

Existence of Eigenvector for Eigenvalue

Informal description

For any linear endomorphism $f$ of an $R$-module $M$ and any scalar $\mu \in R$, if $\mu$ is an eigenvalue of $f$, then there exists a nonzero vector $v \in M$ such that $f(v) = \mu \cdot v$.

Module.End.HasEigenvalue.pow theorem

{f : End R M} {μ : R} (h : f.HasEigenvalue μ) (n : ℕ) : (f ^ n).HasEigenvalue (μ ^ n)

Full source

nonrec
lemma HasEigenvalue.pow {f : End R M} {μ : R} (h : f.HasEigenvalue μ) (n : ℕ) :
    (f ^ n).HasEigenvalue (μ ^ n) :=
  h.pow n

Eigenvalues of Iterated Endomorphism: $\mu^n$ is an eigenvalue of $f^n$ if $\mu$ is an eigenvalue of $f$

Informal description

Let $M$ be a module over a ring $R$, and let $f$ be an $R$-linear endomorphism of $M$. If $\mu$ is an eigenvalue of $f$, then for any natural number $n$, the scalar $\mu^n$ is an eigenvalue of the $n$-th iterate $f^n$.

Module.End.HasEigenvalue.isNilpotent_of_isNilpotent theorem

[NoZeroSMulDivisors R M] {f : End R M} (hfn : IsNilpotent f) {μ : R} (hf : f.HasEigenvalue μ) : IsNilpotent μ

Full source

/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`. -/
nonrec
lemma HasEigenvalue.isNilpotent_of_isNilpotent [NoZeroSMulDivisors R M] {f : End R M}
    (hfn : IsNilpotent f) {μ : R} (hf : f.HasEigenvalue μ) :
    IsNilpotent μ :=
  hf.isNilpotent_of_isNilpotent hfn

Nilpotency of Eigenvalues for Nilpotent Endomorphisms

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. If $f$ is a nilpotent $R$-linear endomorphism of $M$ and $\mu$ is an eigenvalue of $f$, then $\mu$ is a nilpotent element of $R$.

Module.End.HasEigenvalue.mem_spectrum theorem

{f : End R M} {μ : R} (hμ : HasEigenvalue f μ) : μ ∈ spectrum R f

Full source

nonrec
theorem HasEigenvalue.mem_spectrum {f : End R M} {μ : R} (hμ : HasEigenvalue f μ) :
    μ ∈ spectrum R f :=
  hμ.mem_spectrum

Eigenvalues Belong to Spectrum: $\mu \in \text{spectrum}(f)$ if $\mu$ is an eigenvalue of $f$

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, if $\mu$ is an eigenvalue of $f$, then $\mu$ belongs to the spectrum of $f$. In other words, if there exists a nonzero vector $v \in M$ such that $f(v) = \mu v$, then the linear map $f - \mu \cdot \text{id}$ is not invertible.

Module.End.hasEigenvalue_iff_mem_spectrum theorem

[FiniteDimensional K V] {f : End K V} {μ : K} : f.HasEigenvalue μ ↔ μ ∈ spectrum K f

Full source

theorem hasEigenvalue_iff_mem_spectrum [FiniteDimensional K V] {f : End K V} {μ : K} :
    f.HasEigenvalue μ ↔ μ ∈ spectrum K f :=
  hasUnifEigenvalue_iff_mem_spectrum

Equivalence of Eigenvalues and Spectrum in Finite Dimensions: $\mu$ is an eigenvalue of $f$ if and only if $\mu \in \text{spectrum}(f)$

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f : V \to V$ be a linear endomorphism. For any scalar $\mu \in K$, the following are equivalent: 1. $\mu$ is an eigenvalue of $f$ (i.e., there exists a nonzero vector $v \in V$ such that $f(v) = \mu v$). 2. $\mu$ belongs to the spectrum of $f$ (i.e., the linear map $f - \mu \cdot \text{id}$ is not invertible).

Module.End.eigenspace_div theorem

(f : End K V) (a b : K) (hb : b ≠ 0) : eigenspace f (a / b) = LinearMap.ker (b • f - algebraMap K (End K V) a)

Full source

theorem eigenspace_div (f : End K V) (a b : K) (hb : b ≠ 0) :
    eigenspace f (a / b) = LinearMap.ker (b • f - algebraMap K (End K V) a) :=
  genEigenspace_div f a b hb

Eigenspace as Kernel of Scaled Endomorphism Minus Scalar Identity

Informal description

Let $V$ be a vector space over a field $K$, $f$ a linear endomorphism of $V$, and $a, b \in K$ with $b \neq 0$. The eigenspace of $f$ corresponding to the eigenvalue $\frac{a}{b}$ is equal to the kernel of the linear map $b f - a \cdot \text{id}$. That is, \[ \text{eigenspace}(f, \tfrac{a}{b}) = \ker(b f - a \cdot \text{id}). \]

Module.End.genEigenspace_def theorem

(f : End R M) (μ : R) (k : ℕ) : f.genEigenspace μ k = LinearMap.ker ((f - μ • 1) ^ k)

Full source

@[deprecated genEigenspace_nat (since := "2024-10-28")]
lemma genEigenspace_def (f : End R M) (μ : R) (k : ℕ) :
    f.genEigenspace μ k = LinearMap.ker ((f - μ • 1) ^ k) :=
  genEigenspace_nat

Generalized Eigenspace as Kernel of Power Map

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a natural number $k \in \mathbb{N}$, the generalized eigenspace of $f$ at $\mu$ for $k$ is equal to the kernel of the linear map $(f - \mu \cdot \text{id})^k$. That is, \[ \text{genEigenspace}(f, \mu, k) = \ker((f - \mu \cdot \text{id})^k). \]

Module.End.HasGenEigenvector abbrev

(f : End R M) (μ : R) (k : ℕ) (x : M) : Prop

Full source

/-- A nonzero element of a generalized eigenspace is a generalized eigenvector.
(Def 8.9 of [axler2015]) -/
abbrev HasGenEigenvector (f : End R M) (μ : R) (k : ℕ) (x : M) : Prop :=
  HasUnifEigenvector f μ k x

Definition of Generalized Eigenvector

Informal description

Given an $R$-module $M$, a linear endomorphism $f$ of $M$, a scalar $\mu \in R$, and a natural number $k \in \mathbb{N}$, a vector $x \in M$ is called a *generalized eigenvector* of $f$ with eigenvalue $\mu$ and order $k$ if $x$ is a nonzero element of the generalized eigenspace $\ker((f - \mu \cdot \text{id})^k)$. In other words, $x$ satisfies $(f - \mu \cdot \text{id})^k x = 0$ and $x \neq 0$.

Module.End.hasGenEigenvector_iff theorem

{f : End R M} {μ : R} {k : ℕ} {x : M} : f.HasGenEigenvector μ k x ↔ x ∈ f.genEigenspace μ k ∧ x ≠ 0

Full source

lemma hasGenEigenvector_iff {f : End R M} {μ : R} {k : ℕ} {x : M} :
    f.HasGenEigenvector μ k x ↔ x ∈ f.genEigenspace μ k ∧ x ≠ 0 := Iff.rfl

Characterization of Generalized Eigenvectors via Eigenspace Membership

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, a natural number $k \in \mathbb{N}$, and a vector $x \in M$, the following are equivalent: 1. $x$ is a generalized eigenvector of $f$ with eigenvalue $\mu$ and order $k$ (i.e., $(f - \mu \cdot \text{id})^k x = 0$ and $x \neq 0$). 2. $x$ belongs to the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ and $x$ is nonzero. In other words, $f$ has a generalized eigenvector $x$ with eigenvalue $\mu$ and order $k$ if and only if $x$ is a nonzero element of the generalized eigenspace $\ker((f - \mu \cdot \text{id})^k)$.

Module.End.HasGenEigenvalue abbrev

(f : End R M) (μ : R) (k : ℕ) : Prop

Full source

/-- A scalar `μ` is a generalized eigenvalue for a linear map `f` and an exponent `k ∈ ℕ` if there
are generalized eigenvectors for `f`, `k`, and `μ`. -/
abbrev HasGenEigenvalue (f : End R M) (μ : R) (k : ℕ) : Prop :=
  HasUnifEigenvalue f μ k

Generalized Eigenvalue Condition for Linear Endomorphisms

Informal description

A scalar $\mu$ is a generalized eigenvalue for a linear endomorphism $f$ of an $R$-module $M$ with exponent $k \in \mathbb{N}$ if the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is nontrivial (i.e., contains a nonzero vector). Equivalently, $\mu$ is a generalized eigenvalue if there exists a nonzero vector $x \in M$ such that $(f - \mu \cdot \text{id})^k x = 0$.

Module.End.hasGenEigenvalue_iff theorem

{f : End R M} {μ : R} {k : ℕ} : f.HasGenEigenvalue μ k ↔ f.genEigenspace μ k ≠ ⊥

Full source

lemma hasGenEigenvalue_iff {f : End R M} {μ : R} {k : ℕ} :
    f.HasGenEigenvalue μ k ↔ f.genEigenspace μ k ≠ ⊥ := Iff.rfl

Generalized Eigenvalue Criterion: Nontrivial Eigenspace Condition

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a natural number $k$, the following are equivalent: 1. $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ (i.e., there exists a nonzero vector $x \in M$ such that $(f - \mu \cdot \text{id})^k x = 0$). 2. The generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is nontrivial (i.e., not equal to the zero subspace $\bot$).

Module.End.genEigenrange_def theorem

{f : End R M} {μ : R} {k : ℕ} : f.genEigenrange μ k = LinearMap.range ((f - μ • 1) ^ k)

Full source

@[deprecated genEigenrange_nat (since := "2024-10-28")]
lemma genEigenrange_def {f : End R M} {μ : R} {k : ℕ} :
    f.genEigenrange μ k = LinearMap.range ((f - μ • 1) ^ k) :=
  genEigenrange_nat

Generalized Eigenrange as Range of $(f - \mu \cdot \text{id})^k$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a natural number $k$, the generalized eigenrange of $f$ at $\mu$ with exponent $k$ is equal to the range of the linear map $(f - \mu \cdot \text{id})^k$.

Module.End.exp_ne_zero_of_hasGenEigenvalue theorem

{f : End R M} {μ : R} {k : ℕ} (h : f.HasGenEigenvalue μ k) : k ≠ 0

Full source

/-- The exponent of a generalized eigenvalue is never 0. -/
theorem exp_ne_zero_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ}
    (h : f.HasGenEigenvalue μ k) : k ≠ 0 :=
  HasUnifEigenvalue.exp_ne_zero h

Nonzero Exponent Property for Generalized Eigenvalues

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, scalar $\mu \in R$, and natural number $k$, if $\mu$ is a generalized eigenvalue of $f$ with exponent $k$, then $k \neq 0$.

Module.End.maxGenEigenspace abbrev

(f : End R M) (μ : R) : Submodule R M

Full source

/-- The union of the kernels of `(f - μ • id) ^ k` over all `k`. -/
abbrev maxGenEigenspace (f : End R M) (μ : R) : Submodule R M :=
  genEigenspace f μ ⊤

Maximal Generalized Eigenspace of a Linear Endomorphism

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the *maximal generalized eigenspace* of $f$ at $\mu$ is the union of all generalized eigenspaces $\ker((f - \mu \cdot \text{id})^k)$ over all natural numbers $k \in \mathbb{N}$. More precisely, it is the supremum (or union) of the nested sequence of subspaces $\ker(f - \mu \cdot \text{id}) \subseteq \ker((f - \mu \cdot \text{id})^2) \subseteq \cdots$, which stabilizes for sufficiently large $k$ when $M$ is finite-dimensional.

Module.End.iSup_genEigenspace_eq theorem

(f : End R M) (μ : R) : ⨆ k : ℕ, (f.genEigenspace μ) k = f.maxGenEigenspace μ

Full source

lemma iSup_genEigenspace_eq (f : End R M) (μ : R) :
    ⨆ k : ℕ, (f.genEigenspace μ) k = f.maxGenEigenspace μ := by
  simp_rw [maxGenEigenspace, genEigenspace_top]

Supremum of Generalized Eigenspaces Equals Maximal Generalized Eigenspace

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the supremum of the generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$ equals the maximal generalized eigenspace $\text{maxGenEigenspace}(f, \mu)$.

Module.End.maxGenEigenspace_def theorem

(f : End R M) (μ : R) : f.maxGenEigenspace μ = ⨆ k : ℕ, f.genEigenspace μ k

Full source

@[deprecated iSup_genEigenspace_eq (since := "2024-10-23")]
lemma maxGenEigenspace_def (f : End R M) (μ : R) :
    f.maxGenEigenspace μ = ⨆ k : ℕ, f.genEigenspace μ k :=
  (iSup_genEigenspace_eq f μ).symm

Maximal Generalized Eigenspace as Union of Generalized Eigenspaces

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the maximal generalized eigenspace of $f$ at $\mu$ is equal to the supremum (union) of the generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$.

Module.End.genEigenspace_le_maximal theorem

(f : End R M) (μ : R) (k : ℕ) : f.genEigenspace μ k ≤ f.maxGenEigenspace μ

Full source

theorem genEigenspace_le_maximal (f : End R M) (μ : R) (k : ℕ) :
    f.genEigenspace μ k ≤ f.maxGenEigenspace μ :=
  (f.genEigenspace μ).monotone le_top

Generalized Eigenspace is Contained in Maximal Generalized Eigenspace

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and any natural number $k \in \mathbb{N}$, the generalized eigenspace $\text{genEigenspace}\, f\, \mu\, k$ is contained in the maximal generalized eigenspace $\text{maxGenEigenspace}\, f\, \mu$.

Module.End.mem_maxGenEigenspace theorem

(f : End R M) (μ : R) (m : M) : m ∈ f.maxGenEigenspace μ ↔ ∃ k : ℕ, ((f - μ • (1 : End R M)) ^ k) m = 0

Full source

@[simp]
theorem mem_maxGenEigenspace (f : End R M) (μ : R) (m : M) :
    m ∈ f.maxGenEigenspace μm ∈ f.maxGenEigenspace μ ↔ ∃ k : ℕ, ((f - μ • (1 : End R M)) ^ k) m = 0 :=
  mem_genEigenspace_top

Characterization of Vectors in the Maximal Generalized Eigenspace

Informal description

For a linear endomorphism $f$ of an $R$-module $M$, a scalar $\mu \in R$, and a vector $m \in M$, the following are equivalent: 1. $m$ belongs to the maximal generalized eigenspace of $f$ at $\mu$. 2. There exists a natural number $k$ such that $(f - \mu \cdot \text{id})^k m = 0$.

Module.End.maxGenEigenspaceIndex abbrev

(f : End R M) (μ : R)

Full source

/-- 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. -/
noncomputable abbrev maxGenEigenspaceIndex (f : End R M) (μ : R) :=
  maxUnifEigenspaceIndex f μ

Minimal exponent for maximal generalized eigenspace of $f$ at $\mu$

Informal description

For a linear endomorphism $f$ of an $R$-module $M$ and a scalar $\mu \in R$, the value $\text{maxGenEigenspaceIndex}\, f\, \mu$ is the minimal natural number $k$ such that the generalized eigenspace $\ker((f - \mu \cdot \text{id})^k)$ is maximal (i.e., equals $\ker((f - \mu \cdot \text{id})^\infty)$). If no such $k$ exists, the value is not meaningful.

Module.End.maxGenEigenspace_eq theorem

[IsNoetherian R M] (f : End R M) (μ : R) : maxGenEigenspace f μ = f.genEigenspace μ (maxGenEigenspaceIndex f μ)

Full source

/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
`(f - μ • id) ^ k` for some `k`. -/
theorem maxGenEigenspace_eq [IsNoetherian R M] (f : End R M) (μ : R) :
    maxGenEigenspace f μ = f.genEigenspace μ (maxGenEigenspaceIndex f μ) :=
  genEigenspace_top_eq_maxUnifEigenspaceIndex _ _

Maximal Generalized Eigenspace Characterization in Noetherian Modules

Informal description

Let $R$ be a ring and $M$ a Noetherian $R$-module. For any endomorphism $f$ of $M$ and scalar $\mu \in R$, the maximal generalized eigenspace of $f$ at $\mu$ equals the generalized eigenspace $\ker((f - \mu \cdot \text{id})^k)$, where $k$ is the minimal natural number such that this kernel is maximal (i.e., equals $\ker((f - \mu \cdot \text{id})^\infty)$).

Module.End.hasGenEigenvalue_of_hasGenEigenvalue_of_le theorem

{f : End R M} {μ : R} {k : ℕ} {m : ℕ} (hm : k ≤ m) (hk : f.HasGenEigenvalue μ k) : f.HasGenEigenvalue μ m

Full source

/-- A generalized eigenvalue for some exponent `k` is also
    a generalized eigenvalue for exponents larger than `k`. -/
theorem hasGenEigenvalue_of_hasGenEigenvalue_of_le {f : End R M} {μ : R} {k : ℕ}
    {m : ℕ} (hm : k ≤ m) (hk : f.HasGenEigenvalue μ k) :
    f.HasGenEigenvalue μ m :=
  hk.le <| by simpa using hm

Generalized Eigenvalue Persistence: $\text{HasGenEigenvalue}\, f\, \mu\, k \to k \leq m \to \text{HasGenEigenvalue}\, f\, \mu\, m$

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k, m \in \mathbb{N}$ natural numbers. If $k \leq m$ and $\mu$ is a generalized eigenvalue of $f$ with exponent $k$, then $\mu$ is also a generalized eigenvalue of $f$ with exponent $m$.

Module.End.eigenspace_le_genEigenspace theorem

{f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) : f.eigenspace μ ≤ f.genEigenspace μ k

Full source

/-- The eigenspace is a subspace of the generalized eigenspace. -/
theorem eigenspace_le_genEigenspace {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) :
    f.eigenspace μ ≤ f.genEigenspace μ k :=
  (f.genEigenspace _).monotone <| by simpa using Nat.succ_le_of_lt hk

Inclusion of Eigenspace in Generalized Eigenspace

Informal description

For any linear endomorphism $f$ of an $R$-module $M$, any scalar $\mu \in R$, and any natural number $k > 0$, the eigenspace of $f$ corresponding to $\mu$ is contained in the generalized eigenspace of $f$ corresponding to $\mu$ and $k$. In other words, $\text{eigenspace}\, f\, \mu \leq \text{genEigenspace}\, f\, \mu\, k$.

Module.End.hasGenEigenvalue_of_hasEigenvalue theorem

{f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) (hμ : f.HasEigenvalue μ) : f.HasGenEigenvalue μ k

Full source

/-- All eigenvalues are generalized eigenvalues. -/
theorem hasGenEigenvalue_of_hasEigenvalue {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k)
    (hμ : f.HasEigenvalue μ) : f.HasGenEigenvalue μ k :=
  hμ.lt <| by simpa using hk

Eigenvalues are Generalized Eigenvalues for Positive Exponents

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k \in \mathbb{N}$ a natural number such that $k > 0$. If $\mu$ is an eigenvalue of $f$, then $\mu$ is also a generalized eigenvalue of $f$ with exponent $k$.

Module.End.hasEigenvalue_of_hasGenEigenvalue theorem

{f : End R M} {μ : R} {k : ℕ} (hμ : f.HasGenEigenvalue μ k) : f.HasEigenvalue μ

Full source

/-- All generalized eigenvalues are eigenvalues. -/
theorem hasEigenvalue_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ}
    (hμ : f.HasGenEigenvalue μ k) : f.HasEigenvalue μ :=
  hμ.lt zero_lt_one

Generalized Eigenvalues are Eigenvalues

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k \in \mathbb{N}$ a natural number. If $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ (i.e., there exists a nonzero vector $x \in M$ such that $(f - \mu \cdot \text{id})^k x = 0$), then $\mu$ is an eigenvalue of $f$ (i.e., there exists a nonzero vector $y \in M$ such that $f(y) = \mu \cdot y$).

Module.End.hasGenEigenvalue_iff_hasEigenvalue theorem

{f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) : f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ

Full source

/-- Generalized eigenvalues are actually just eigenvalues. -/
@[simp]
theorem hasGenEigenvalue_iff_hasEigenvalue {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) :
    f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ :=
  hasUnifEigenvalue_iff_hasUnifEigenvalue_one <| by simpa using hk

Generalized Eigenvalues Coincide with Eigenvalues for Positive Exponents

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $\mu \in R$ a scalar, and $k \in \mathbb{N}$ a natural number such that $k > 0$. Then $\mu$ is a generalized eigenvalue of $f$ with exponent $k$ if and only if $\mu$ is an eigenvalue of $f$.

Module.End.maxGenEigenspace_eq_genEigenspace_finrank theorem

[FiniteDimensional K V] (f : End K V) (μ : K) : f.maxGenEigenspace μ = f.genEigenspace μ (finrank K V)

Full source

theorem maxGenEigenspace_eq_genEigenspace_finrank
    [FiniteDimensional K V] (f : End K V) (μ : K) :
    f.maxGenEigenspace μ = f.genEigenspace μ (finrank K V) := by
  apply le_antisymm _ <| (f.genEigenspace μ).monotone le_top
  rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
  apply genEigenspace_le_genEigenspace_finrank f μ

Maximal Generalized Eigenspace Equals Generalized Eigenspace at Dimension Exponent

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f \colon V \to V$ be a linear endomorphism. For any scalar $\mu \in K$, the maximal generalized eigenspace of $f$ at $\mu$ is equal to the generalized eigenspace of $f$ at $\mu$ with exponent equal to the dimension of $V$ over $K$. That is, \[ \text{maxGenEigenspace}(f, \mu) = \text{genEigenspace}(f, \mu, \dim_K V). \]

Module.End.mapsTo_maxGenEigenspace_of_comm theorem

{f g : End R M} (h : Commute f g) (μ : R) : MapsTo g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)

Full source

lemma mapsTo_maxGenEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) :
    MapsTo g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
  mapsTo_genEigenspace_of_comm h μ ⊤

Commuting Endomorphisms Preserve Maximal Generalized Eigenspaces

Informal description

Let $f$ and $g$ be commuting linear endomorphisms of an $R$-module $M$ (i.e., $f \circ g = g \circ f$). Then for any scalar $\mu \in R$, the endomorphism $g$ maps the maximal generalized eigenspace $\text{maxGenEigenspace}(f, \mu)$ into itself. In other words, if $x \in \text{maxGenEigenspace}(f, \mu)$, then $g(x) \in \text{maxGenEigenspace}(f, \mu)$.

Module.End.mapsTo_iSup_genEigenspace_of_comm theorem

 {f g : End R M} (h : Commute f g) (μ : R) : MapsTo g ↑(⨆ k : ℕ, f.genEigenspace μ k) ↑(⨆ k : ℕ, f.genEigenspace μ k)

Full source

@[deprecated mapsTo_iSup_genEigenspace_of_comm (since := "2024-10-23")]
lemma mapsTo_iSup_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) :
    MapsTo g ↑(⨆ k : ℕ, f.genEigenspace μ k) ↑(⨆ k : ℕ, f.genEigenspace μ k) := by
  rw [iSup_genEigenspace_eq]
  apply mapsTo_maxGenEigenspace_of_comm h

Commuting Endomorphisms Preserve the Union of Generalized Eigenspaces

Informal description

Let $f$ and $g$ be commuting linear endomorphisms of an $R$-module $M$ (i.e., $f \circ g = g \circ f$). Then for any scalar $\mu \in R$, the endomorphism $g$ maps the supremum of the generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$ into itself. In other words, if $x \in \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$, then $g(x) \in \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$.

Module.End.disjoint_genEigenspace theorem

 [NoZeroSMulDivisors R M] (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) (k l : ℕ∞) :
  Disjoint (f.genEigenspace μ₁ k) (f.genEigenspace μ₂ l)

Full source

lemma disjoint_genEigenspace [NoZeroSMulDivisors R M]
    (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) (k l : ℕ∞) :
    Disjoint (f.genEigenspace μ₁ k) (f.genEigenspace μ₂ l) := by
  rw [genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_eq_iSup_genEigenspace_nat]
  simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]
  rintro ⟨k, -⟩ ⟨l, -⟩
  nontriviality M
  have := NoZeroSMulDivisors.isReduced R M
  rw [disjoint_iff]
  set p := f.genEigenspace μ₁ k ⊓ f.genEigenspace μ₂ l
  by_contra hp
  replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp
  let f₁ : End R p := (f - algebraMap R (End R M) μ₁).restrict <| MapsTo.inter_inter
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₁) μ₁ k)
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₁) μ₂ l)
  let f₂ : End R p := (f - algebraMap R (End R M) μ₂).restrict <| MapsTo.inter_inter
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₂) μ₁ k)
    (mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ₂) μ₂ l)
  have : IsNilpotent (f₂ - f₁) := by
    apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
    · ext; simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]
    apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
    apply isNilpotent_restrict_genEigenspace_nat
    apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
    apply isNilpotent_restrict_genEigenspace_nat
  have hf₁₂ : f₂ - f₁ = algebraMap R (End R p) (μ₁ - μ₂) := by ext; simp [f₁, f₂, sub_smul]
  rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)),
    isNilpotent_iff_eq_zero, sub_eq_zero] at this
  contradiction

Disjointness of Generalized Eigenspaces for Distinct Eigenvalues

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$ and distinct scalars $\mu_1 \neq \mu_2$ in $R$, the generalized eigenspaces $\text{genEigenspace}(f, \mu_1, k)$ and $\text{genEigenspace}(f, \mu_2, l)$ are disjoint for any extended natural numbers $k, l \in \mathbb{N}_\infty$. In other words, the intersection of these generalized eigenspaces is the trivial submodule $\{0\}$: \[ \text{genEigenspace}(f, \mu_1, k) \cap \text{genEigenspace}(f, \mu_2, l) = \{0\}. \]

Module.End.injOn_genEigenspace theorem

[NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) : InjOn (f.genEigenspace · k) {μ | f.genEigenspace μ k ≠ ⊥}

Full source

lemma injOn_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    InjOn (f.genEigenspace · k) {μ | f.genEigenspace μ k ≠ ⊥} := by
  rintro μ₁ _ μ₂ hμ₂ hμ₁₂
  by_contra contra
  apply hμ₂
  simpa only [hμ₁₂, disjoint_self] using f.disjoint_genEigenspace contra k k

Injectivity of Generalized Eigenspace Construction for Nontrivial Eigenspaces

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$ and extended natural number $k \in \mathbb{N}_\infty$, the function $\mu \mapsto \text{genEigenspace}(f, \mu, k)$ is injective on the set of scalars $\mu$ for which the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ is nontrivial. In other words, if $\mu_1, \mu_2$ are scalars such that $\text{genEigenspace}(f, \mu_1, k) \neq \{0\}$ and $\text{genEigenspace}(f, \mu_2, k) \neq \{0\}$, then $\text{genEigenspace}(f, \mu_1, k) = \text{genEigenspace}(f, \mu_2, k)$ implies $\mu_1 = \mu_2$.

Module.End.disjoint_iSup_genEigenspace theorem

 [NoZeroSMulDivisors R M] (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) :
  Disjoint (⨆ k : ℕ, f.genEigenspace μ₁ k) (⨆ k : ℕ, f.genEigenspace μ₂ k)

Full source

@[deprecated disjoint_genEigenspace (since := "2024-10-23")]
lemma disjoint_iSup_genEigenspace [NoZeroSMulDivisors R M]
    (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) :
    Disjoint (⨆ k : ℕ, f.genEigenspace μ₁ k) (⨆ k : ℕ, f.genEigenspace μ₂ k) := by
  simpa only [iSup_genEigenspace_eq] using disjoint_genEigenspace f hμ ⊤ ⊤

Disjointness of Suprema of Generalized Eigenspaces for Distinct Eigenvalues

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$ and distinct scalars $\mu_1 \neq \mu_2$ in $R$, the suprema of the generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_1, k)$ and $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_2, k)$ are disjoint. In other words, their intersection is the trivial submodule $\{0\}$: \[ \left( \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_1, k) \right) \cap \left( \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_2, k) \right) = \{0\}. \]

Module.End.injOn_maxGenEigenspace theorem

[NoZeroSMulDivisors R M] (f : End R M) : InjOn (f.maxGenEigenspace ·) {μ | f.maxGenEigenspace μ ≠ ⊥}

Full source

lemma injOn_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    InjOn (f.maxGenEigenspace ·) {μ | f.maxGenEigenspace μ ≠ ⊥} :=
  injOn_genEigenspace f ⊤

Injectivity of Maximal Generalized Eigenspace Construction for Nontrivial Eigenspaces

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$, the function $\mu \mapsto \text{maxGenEigenspace}(f, \mu)$ is injective on the set of scalars $\mu$ for which the maximal generalized eigenspace $\text{maxGenEigenspace}(f, \mu)$ is nontrivial. In other words, if $\mu_1, \mu_2$ are scalars such that $\text{maxGenEigenspace}(f, \mu_1) \neq \{0\}$ and $\text{maxGenEigenspace}(f, \mu_2) \neq \{0\}$, then $\text{maxGenEigenspace}(f, \mu_1) = \text{maxGenEigenspace}(f, \mu_2)$ implies $\mu_1 = \mu_2$.

Module.End.injOn_iSup_genEigenspace theorem

 [NoZeroSMulDivisors R M] (f : End R M) : InjOn (⨆ k : ℕ, f.genEigenspace · k) {μ | ⨆ k : ℕ, f.genEigenspace μ k ≠ ⊥}

Full source

@[deprecated injOn_genEigenspace (since := "2024-10-23")]
lemma injOn_iSup_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    InjOn (⨆ k : ℕ, f.genEigenspace · k) {μ | ⨆ k : ℕ, f.genEigenspace μ k ≠ ⊥} := by
  simp_rw [iSup_genEigenspace_eq]
  apply injOn_maxGenEigenspace

Injectivity of Supremum of Generalized Eigenspaces for Nontrivial Cases

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$, the function $\mu \mapsto \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$ is injective on the set of scalars $\mu$ for which $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k) \neq \{0\}$. In other words, if $\mu_1, \mu_2$ are scalars such that $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_1, k) \neq \{0\}$ and $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_2, k) \neq \{0\}$, then $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_1, k) = \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu_2, k)$ implies $\mu_1 = \mu_2$.

Module.End.independent_genEigenspace theorem

[NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) : iSupIndep (f.genEigenspace · k)

Full source

theorem independent_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    iSupIndep (f.genEigenspace · k) := by
  classical
  suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.genEigenspace μ₁ k)
    (s.sup fun μ ↦ f.genEigenspace μ k) by
    simp_rw [iSupIndep_iff_supIndep_of_injOn (injOn_genEigenspace f k),
      Finset.supIndep_iff_disjoint_erase]
    exact fun s μ _ ↦ this _ _ (s.not_mem_erase μ)
  intro μ₁ s
  induction s using Finset.induction_on with
  | empty => simp
  | insert μ₂ s _ ih =>
  intro hμ₁₂
  obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
  specialize ih hμ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  let g := f - μ₂ • 1
  simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
  peel hy with l hlk hl
  simp only [mem_genEigenspace_nat, LinearMap.mem_ker] at hl
  have hyz : (g ^ l) (y + z) ∈
      (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k := by
    refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
    · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
    · rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
  rwa [ih.eq_bot, Submodule.mem_bot] at hyz

Supremum Independence of Generalized Eigenspaces for a Linear Endomorphism

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$ and extended natural number $k \in \mathbb{N}_\infty$, the family of generalized eigenspaces $\{\text{genEigenspace}(f, \mu, k) \mid \mu \in R\}$ is supremum independent. This means that for any scalar $\mu$, the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ is disjoint from the supremum of all other generalized eigenspaces: \[ \text{genEigenspace}(f, \mu, k) \cap \left(\bigsqcup_{\mu' \neq \mu} \text{genEigenspace}(f, \mu', k)\right) = \{0\}. \]

Module.End.independent_maxGenEigenspace theorem

[NoZeroSMulDivisors R M] (f : End R M) : iSupIndep f.maxGenEigenspace

Full source

theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    iSupIndep f.maxGenEigenspace := by
  apply independent_genEigenspace

Supremum Independence of Maximal Generalized Eigenspaces for a Linear Endomorphism

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$, the family of maximal generalized eigenspaces $\{\text{maxGenEigenspace}(f, \mu) \mid \mu \in R\}$ is supremum independent. This means that for any scalar $\mu$, the maximal generalized eigenspace $\text{maxGenEigenspace}(f, \mu)$ is disjoint from the supremum of all other maximal generalized eigenspaces: \[ \text{maxGenEigenspace}(f, \mu) \cap \left(\bigsqcup_{\mu' \neq \mu} \text{maxGenEigenspace}(f, \mu')\right) = \{0\}. \]

Module.End.independent_iSup_genEigenspace theorem

[NoZeroSMulDivisors R M] (f : End R M) : iSupIndep (fun μ ↦ ⨆ k : ℕ, f.genEigenspace μ k)

Full source

@[deprecated independent_genEigenspace (since := "2024-10-23")]
theorem independent_iSup_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    iSupIndep (fun μ ↦ ⨆ k : ℕ, f.genEigenspace μ k) := by
  simp_rw [iSup_genEigenspace_eq]
  apply independent_maxGenEigenspace

Supremum Independence of Unions of Generalized Eigenspaces for a Linear Endomorphism

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$, the family of subspaces $\{\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k) \mid \mu \in R\}$ is supremum independent. This means that for any scalar $\mu$, the subspace $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$ is disjoint from the supremum of all other such subspaces: \[ \left(\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)\right) \cap \left(\bigsqcup_{\mu' \neq \mu} \bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu', k)\right) = \{0\}. \]

Module.End.eigenspaces_iSupIndep theorem

[NoZeroSMulDivisors R M] (f : End R M) : iSupIndep f.eigenspace

Full source

/-- 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 eigenspaces_iSupIndep [NoZeroSMulDivisors R M] (f : End R M) :
    iSupIndep f.eigenspace :=
  (f.independent_genEigenspace 1).mono fun _ ↦ le_rfl

Supremum Independence of Eigenspaces for a Linear Endomorphism

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. For any linear endomorphism $f$ of $M$, the family of eigenspaces $\{\text{eigenspace}(f, \mu) \mid \mu \in R\}$ is supremum independent. This means that for any scalar $\mu$, the eigenspace $\text{eigenspace}(f, \mu)$ is disjoint from the supremum of all other eigenspaces: \[ \text{eigenspace}(f, \mu) \cap \left(\bigsqcup_{\mu' \neq \mu} \text{eigenspace}(f, \mu')\right) = \{0\}. \]

Module.End.eigenvectors_linearIndependent' theorem

 {ι : Type*} [NoZeroSMulDivisors R M] (f : End R M) (μ : ι → R) (hμ : Function.Injective μ) (v : ι → M)
  (h_eigenvec : ∀ i, f.HasEigenvector (μ i) (v i)) : LinearIndependent R v

Full source

/-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
    independent. -/
theorem eigenvectors_linearIndependent' {ι : Type*} [NoZeroSMulDivisors R M]
    (f : End R M) (μ : ι → R) (hμ : Function.Injective μ) (v : ι → M)
    (h_eigenvec : ∀ i, f.HasEigenvector (μ i) (v i)) : LinearIndependent R v :=
  f.eigenspaces_iSupIndep.comp hμ |>.linearIndependent _
    (fun i ↦ h_eigenvec i |>.left) (fun i ↦ h_eigenvec i |>.right)

Linear Independence of Eigenvectors Corresponding to Distinct Eigenvalues

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. Given a linear endomorphism $f$ of $M$, an index set $\iota$, an injective function $\mu : \iota \to R$ assigning distinct eigenvalues, and a family of vectors $v : \iota \to M$ such that for each $i \in \iota$, $v_i$ is an eigenvector of $f$ with eigenvalue $\mu_i$ (i.e., $v_i \neq 0$ and $f(v_i) = \mu_i \cdot v_i$), then the family of vectors $\{v_i\}_{i \in \iota}$ is linearly independent over $R$.

Module.End.eigenvectors_linearIndependent theorem

 [NoZeroSMulDivisors R M] (f : End R M) (μs : Set R) (xs : μs → M) (h_eigenvec : ∀ μ : μs, f.HasEigenvector μ (xs μ)) :
  LinearIndependent R xs

Full source

/-- 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 eigenvectors_linearIndependent [NoZeroSMulDivisors R M]
    (f : End R M) (μs : Set R) (xs : μs → M)
    (h_eigenvec : ∀ μ : μs, f.HasEigenvector μ (xs μ)) : LinearIndependent R xs :=
  f.eigenvectors_linearIndependent' (fun μ : μs ↦ μ) Subtype.coe_injective _ h_eigenvec

Linear Independence of Eigenvectors Corresponding to Distinct Eigenvalues

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. Given a linear endomorphism $f$ of $M$, a set of eigenvalues $\mu_s \subseteq R$, and a family of vectors $(x_\mu)_{\mu \in \mu_s}$ such that for each $\mu \in \mu_s$, $x_\mu$ is an eigenvector of $f$ with eigenvalue $\mu$ (i.e., $x_\mu \neq 0$ and $f(x_\mu) = \mu \cdot x_\mu$), then the family of vectors $(x_\mu)_{\mu \in \mu_s}$ is linearly independent over $R$.

Module.End.genEigenspace_restrict theorem

 (f : End R M) (p : Submodule R M) (k : ℕ∞) (μ : R) (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
  genEigenspace (LinearMap.restrict f hfp) μ k = Submodule.comap p.subtype (f.genEigenspace μ k)

Full source

/-- 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 genEigenspace_restrict (f : End R M) (p : Submodule R M) (k : ℕ∞) (μ : R)
    (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
    genEigenspace (LinearMap.restrict f hfp) μ k =
      Submodule.comap p.subtype (f.genEigenspace μ k) := by
  ext x
  suffices ∀ l : ℕ, genEigenspace (LinearMap.restrict f hfp) μ l =
      Submodule.comap p.subtype (f.genEigenspace μ l) by
    simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
      Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]
  intro l
  simp only [genEigenspace_nat, OrderHom.coe_mk, ← LinearMap.ker_comp]
  induction l with
  | zero =>
    rw [pow_zero, pow_zero, Module.End.one_eq_id]
    apply (Submodule.ker_subtype _).symm
  | succ l ih =>
    erw [pow_succ, pow_succ, LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp,
      LinearMap.comp_assoc]

Generalized Eigenspace of Restricted Endomorphism Equals Intersection with Submodule

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $p$ a submodule of $M$, and $\mu \in R$ a scalar. If $f$ maps $p$ into itself (i.e., for all $x \in p$, $f(x) \in p$), then for any extended natural number $k \in \mathbb{N}_\infty$, the generalized eigenspace of the restriction of $f$ to $p$ at $\mu$ and $k$ is equal to the preimage of the generalized eigenspace of $f$ at $\mu$ and $k$ under the inclusion map of $p$ into $M$. In other words: \[ \text{genEigenspace}\, (f|_p)\, \mu\, k = p \cap \text{genEigenspace}\, f\, \mu\, k \] where $f|_p$ denotes the restriction of $f$ to $p$.

Submodule.inf_genEigenspace theorem

 (f : End R M) (p : Submodule R M) {k : ℕ∞} {μ : R} (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
  p ⊓ f.genEigenspace μ k = (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype

Full source

lemma _root_.Submodule.inf_genEigenspace (f : End R M) (p : Submodule R M) {k : ℕ∞} {μ : R}
    (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
    p ⊓ f.genEigenspace μ k =
      (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := by
  rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype]

Intersection of Submodule with Generalized Eigenspace Equals Restricted Generalized Eigenspace

Informal description

Let $f$ be a linear endomorphism of an $R$-module $M$, $p$ a submodule of $M$ invariant under $f$ (i.e., $f(p) \subseteq p$), $\mu \in R$ a scalar, and $k \in \mathbb{N}_\infty$ an extended natural number. Then the intersection of $p$ with the generalized eigenspace of $f$ at $\mu$ and $k$ is equal to the image under the inclusion map $p \hookrightarrow M$ of the generalized eigenspace of the restriction $f|_p$ at $\mu$ and $k$. In other words: \[ p \cap \text{genEigenspace}(f, \mu, k) = \text{genEigenspace}(f|_p, \mu, k) \] where the right side is considered as a submodule of $M$ via the inclusion map.

Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo theorem

 {p : Submodule R M} (f g : End R M) (hf : MapsTo f p p) (hg : MapsTo g p p) {μ₁ μ₂ : R}
  (h : MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) :
  MapsTo (f.restrict hf) (maxGenEigenspace (g.restrict hg) μ₁) (maxGenEigenspace (g.restrict hg) μ₂)

Full source

lemma mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo
    {p : Submodule R M} (f g : End R M) (hf : MapsTo f p p) (hg : MapsTo g p p) {μ₁ μ₂ : R}
    (h : MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) :
    MapsTo (f.restrict hf)
      (maxGenEigenspace (g.restrict hg) μ₁)
      (maxGenEigenspace (g.restrict hg) μ₂) := by
  intro x hx
  simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
    LinearMap.restrict_sub _, Module.End.pow_restrict _, LinearMap.restrict_apply,
    Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢
  exact h hx

Restriction of Maps Between Maximal Generalized Eigenspaces

Informal description

Let $M$ be an $R$-module, $p$ a submodule of $M$, and $f, g$ linear endomorphisms of $M$ such that $f$ and $g$ preserve $p$ (i.e., $f(p) \subseteq p$ and $g(p) \subseteq p$). Suppose that for some scalars $\mu_1, \mu_2 \in R$, the map $f$ sends the maximal generalized eigenspace of $g$ at $\mu_1$ into the maximal generalized eigenspace of $g$ at $\mu_2$. Then the restriction of $f$ to $p$ sends the maximal generalized eigenspace of the restriction of $g$ to $p$ at $\mu_1$ into the maximal generalized eigenspace of the restriction of $g$ to $p$ at $\mu_2$.

Module.End.eigenspace_restrict_le_eigenspace theorem

 (f : End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) (μ : R) :
  (eigenspace (f.restrict hfp) μ).map p.subtype ≤ f.eigenspace μ

Full source

/-- 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 eigenspace_restrict_le_eigenspace (f : End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p)
    (μ : R) : (eigenspace (f.restrict hfp) μ).map p.subtype ≤ f.eigenspace μ := by
  rintro a ⟨x, hx, rfl⟩
  simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢
  exact congr_arg Subtype.val hx

Inclusion of Restricted Eigenspace in Full Eigenspace

Informal description

Let $f$ be an $R$-linear endomorphism of an $R$-module $M$, and let $p$ be a submodule of $M$ that is invariant under $f$ (i.e., for all $x \in p$, we have $f x \in p$). Then for any scalar $\mu \in R$, the $\mu$-eigenspace of the restriction of $f$ to $p$ is contained in the $\mu$-eigenspace of $f$ on $M$. More precisely, the image of the $\mu$-eigenspace of $f|_{p}$ under the inclusion map $p \hookrightarrow M$ is a submodule of the $\mu$-eigenspace of $f$ on $M$.

Module.End.generalized_eigenvec_disjoint_range_ker theorem

 [FiniteDimensional K V] (f : End K V) (μ : K) :
  Disjoint (f.genEigenrange μ (finrank K V)) (f.genEigenspace μ (finrank K V))

Full source

/-- Generalized eigenrange and generalized eigenspace for exponent `finrank K V` are disjoint. -/
theorem generalized_eigenvec_disjoint_range_ker [FiniteDimensional K V] (f : End K V) (μ : K) :
    Disjoint (f.genEigenrange μ (finrank K V))
      (f.genEigenspace μ (finrank K V)) := by
  have h :=
    calc
      Submodule.comap ((f - μ • 1) ^ finrank K V)
        (f.genEigenspace μ (finrank K V)) =
          LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
            (f - algebraMap K (End K V) μ) ^ finrank K V) := by
              rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
      _ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by
              simp_rw [← pow_add, genEigenspace_nat]; rfl
      _ = f.genEigenspace μ (finrank K V) := by
              rw [genEigenspace_eq_genEigenspace_finrank_of_le]; omega
  rw [disjoint_iff_inf_le, genEigenrange_nat, LinearMap.range_eq_map,
    Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h, genEigenspace_nat]
  apply Submodule.map_comap_le

Disjointness of Generalized Eigenrange and Eigenspace at Dimension Exponent

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f \colon V \to V$ be a linear endomorphism. For any scalar $\mu \in K$, the generalized eigenrange and generalized eigenspace of $f$ at $\mu$ with exponent equal to the dimension of $V$ are disjoint, i.e., \[ \text{genEigenrange}(f, \mu, \dim_K V) \cap \text{genEigenspace}(f, \mu, \dim_K V) = \{0\}. \]

Module.End.eigenspace_restrict_eq_bot theorem

 {f : End R M} {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) {μ : R} (hμp : Disjoint (f.eigenspace μ) p) :
  eigenspace (f.restrict hfp) μ = ⊥

Full source

/-- 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 eigenspace_restrict_eq_bot {f : End R M} {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p)
    {μ : R} (hμp : Disjoint (f.eigenspace μ) p) : eigenspace (f.restrict hfp) μ = ⊥ := by
  rw [eq_bot_iff]
  intro x hx
  simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩

Triviality of Restricted Eigenspace under Disjointness Condition

Informal description

Let $f$ be an $R$-linear endomorphism of an $R$-module $M$, and let $p$ be a submodule of $M$ that is invariant under $f$ (i.e., for all $x \in p$, we have $f x \in p$). If the $\mu$-eigenspace of $f$ is disjoint from $p$, then the $\mu$-eigenspace of the restriction of $f$ to $p$ is trivial, i.e., $\text{eigenspace}\, (f|_{p})\, \mu = \{\mathbf{0}\}$.

Module.End.pos_finrank_genEigenspace_of_hasEigenvalue theorem

 [FiniteDimensional K V] {f : End K V} {k : ℕ} {μ : K} (hx : f.HasEigenvalue μ) (hk : 0 < k) :
  0 < finrank K (f.genEigenspace μ k)

Full source

/-- The generalized eigenspace of an eigenvalue has positive dimension for positive exponents. -/
theorem pos_finrank_genEigenspace_of_hasEigenvalue [FiniteDimensional K V] {f : End K V}
    {k : ℕ} {μ : K} (hx : f.HasEigenvalue μ) (hk : 0 < k) :
    0 < finrank K (f.genEigenspace μ k) :=
  calc
    0 = finrank K (⊥ : Submodule K V) := by rw [finrank_bot]
    _ < finrank K (f.eigenspace μ) := Submodule.finrank_lt_finrank_of_lt (bot_lt_iff_ne_bot.2 hx)
    _ ≤ finrank K (f.genEigenspace μ k) :=
      Submodule.finrank_mono ((f.genEigenspace μ).monotone (by simpa using Nat.succ_le_of_lt hk))

Positive Dimension of Generalized Eigenspace for Eigenvalues with Positive Exponent

Informal description

Let $V$ be a finite-dimensional vector space over a field $K$, and let $f$ be a linear endomorphism of $V$. If $\mu$ is an eigenvalue of $f$ and $k$ is a positive natural number, then the generalized eigenspace $\text{genEigenspace}(f, \mu, k)$ has positive dimension, i.e., $\dim_K \text{genEigenspace}(f, \mu, k) > 0$.

Module.End.map_genEigenrange_le theorem

{f : End K V} {μ : K} {n : ℕ} : Submodule.map f (f.genEigenrange μ n) ≤ f.genEigenrange μ n

Full source

/-- A linear map maps a generalized eigenrange into itself. -/
theorem map_genEigenrange_le {f : End K V} {μ : K} {n : ℕ} :
    Submodule.map f (f.genEigenrange μ n) ≤ f.genEigenrange μ n :=
  calc
    Submodule.map f (f.genEigenrange μ n) =
      LinearMap.range (f * (f - algebraMap _ _ μ) ^ n) := by
        rw [genEigenrange_nat]; exact (LinearMap.range_comp _ _).symm
    _ = LinearMap.range ((f - algebraMap _ _ μ) ^ n * f) := by
        rw [Algebra.mul_sub_algebraMap_pow_commutes]
    _ = Submodule.map ((f - algebraMap _ _ μ) ^ n) (LinearMap.range f) := LinearMap.range_comp _ _
    _ ≤ f.genEigenrange μ n := by rw [genEigenrange_nat]; apply LinearMap.map_le_range

Linear Endomorphism Preserves Generalized Eigenrange

Informal description

For a linear endomorphism $f$ of a finite-dimensional vector space $V$ over a field $K$, a scalar $\mu \in K$, and a natural number $n$, the image of the generalized eigenrange of $f$ at $\mu$ with exponent $n$ under $f$ is contained within the generalized eigenrange itself. In other words, $f$ maps the range of $(f - \mu \cdot \text{id})^n$ into itself.

Module.End.genEigenspace_le_smul theorem

(f : Module.End R M) (μ t : R) (k : ℕ∞) : (f.genEigenspace μ k) ≤ (t • f).genEigenspace (t * μ) k

Full source

lemma genEigenspace_le_smul (f : Module.End R M) (μ t : R) (k : ℕ∞) :
    (f.genEigenspace μ k) ≤ (t • f).genEigenspace (t * μ) k := by
  intro m hm
  simp_rw [mem_genEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢
  peel hm with l hlk hl
  rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero]

Generalized Eigenspace Inclusion Under Scalar Multiplication: $\text{genEigenspace}(f, \mu, k) \subseteq \text{genEigenspace}(t \cdot f, t \cdot \mu, k)$

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module. For any linear endomorphism $f$ of $M$, scalar $\mu \in R$, extended natural number $k \in \mathbb{N}_\infty$, and scalar $t \in R$, the generalized eigenspace of $f$ for eigenvalue $\mu$ and order $k$ is contained in the generalized eigenspace of $t \cdot f$ for eigenvalue $t \cdot \mu$ and order $k$. In other words, $$ \text{genEigenspace}(f, \mu, k) \subseteq \text{genEigenspace}(t \cdot f, t \cdot \mu, k). $$

Module.End.iSup_genEigenspace_le_smul theorem

 (f : Module.End R M) (μ t : R) : (⨆ k : ℕ, f.genEigenspace μ k) ≤ ⨆ k : ℕ, (t • f).genEigenspace (t * μ) k

Full source

@[deprecated genEigenspace_le_smul (since := "2024-10-23")]
lemma iSup_genEigenspace_le_smul (f : Module.End R M) (μ t : R) :
    (⨆ k : ℕ, f.genEigenspace μ k) ≤ ⨆ k : ℕ, (t • f).genEigenspace (t * μ) k := by
  rw [iSup_genEigenspace_eq, iSup_genEigenspace_eq]
  apply genEigenspace_le_smul

Supremum of Generalized Eigenspaces is Contained Under Scalar Multiplication: $\bigsqcup_k \text{genEigenspace}(f, \mu, k) \subseteq \bigsqcup_k \text{genEigenspace}(t \cdot f, t \cdot \mu, k)$

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module. For any linear endomorphism $f$ of $M$, scalar $\mu \in R$, and scalar $t \in R$, the supremum of the generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f, \mu, k)$ is contained in the supremum of the generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(t \cdot f, t \cdot \mu, k)$. In other words, $$ \bigsqcup_{k \in \mathbb{N}} \ker((f - \mu \cdot \text{id})^k) \subseteq \bigsqcup_{k \in \mathbb{N}} \ker((t \cdot f - t \cdot \mu \cdot \text{id})^k). $$

Module.End.genEigenspace_inf_le_add theorem

 (f₁ f₂ : End R M) (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞) (h : Commute f₁ f₂) :
  (f₁.genEigenspace μ₁ k₁) ⊓ (f₂.genEigenspace μ₂ k₂) ≤ (f₁ + f₂).genEigenspace (μ₁ + μ₂) (k₁ + k₂)

Full source

lemma genEigenspace_inf_le_add
    (f₁ f₂ : End R M) (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞) (h : Commute f₁ f₂) :
    (f₁.genEigenspace μ₁ k₁) ⊓ (f₂.genEigenspace μ₂ k₂) ≤
    (f₁ + f₂).genEigenspace (μ₁ + μ₂) (k₁ + k₂) := by
  intro m hm
  simp only [Submodule.mem_inf, mem_genEigenspace, LinearMap.mem_ker] at hm ⊢
  obtain ⟨⟨l₁, hlk₁, hl₁⟩, ⟨l₂, hlk₂, hl₂⟩⟩ := hm
  use l₁ + l₂
  have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by
    rw [add_smul]; exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)
  replace h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1) :=
    (h.sub_right <| Algebra.commute_algebraMap_right μ₂ f₁).sub_left
      (Algebra.commute_algebraMap_left μ₁ _)
  rw [this, h.add_pow', LinearMap.coeFn_sum, Finset.sum_apply]
  constructor
  · simpa only [Nat.cast_add] using add_le_add hlk₁ hlk₂
  refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_
  suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
    rw [LinearMap.smul_apply, this, smul_zero]
  rw [Finset.mem_antidiagonal] at hij
  obtain hi|hj : l₁ ≤ i ∨ l₂ ≤ j := by omega
  · rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁,
      LinearMap.map_zero]
  · rw [Module.End.mul_apply, Module.End.pow_map_zero_of_le hj hl₂, LinearMap.map_zero]

Intersection of Generalized Eigenspaces for Commuting Endomorphisms is Contained in Sum's Generalized Eigenspace

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module. For any two commuting endomorphisms $f_1, f_2 \in \text{End}_R(M)$, scalars $\mu_1, \mu_2 \in R$, and extended natural numbers $k_1, k_2 \in \mathbb{N}_\infty$, the intersection of the generalized eigenspaces $\text{genEigenspace}(f_1, \mu_1, k_1)$ and $\text{genEigenspace}(f_2, \mu_2, k_2)$ is contained in the generalized eigenspace $\text{genEigenspace}(f_1 + f_2, \mu_1 + \mu_2, k_1 + k_2)$. In other words, if $x \in M$ is a generalized eigenvector for $f_1$ with eigenvalue $\mu_1$ and order $\leq k_1$, and also a generalized eigenvector for $f_2$ with eigenvalue $\mu_2$ and order $\leq k_2$, then $x$ is a generalized eigenvector for $f_1 + f_2$ with eigenvalue $\mu_1 + \mu_2$ and order $\leq k_1 + k_2$.

Module.End.iSup_genEigenspace_inf_le_add theorem

 (f₁ f₂ : End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) :
  (⨆ k : ℕ, f₁.genEigenspace μ₁ k) ⊓ (⨆ k : ℕ, f₂.genEigenspace μ₂ k) ≤ ⨆ k : ℕ, (f₁ + f₂).genEigenspace (μ₁ + μ₂) k

Full source

@[deprecated genEigenspace_inf_le_add (since := "2024-10-23")]
lemma iSup_genEigenspace_inf_le_add
    (f₁ f₂ : End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) :
    (⨆ k : ℕ, f₁.genEigenspace μ₁ k) ⊓ (⨆ k : ℕ, f₂.genEigenspace μ₂ k) ≤
    ⨆ k : ℕ, (f₁ + f₂).genEigenspace (μ₁ + μ₂) k := by
  simp_rw [iSup_genEigenspace_eq]
  apply genEigenspace_inf_le_add
  assumption

Intersection of Maximal Generalized Eigenspaces for Commuting Endomorphisms is Contained in Sum's Maximal Generalized Eigenspace

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module. For any two commuting endomorphisms $f_1, f_2 \in \text{End}_R(M)$ and scalars $\mu_1, \mu_2 \in R$, the intersection of the maximal generalized eigenspaces $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f_1, \mu_1, k)$ and $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f_2, \mu_2, k)$ is contained in the maximal generalized eigenspace $\bigsqcup_{k \in \mathbb{N}} \text{genEigenspace}(f_1 + f_2, \mu_1 + \mu_2, k)$. In other words, if $x \in M$ is a generalized eigenvector for $f_1$ with eigenvalue $\mu_1$ (of some order) and also a generalized eigenvector for $f_2$ with eigenvalue $\mu_2$ (of some order), then $x$ is a generalized eigenvector for $f_1 + f_2$ with eigenvalue $\mu_1 + \mu_2$ (of some order).

Module.End.map_smul_of_iInf_genEigenspace_ne_bot theorem

 [NoZeroSMulDivisors R M] {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F)
  (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥) (t : R) (x : L) : μ (t • x) = t • μ x

Full source

lemma map_smul_of_iInf_genEigenspace_ne_bot [NoZeroSMulDivisors R M]
    {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F)
    (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥)
    (t : R) (x : L) :
    μ (t • x) = t • μ x := by
  by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)
  simp only [g, map_smul]
  exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

Scalar Multiplication Property of Eigenvalue Function for Nontrivial Generalized Eigenspace Intersection

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. Let $L$ be a type with a scalar multiplication action by $R$, and $F$ a type of $R$-equivariant functions from $L$ to $\text{End}_R(M)$. Given a function $f \in F$ and a scalar-valued function $\mu : L \to R$, suppose the infimum of generalized eigenspaces $\bigsqcap_{x \in L} \text{genEigenspace}(f(x), \mu(x), k)$ is nontrivial for some extended natural number $k \in \mathbb{N}_\infty$. Then for any scalar $t \in R$ and element $x \in L$, the function $\mu$ satisfies the scalar multiplication property: \[ \mu(t \cdot x) = t \cdot \mu(x). \]

Module.End.map_smul_of_iInf_iSup_genEigenspace_ne_bot theorem

 [NoZeroSMulDivisors R M] {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F)
  (μ : L → R) (h_ne : ⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k ≠ ⊥) (t : R) (x : L) : μ (t • x) = t • μ x

Full source

@[deprecated map_smul_of_iInf_genEigenspace_ne_bot (since := "2024-10-23")]
lemma map_smul_of_iInf_iSup_genEigenspace_ne_bot [NoZeroSMulDivisors R M]
    {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F)
    (μ : L → R) (h_ne : ⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k ≠ ⊥)
    (t : R) (x : L) :
    μ (t • x) = t • μ x := by
  simp_rw [iSup_genEigenspace_eq] at h_ne
  apply map_smul_of_iInf_genEigenspace_ne_bot f μ ⊤ h_ne t x

Scalar multiplication property of eigenvalue function for nontrivial intersection of maximal generalized eigenspaces

Informal description

Let $R$ be a ring and $M$ an $R$-module with no zero scalar divisors. Let $L$ be a type with a scalar multiplication action by $R$, and $F$ a type of $R$-equivariant functions from $L$ to $\text{End}_R(M)$. Given a function $f \in F$ and a scalar-valued function $\mu : L \to R$, suppose the intersection of the maximal generalized eigenspaces $\bigcap_{x \in L} \bigcup_{k \in \mathbb{N}} \text{genEigenspace}(f(x), \mu(x), k)$ is nontrivial. Then for any scalar $t \in R$ and element $x \in L$, the function $\mu$ satisfies the scalar multiplication property: \[ \mu(t \cdot x) = t \cdot \mu(x). \]

Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute theorem

 [NoZeroSMulDivisors R M] {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F) (μ : L → R)
  (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥) (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
  μ (x + y) = μ x + μ y

Full source

lemma map_add_of_iInf_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M]
    {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F)
    (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).genEigenspace (μ x) k⨅ x, (f x).genEigenspace (μ x) k ≠ ⊥)
    (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
    μ (x + y) = μ x + μ y := by
  by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))
  simp only [g, map_add]
  exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

Additivity of Eigenvalue Function for Commuting Endomorphisms with Nontrivial Intersection of Generalized Eigenspaces

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module with no zero scalar divisors. Let $L$ be an additive group and $F$ a type of additive homomorphisms from $L$ to the endomorphism ring $\text{End}_R(M)$. Given a function $\mu : L \to R$ and an extended natural number $k \in \mathbb{N}_\infty$, suppose that the intersection of the generalized eigenspaces $\bigcap_{x \in L} \text{genEigenspace}(f(x), \mu(x), k)$ is nontrivial (i.e., not equal to $\{0\}$). If the endomorphisms $f(x)$ and $f(y)$ commute for all $x, y \in L$, then $\mu$ is additive, i.e., $\mu(x + y) = \mu(x) + \mu(y)$ for all $x, y \in L$.

Module.End.map_add_of_iInf_iSup_genEigenspace_ne_bot_of_commute theorem

 [NoZeroSMulDivisors R M] {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F) (μ : L → R)
  (h_ne : ⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k ≠ ⊥) (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
  μ (x + y) = μ x + μ y

Full source

@[deprecated map_add_of_iInf_genEigenspace_ne_bot_of_commute (since := "2024-10-23")]
lemma map_add_of_iInf_iSup_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M]
    {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F)
    (μ : L → R) (h_ne : ⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k⨅ x, ⨆ k : ℕ, (f x).genEigenspace (μ x) k ≠ ⊥)
    (h : ∀ x y, Commute (f x) (f y)) (x y : L) :
    μ (x + y) = μ x + μ y := by
  simp_rw [iSup_genEigenspace_eq] at h_ne
  apply map_add_of_iInf_genEigenspace_ne_bot_of_commute f μ ⊤ h_ne h x y

Additivity of Eigenvalue Function for Commuting Endomorphisms with Nontrivial Generalized Eigenspaces

Informal description

Let $R$ be a commutative ring and $M$ an $R$-module with no zero scalar divisors. Let $L$ be an additive group and $F$ a type of additive homomorphisms from $L$ to the endomorphism ring $\text{End}_R(M)$. Given a function $\mu : L \to R$, suppose that for each $x \in L$, the union $\bigcup_{k \in \mathbb{N}} \text{genEigenspace}(f(x), \mu(x), k)$ of generalized eigenspaces is nontrivial, and that the intersection $\bigcap_{x \in L} \bigcup_{k \in \mathbb{N}} \text{genEigenspace}(f(x), \mu(x), k)$ is also nontrivial. If the endomorphisms $f(x)$ and $f(y)$ commute for all $x, y \in L$, then $\mu$ is additive, i.e., $\mu(x + y) = \mu(x) + \mu(y)$ for all $x, y \in L$.

Mathlib.LinearAlgebra.Eigenspace.Basic

References

Tags