From 7faa8afcf3820474b70273380dbd8f5f1d8880e6 Mon Sep 17 00:00:00 2001
From: JonBannon <jbannon@siena.edu>
Date: Thu, 27 Jun 2024 18:55:39 +0000
Subject: [PATCH] feat: the spectrum of a diagonal matrix is the range of the
 diagonal (#13837)

We add various theorems that assert the spectrum of a diagonal matrix is the range of the diagonal viewed as a function.

Co-Authored by @j-loreaux



Co-authored-by: JonBannon <59937998+JonBannon@users.noreply.github.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
---
 Mathlib.lean                                 |  1 +
 Mathlib/LinearAlgebra/Eigenspace/Matrix.lean | 80 ++++++++++++++++++++
 2 files changed, 81 insertions(+)
 create mode 100644 Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1a2338142fc9f..d41fc4deb9895 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2757,6 +2757,7 @@ import Mathlib.LinearAlgebra.DirectSum.Finsupp
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.Eigenspace.Basic
+import Mathlib.LinearAlgebra.Eigenspace.Matrix
 import Mathlib.LinearAlgebra.Eigenspace.Minpoly
 import Mathlib.LinearAlgebra.Eigenspace.Semisimple
 import Mathlib.LinearAlgebra.Eigenspace.Triangularizable
diff --git a/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean b/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
new file mode 100644
index 0000000000000..a58ddeb616fdd
--- /dev/null
+++ b/Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2024 Jon Bannon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Bannon, Jireh Loreaux
+-/
+
+import Mathlib.LinearAlgebra.Eigenspace.Basic
+
+/-!
+
+# Eigenvalues, Eigenvectors and Spectrum for Matrices
+
+This file collects results about eigenvectors, eigenvalues and spectrum specific to matrices
+over a nontrivial commutative ring, nontrivial commutative ring without zero divisors, or field.
+
+## Tags
+eigenspace, eigenvector, eigenvalue, spectrum, matrix
+
+-/
+
+section SpectrumDiagonal
+
+variable {R n M : Type*} [DecidableEq n] [Fintype n]
+
+open Matrix
+open Module.End
+
+section NontrivialCommRing
+
+variable [CommRing R] [Nontrivial R] [AddCommGroup M] [Module R M]
+
+/-- Basis vectors are eigenvectors of associated diagonal linear operator. -/
+lemma hasEigenvector_toLin_diagonal (d : n → R) (i : n) (b : Basis n R M) :
+    HasEigenvector (toLin b b (diagonal d)) (d i) (b i) :=
+  ⟨mem_eigenspace_iff.mpr <| by simp [diagonal], Basis.ne_zero b i⟩
+
+/--  Standard basis vectors are eigenvectors of any associated diagonal linear operator. -/
+lemma hasEigenvector_toLin'_diagonal (d : n → R) (i : n) :
+    HasEigenvector (toLin' (diagonal d)) (d i) (Pi.basisFun R n i)  :=
+  hasEigenvector_toLin_diagonal ..
+
+/-- Eigenvalues of a diagonal linear operator are the diagonal entries. -/
+lemma 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μ_not_mem : μ ∉ Set.range d := by simpa using fun i ↦ (hμ i)
+    have := eigenspaces_independent (toLin b b (diagonal d)) |>.disjoint_biSup hμ_not_mem
+    rw [h_iSup, disjoint_top] at this
+    exact h_eig this
+  · rintro ⟨i, rfl⟩
+    exact this i
+
+/-- Eigenvalues of a diagonal linear operator with respect to standard basis
+    are the diagonal entries. -/
+lemma hasEigenvalue_toLin'_diagonal_iff [NoZeroDivisors R] (d : n → R) {μ : R} :
+    HasEigenvalue (toLin' (diagonal d)) μ ↔ (∃ i, d i = μ) :=
+  hasEigenvalue_toLin_diagonal_iff _ <| Pi.basisFun R n
+
+end NontrivialCommRing
+
+/-- The spectrum of the diagonal operator is the range of the diagonal viewed as a function. -/
+lemma spectrum_diagonal [Field R] (d : n → R) :
+    spectrum R (diagonal d) = Set.range d := by
+  ext μ
+  rw [← AlgEquiv.spectrum_eq (toLinAlgEquiv <| Pi.basisFun R n), ← hasEigenvalue_iff_mem_spectrum]
+  exact hasEigenvalue_toLin'_diagonal_iff d
+
+end SpectrumDiagonal