feat(linear_algebra/eigenspace): mem_maximal_generalized_eigenspace (…

…#7162)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/linear_algebra/basic.lean

@@ -14,6 +14,7 @@ import data.finsupp.basic
 import data.dfinsupp
 import algebra.pointwise
 import order.compactly_generated
+import order.omega_complete_partial_order
 
 /-!
 # Linear algebra
@@ -834,6 +835,19 @@ begin
   simp only [Sup_eq_supr', mem_supr_of_directed _ hdir.directed_coe, set_coe.exists, subtype.coe_mk]
 end
 
+@[norm_cast, simp] lemma coe_supr_of_chain (a : ℕ →ₘ submodule R M) :
+  (↑(⨆ k, a k) : set M) = ⋃ k, (a k : set M) :=
+coe_supr_of_directed a a.monotone.directed_le
+
+/-- We can regard `coe_supr_of_chain` as the statement that `coe : (submodule R M) → set M` is
+Scott continuous for the ω-complete partial order induced by the complete lattice structures. -/
+lemma coe_scott_continuous : omega_complete_partial_order.continuous' 
+  (coe : submodule R M → set M) :=
+⟨set_like.coe_mono, coe_supr_of_chain⟩
+
+@[simp] lemma mem_supr_of_chain (a : ℕ →ₘ submodule R M) (m : M) : m ∈ (⨆ k, a k) ↔ ∃ k, m ∈ a k :=
+mem_supr_of_directed a a.monotone.directed_le
+
 section
 
 variables {p p'}

src/linear_algebra/eigenspace.lean

@@ -307,6 +307,10 @@ def generalized_eigenspace (f : End R M) (μ : R) : ℕ →ₘ submodule R M :=
       ((f - algebra_map R (End R M) μ) ^ k) ((f - algebra_map R (End R M) μ) ^ (m - k)),
   end }
 
+@[simp] lemma mem_generalized_eigenspace (f : End R M) (μ : R) (k : ℕ) (m : M) :
+  m ∈ f.generalized_eigenspace μ k ↔ ((f - μ • 1)^k) m = 0 :=
+iff.rfl
+
 /-- A nonzero element of a generalized eigenspace is a generalized eigenvector.
     (Def 8.9 of [axler2015])-/
 def has_generalized_eigenvector (f : End R M) (μ : R) (k : ℕ) (x : M) : Prop :=
@@ -334,6 +338,15 @@ end
 def maximal_generalized_eigenspace (f : End R M) (μ : R) : submodule R M :=
 ⨆ k, f.generalized_eigenspace μ k
 
+lemma generalized_eigenspace_le_maximal (f : End R M) (μ : R) (k : ℕ) :
+  f.generalized_eigenspace μ k ≤ f.maximal_generalized_eigenspace μ :=
+le_supr _ _
+
+@[simp] lemma mem_maximal_generalized_eigenspace (f : End R M) (μ : R) (m : M) :
+  m ∈ f.maximal_generalized_eigenspace μ ↔ ∃ (k : ℕ), ((f - μ • 1)^k) m = 0 :=
+by simp only [maximal_generalized_eigenspace, ← mem_generalized_eigenspace,
+  submodule.mem_supr_of_chain]
+
 /-- 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. -/

src/order/directed.lean

@@ -52,6 +52,10 @@ lemma directed_of_sup [semilattice_sup α] {f : α → β} {r : β → β → Pr
   (H : ∀ ⦃i j⦄, i ≤ j → r (f i) (f j)) : directed r f :=
 λ a b, ⟨a ⊔ b, H le_sup_left, H le_sup_right⟩
 
+lemma monotone.directed_le [semilattice_sup α] [preorder β] {f : α → β} :
+  monotone f → directed (≤) f :=
+directed_of_sup
+
 /-- An antimonotone function on an inf-semilattice is directed. -/
 lemma directed_of_inf [semilattice_inf α] {r : β → β → Prop} {f : α → β}
   (hf : ∀a₁ a₂, a₁ ≤ a₂ → r (f a₂) (f a₁)) : directed r f :=