chore(algebra/algebra/spectrum): move `exists_spectrum_of_is_alg_clos…

…ed_of_finite_dimensional` (#10919)

Move a lemma from `field_theory/is_alg_closed/basic` into `algebra/algebra/spectrum` which belongs in this relatively new file. Also, rename (now in `spectrum` namespace) and refactor it slightly; and update the two references to it accordingly.

- [x] depends on: #10783 



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/algebra/algebra/spectrum.lean

@@ -310,6 +310,22 @@ begin
     simp only [set.image_congr, eval_C, aeval_C, scalar_eq, set.nonempty.image_const hnon] },
 end
 
+variable (𝕜)
+/--
+Every element `a` in a nontrivial finite-dimensional algebra `A`
+over an algebraically closed field `𝕜` has non-empty spectrum. -/
+-- We will use this both to show eigenvalues exist, and to prove Schur's lemma.
+lemma nonempty_of_is_alg_closed_of_finite_dimensional [is_alg_closed 𝕜]
+  [nontrivial A] [I : finite_dimensional 𝕜 A] (a : A) :
+  ∃ k : 𝕜, k ∈ σ a :=
+begin
+  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := is_integral_of_noetherian (is_noetherian.iff_fg.2 I) a,
+  have nu : ¬ is_unit (aeval a p), { rw [←aeval_def] at h_eval_p, rw h_eval_p, simp, },
+  rw [eq_prod_roots_of_monic_of_splits_id h_mon (is_alg_closed.splits p)] at nu,
+  obtain ⟨k, hk, _⟩ := exists_mem_of_not_is_unit_aeval_prod (monic.ne_zero h_mon) nu,
+  exact ⟨k, hk⟩
+end
+
 end scalar_field
 
 end spectrum

src/category_theory/preadditive/schur.lean

@@ -7,7 +7,7 @@ import algebra.group.ext
 import category_theory.simple
 import category_theory.linear
 import category_theory.endomorphism
-import field_theory.is_alg_closed.basic
+import algebra.algebra.spectrum
 
 /-!
 # Schur's lemma
@@ -109,11 +109,11 @@ begin
   { exact id_nonzero, },
   { intro f,
     haveI : nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero,
-    obtain ⟨c, nu⟩ := @exists_spectrum_of_is_alg_closed_of_finite_dimensional 𝕜 _ _ (End X) _ _ _
+    obtain ⟨c, nu⟩ := @spectrum.nonempty_of_is_alg_closed_of_finite_dimensional 𝕜 (End X) _ _ _ _ _
       (by { convert I, ext, refl, ext, refl, }) (End.of f),
     use c,
-    rw [is_unit_iff_is_iso, is_iso_iff_nonzero, ne.def, not_not, sub_eq_zero,
-      algebra.algebra_map_eq_smul_one] at nu,
+    rw [spectrum.mem_iff, is_unit.sub_iff, is_unit_iff_is_iso, is_iso_iff_nonzero, ne.def,
+      not_not, sub_eq_zero, algebra.algebra_map_eq_smul_one] at nu,
     exact nu.symm, },
 end
 

src/field_theory/is_alg_closed/basic.lean

@@ -166,27 +166,6 @@ theorem is_alg_closure_iff (K : Type v) [field K] [algebra k K] :
   is_alg_closure k K ↔ is_alg_closed K ∧ algebra.is_algebraic k K :=
 ⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩
 
-/--
-Every element `f` in a nontrivial finite-dimensional algebra `A`
-over an algebraically closed field `K`
-has non-empty spectrum:
-that is, there is some `c : K` so `f - c • 1` is not invertible.
--/
--- We will use this both to show eigenvalues exist, and to prove Schur's lemma.
-lemma exists_spectrum_of_is_alg_closed_of_finite_dimensional (𝕜 : Type*) [field 𝕜] [is_alg_closed 𝕜]
-  {A : Type*} [nontrivial A] [ring A] [algebra 𝕜 A] [I : finite_dimensional 𝕜 A] (f : A) :
-  ∃ c : 𝕜, ¬ is_unit (f - algebra_map 𝕜 A c) :=
-begin
-  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := is_integral_of_noetherian (is_noetherian.iff_fg.2 I) f,
-  have nu : ¬ is_unit (aeval f p), { rw [←aeval_def] at h_eval_p, rw h_eval_p, simp, },
-  rw [eq_prod_roots_of_monic_of_splits_id h_mon (is_alg_closed.splits p),
-    ←multiset.prod_to_list, alg_hom.map_list_prod] at nu,
-  replace nu := mt list.prod_is_unit nu,
-  simp only [not_forall, exists_prop, aeval_C, multiset.mem_to_list,
-    list.mem_map, aeval_X, exists_exists_and_eq_and, multiset.mem_map, alg_hom.map_sub] at nu,
-  exact ⟨nu.some, nu.some_spec.2⟩,
-end
-
 namespace lift
 /- In this section, the homomorphism from any algebraic extension into an algebraically
   closed extension is proven to exist. The assumption that M is algebraically closed could probably

src/linear_algebra/eigenspace.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp
 -/
 
-import field_theory.is_alg_closed.basic
 import linear_algebra.charpoly.basic
 import linear_algebra.finsupp
 import linear_algebra.matrix.to_lin
@@ -202,9 +201,9 @@ end minpoly
 lemma exists_eigenvalue [is_alg_closed K] [finite_dimensional K V] [nontrivial V] (f : End K V) :
   ∃ (c : K), f.has_eigenvalue c :=
 begin
-  obtain ⟨c, nu⟩ := exists_spectrum_of_is_alg_closed_of_finite_dimensional K f,
+  obtain ⟨c, nu⟩ := spectrum.nonempty_of_is_alg_closed_of_finite_dimensional K f,
   use c,
-  rw linear_map.is_unit_iff_ker_eq_bot at nu,
+  rw [spectrum.mem_iff, is_unit.sub_iff, linear_map.is_unit_iff_ker_eq_bot] at nu,
   exact has_eigenvalue_of_has_eigenvector (submodule.exists_mem_ne_zero_of_ne_bot nu).some_spec,
 end