feat(linear_algebra/eigenspace): define the maximal generalized eigenspace (#7125)

And prove that it is of the form kernel of `(f - μ • id) ^ k` for some finite `k` for endomorphisms of Noetherian modules.

Author: ocfnash

src/linear_algebra/eigenspace.lean

@@ -7,6 +7,7 @@ Authors: Alexander Bentkamp
 import field_theory.algebraic_closure
 import linear_algebra.finsupp
 import linear_algebra.matrix
+import order.preorder_hom
 
 /-!
 # Eigenvectors and eigenvalues
@@ -295,9 +296,16 @@ begin
 end
 
 /-- The generalized eigenspace for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the
-    kernel of `(f - μ • id) ^ k`. (Def 8.10 of [axler2015])-/
-def generalized_eigenspace (f : End R M) (μ : R) (k : ℕ) : submodule R M :=
-((f - algebra_map R (End R M) μ) ^ k).ker
+kernel of `(f - μ • id) ^ k`. (Def 8.10 of [axler2015]). Furthermore, a generalized eigenspace for
+some exponent `k` is contained in the generalized eigenspace for exponents larger than `k`. -/
+def generalized_eigenspace (f : End R M) (μ : R) : ℕ →ₘ submodule R M :=
+{ to_fun    := λ k, ((f - algebra_map R (End R M) μ) ^ k).ker,
+  monotone' := λ k m hm,
+  begin
+    simp only [← pow_sub_mul_pow _ hm],
+    exact linear_map.ker_le_ker_comp
+      ((f - algebra_map R (End R M) μ) ^ k) ((f - algebra_map R (End R M) μ) ^ (m - k)),
+  end }
 
 /-- A nonzero element of a generalized eigenspace is a generalized eigenvector.
     (Def 8.9 of [axler2015])-/
@@ -322,14 +330,24 @@ begin
   exact h linear_map.ker_id
 end
 
-/-- A generalized eigenspace for some exponent `k` is contained in
-    the generalized eigenspace for exponents larger than `k`. -/
-lemma generalized_eigenspace_mono {f : End R M} {μ : R} {k : ℕ} {m : ℕ} (hm : k ≤ m) :
-  f.generalized_eigenspace μ k ≤ f.generalized_eigenspace μ m :=
+/-- The union of the kernels of `(f - μ • id) ^ k` over all `k`. -/
+def maximal_generalized_eigenspace (f : End R M) (μ : R) : submodule R M :=
+⨆ k, f.generalized_eigenspace μ k
+
+/-- 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 maximal_generalized_eigenspace_index (f : End R M) (μ : R) :=
+monotonic_sequence_limit_index (f.generalized_eigenspace μ)
+
+/-- For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel
+`(f - μ • id) ^ k` for some `k`. -/
+lemma maximal_generalized_eigenspace_eq [h : is_noetherian R M] (f : End R M) (μ : R) :
+  maximal_generalized_eigenspace f μ =
+  f.generalized_eigenspace μ (maximal_generalized_eigenspace_index f μ) :=
 begin
-  simp only [generalized_eigenspace, ←pow_sub_mul_pow _ hm],
-  exact linear_map.ker_le_ker_comp
-    ((f - algebra_map R (End R M) μ) ^ k) ((f - algebra_map R (End R M) μ) ^ (m - k)),
+  rw is_noetherian_iff_well_founded at h,
+  exact (well_founded.supr_eq_monotonic_sequence_limit h (f.generalized_eigenspace μ) : _),
 end
 
 /-- A generalized eigenvalue for some exponent `k` is also
@@ -341,21 +359,22 @@ begin
   unfold has_generalized_eigenvalue at *,
   contrapose! hk,
   rw [←le_bot_iff, ←hk],
-  exact generalized_eigenspace_mono hm
+  exact (f.generalized_eigenspace μ).monotone hm,
 end
 
 /-- The eigenspace is a subspace of the generalized eigenspace. -/
-lemma eigenspace_le_generalized_eigenspace {f : End K V} {μ : K} {k : ℕ} (hk : 0 < k) :
+lemma eigenspace_le_generalized_eigenspace {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) :
   f.eigenspace μ ≤ f.generalized_eigenspace μ k :=
-generalized_eigenspace_mono (nat.succ_le_of_lt hk)
+(f.generalized_eigenspace μ).monotone (nat.succ_le_of_lt hk)
 
 /-- All eigenvalues are generalized eigenvalues. -/
 lemma has_generalized_eigenvalue_of_has_eigenvalue
   {f : End R M} {μ : R} {k : ℕ} (hk : 0 < k) (hμ : f.has_eigenvalue μ) :
   f.has_generalized_eigenvalue μ k :=
 begin
   apply has_generalized_eigenvalue_of_has_generalized_eigenvalue_of_le hk,
-  rwa [has_generalized_eigenvalue, generalized_eigenspace, pow_one]
+  rw [has_generalized_eigenvalue, generalized_eigenspace, preorder_hom.coe_fun_mk, pow_one],
+  exact hμ,
 end
 
 /-- All generalized eigenvalues are eigenvalues. -/
@@ -390,11 +409,11 @@ ker_pow_eq_ker_pow_findim_of_le hk
 /-- 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`. -/
 lemma generalized_eigenspace_restrict
-  (f : End K V) (p : submodule K V) (k : ℕ) (μ : K) (hfp : ∀ (x : V), x ∈ p → f x ∈ p) :
+  (f : End R M) (p : submodule R M) (k : ℕ) (μ : R) (hfp : ∀ (x : M), x ∈ p → f x ∈ p) :
   generalized_eigenspace (linear_map.restrict f hfp) μ k =
     submodule.comap p.subtype (f.generalized_eigenspace μ k) :=
 begin
-  rw [generalized_eigenspace, generalized_eigenspace, ←linear_map.ker_comp],
+  simp only [generalized_eigenspace, preorder_hom.coe_fun_mk, ← linear_map.ker_comp],
   induction k with k ih,
   { rw [pow_zero, pow_zero, linear_map.one_eq_id],
     apply (submodule.ker_subtype _).symm },
@@ -409,7 +428,7 @@ begin
   have h := calc
     submodule.comap ((f - algebra_map _ _ μ) ^ findim K V) (f.generalized_eigenspace μ (findim K V))
       = ((f - algebra_map _ _ μ) ^ findim K V * (f - algebra_map K (End K V) μ) ^ findim K V).ker :
-        by { rw [generalized_eigenspace, ←linear_map.ker_comp], refl }
+        by { simpa only [generalized_eigenspace, preorder_hom.coe_fun_mk, ← linear_map.ker_comp], }
   ... = f.generalized_eigenspace μ (findim K V + findim K V) :
         by { rw ←pow_add, refl }
   ... = f.generalized_eigenspace μ (findim K V) :
@@ -427,7 +446,7 @@ calc
     0 = findim K (⊥ : submodule K V) : by rw findim_bot
   ... < findim K (f.eigenspace μ) : submodule.findim_lt_findim_of_lt (bot_lt_iff_ne_bot.2 hx)
   ... ≤ findim K (f.generalized_eigenspace μ k) :
-    submodule.findim_mono (generalized_eigenspace_mono (nat.succ_le_of_lt hk))
+    submodule.findim_mono ((f.generalized_eigenspace μ).monotone (nat.succ_le_of_lt hk))
 
 /-- A linear map maps a generalized eigenrange into itself. -/
 lemma map_generalized_eigenrange_le {f : End K V} {μ : K} {n : ℕ} :

src/order/order_iso_nat.lean

@@ -8,6 +8,7 @@ import data.equiv.denumerable
 import data.set.finite
 import order.rel_iso
 import order.preorder_hom
+import order.conditionally_complete_lattice
 import logic.function.iterate
 
 namespace rel_embedding
@@ -157,3 +158,34 @@ begin
     obtain ⟨n, hn⟩ := h (a.swap : ((<) : ℕ → ℕ → Prop) →r ((<) : α → α → Prop)).to_preorder_hom,
     exact n.succ_ne_self.symm (rel_embedding.to_preorder_hom_injective _ (hn _ n.le_succ)), },
 end
+
+/-- Given an eventually-constant monotonic sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered
+type, `monotonic_sequence_limit_index a` is the least natural number `n` for which `aₙ` reaches the
+constant value. For sequences that are not eventually constant, `monotonic_sequence_limit_index a`
+is defined, but is a junk value. -/
+noncomputable def monotonic_sequence_limit_index {α : Type*} [partial_order α] (a : ℕ →ₘ α) : ℕ :=
+Inf { n | ∀ m, n ≤ m → a n = a m }
+
+/-- The constant value of an eventually-constant monotonic sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
+partially-ordered type. -/
+noncomputable def monotonic_sequence_limit {α : Type*} [partial_order α] (a : ℕ →ₘ α) :=
+a (monotonic_sequence_limit_index a)
+
+lemma well_founded.supr_eq_monotonic_sequence_limit {α : Type*} [complete_lattice α]
+  (h : well_founded ((>) : α → α → Prop)) (a : ℕ →ₘ α) :
+  (⨆ m, a m) = monotonic_sequence_limit a :=
+begin
+  suffices : (⨆ (m : ℕ), a m) ≤ monotonic_sequence_limit a,
+  { exact le_antisymm this (le_supr a _), },
+  apply supr_le,
+  intros m,
+  by_cases hm : m ≤ monotonic_sequence_limit_index a,
+  { exact a.monotone hm, },
+  { replace hm := le_of_not_le hm,
+    let S := { n | ∀ m, n ≤ m → a n = a m },
+    have hInf : Inf S ∈ S,
+    { refine nat.Inf_mem _, rw well_founded.monotone_chain_condition at h, exact h a, },
+    change Inf S ≤ m at hm,
+    change a m ≤ a (Inf S),
+    rw hInf m hm, },
+end