English
For a diagonal operator with respect to a basis, the maximal generalized eigenspace coincides with the ordinary eigenspace.
Русский
Для диагонального оператора относительно базиса максимальное обобщённое эйгенпространство совпадает с обычным эйгенпространством.
LaTeX
$$$\\text{maxGenEigenspace}((\\text{diagonal } d).toLin b b)\\; μ = \\text{eigenspace}((\\text{diagonal } d).toLin b b)\\; μ$$$
Lean4
/-- Eigenvalues of a diagonal linear operator are the diagonal entries. -/
theorem hasEigenvalue_toLin_diagonal_iff (d : n → R) {μ : R} [NoZeroSMulDivisors R M] (b : Basis n R M) :
HasEigenvalue (toLin b b (diagonal d)) μ ↔ ∃ i, d i = μ :=
by
have (i : n) : HasEigenvalue (toLin b b (diagonal d)) (d i) :=
hasEigenvalue_of_hasEigenvector <| hasEigenvector_toLin_diagonal d i b
constructor
· contrapose!
intro hμ h_eig
have h_iSup : ⨆ μ ∈ Set.range d, eigenspace (toLin b b (diagonal d)) μ = ⊤ :=
by
rw [eq_top_iff, ← b.span_eq, Submodule.span_le]
rintro - ⟨i, rfl⟩
simp only [SetLike.mem_coe]
apply Submodule.mem_iSup_of_mem (d i)
apply Submodule.mem_iSup_of_mem ⟨i, rfl⟩
rw [mem_eigenspace_iff]
exact (hasEigenvector_toLin_diagonal d i b).apply_eq_smul
have hμ_notMem : μ ∉ Set.range d := by simpa using fun i ↦ (hμ i)
have := eigenspaces_iSupIndep (toLin b b (diagonal d)) |>.disjoint_biSup hμ_notMem
rw [h_iSup, disjoint_top] at this
exact h_eig this
· rintro ⟨i, rfl⟩
exact this i
