refactor(linear_algebra/eigenspace): refactor exists_eigenvalue (#7345)

We replace the proof of `exists_eigenvalue` with the more general fact:
```
/--
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.
-/
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) := ...
```

We can then use this fact to prove Schur's lemma.



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

src/algebra/algebra/basic.lean

@@ -573,13 +573,21 @@ ext $ λ x, show φ₁.to_linear_map x = φ₂.to_linear_map x, by rw H
 @[simp] lemma comp_to_linear_map (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
   (g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl
 
+lemma map_list_prod (s : list A) :
+  φ s.prod = (s.map φ).prod :=
+φ.to_ring_hom.map_list_prod s
+
 end semiring
 
 section comm_semiring
 
 variables [comm_semiring R] [comm_semiring A] [comm_semiring B]
 variables [algebra R A] [algebra R B] (φ : A →ₐ[R] B)
 
+lemma map_multiset_prod (s : multiset A) :
+  φ s.prod = (s.map φ).prod :=
+φ.to_ring_hom.map_multiset_prod s
+
 lemma map_prod {ι : Type*} (f : ι → A) (s : finset ι) :
   φ (∏ x in s, f x) = ∏ x in s, φ (f x) :=
 φ.to_ring_hom.map_prod f s

src/algebra/group/units.lean

@@ -265,6 +265,7 @@ iff.intro
     by rwa [mul_assoc, units.mul_inv, mul_one] at this)
   (assume ⟨v, hv⟩, hv ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
 
+@[to_additive]
 lemma is_unit.mul [monoid M] {x y : M} : is_unit x → is_unit y → is_unit (x * y) :=
 by { rintros ⟨x, rfl⟩ ⟨y, rfl⟩, exact ⟨x * y, units.coe_mul _ _⟩ }
 
@@ -278,6 +279,11 @@ is_unit_iff_exists_inv.2 ⟨y * z, by rwa ← mul_assoc⟩
   (hu : is_unit (x * y)) : is_unit y :=
 @is_unit_of_mul_is_unit_left _ _ y x $ by rwa mul_comm
 
+@[simp]
+lemma is_unit.mul_iff [comm_monoid M] {x y : M} : is_unit (x * y) ↔ is_unit x ∧ is_unit y :=
+⟨λ h, ⟨is_unit_of_mul_is_unit_left h, is_unit_of_mul_is_unit_right h⟩,
+  λ h, is_unit.mul h.1 h.2⟩
+
 @[to_additive] theorem is_unit.mul_right_inj [monoid M] {a b c : M} (ha : is_unit a) :
   a * b = a * c ↔ b = c :=
 by cases ha with a ha; rw [←ha, units.mul_right_inj]

src/data/list/basic.lean

@@ -2299,6 +2299,15 @@ theorem prod_hom [monoid β] (l : list α) (f : α →* β) :
 by { simp only [prod, foldl_map, f.map_one.symm],
   exact l.foldl_hom _ _ _ 1 f.map_mul }
 
+@[to_additive]
+lemma prod_is_unit [monoid β] : Π {L : list β} (u : ∀ m ∈ L, is_unit m), is_unit L.prod
+| [] _ := by simp
+| (h :: t) u :=
+begin
+  simp only [list.prod_cons],
+  exact is_unit.mul (u h (mem_cons_self h t)) (prod_is_unit (λ m mt, u m (mem_cons_of_mem h mt)))
+end
+
 -- `to_additive` chokes on the next few lemmas, so we do them by hand below
 @[simp]
 lemma prod_take_mul_prod_drop :

src/data/multiset/basic.lean

@@ -264,9 +264,11 @@ classical.some (quotient.exists_rep s)
 @[simp] lemma to_list_zero {α : Type*} : (multiset.to_list 0 : list α) = [] :=
 (multiset.coe_eq_zero _).1 (classical.some_spec (quotient.exists_rep multiset.zero))
 
+@[simp, norm_cast]
 lemma coe_to_list {α : Type*} (s : multiset α) : (s.to_list : multiset α) = s :=
 classical.some_spec (quotient.exists_rep _)
 
+@[simp]
 lemma mem_to_list {α : Type*} (a : α) (s : multiset α) : a ∈ s.to_list ↔ a ∈ s :=
 by rw [←multiset.mem_coe, multiset.coe_to_list]
 
@@ -1020,6 +1022,13 @@ multiset.induction_on s (λ _, dvd_zero _)
 @[simp] theorem sum_map_singleton (s : multiset α) : (s.map (λ a, a ::ₘ 0)).sum = s :=
 multiset.induction_on s (by simp) (by simp)
 
+@[simp, to_additive] theorem prod_to_list [comm_monoid α] (s : multiset α) :
+  s.to_list.prod = s.prod :=
+begin
+  conv_rhs { rw ←coe_to_list s, },
+  rw coe_prod,
+end
+
 /-! ### Join -/
 
 /-- `join S`, where `S` is a multiset of multisets, is the lift of the list join

src/field_theory/algebraic_closure.lean

@@ -338,3 +338,24 @@ instance : is_alg_closure k (algebraic_closure k) :=
 ⟨algebraic_closure.is_alg_closed k, is_algebraic k⟩
 
 end algebraic_closure
+
+/--
+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 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

src/field_theory/splitting_field.lean

@@ -275,6 +275,19 @@ begin
       map_bind_roots_eq]
 end
 
+lemma eq_prod_roots_of_splits_id {p : polynomial K}
+  (hsplit : splits (ring_hom.id K) p) :
+  p = C (p.leading_coeff) * (p.roots.map (λ a, X - C a)).prod :=
+by simpa using eq_prod_roots_of_splits hsplit
+
+lemma eq_prod_roots_of_monic_of_splits_id {p : polynomial K}
+  (m : monic p) (hsplit : splits (ring_hom.id K) p) :
+  p = (p.roots.map (λ a, X - C a)).prod :=
+begin
+  convert eq_prod_roots_of_splits_id hsplit,
+  simp [m], 
+end
+
 lemma eq_X_sub_C_of_splits_of_single_root {x : K} {h : polynomial K} (h_splits : splits i h)
   (h_roots : (h.map i).roots = {i x}) : h = (C (leading_coeff h)) * (X - C x) :=
 begin

src/linear_algebra/eigenspace.lean

@@ -56,13 +56,20 @@ def eigenspace (f : End R M) (μ : R) : submodule R M :=
 
 /-- A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015]) -/
 def has_eigenvector (f : End R M) (μ : R) (x : M) : Prop :=
-x ≠ 0 ∧ x ∈ eigenspace f μ
+x ∈ eigenspace f μ ∧ x ≠ 0
 
 /-- A scalar `μ` is an eigenvalue for a linear map `f` if there are nonzero vectors `x`
     such that `f x = μ • x`. (Def 5.5 of [axler2015]) -/
 def has_eigenvalue (f : End R M) (a : R) : Prop :=
 eigenspace f a ≠ ⊥
 
+lemma has_eigenvalue_of_has_eigenvector {f : End R M} {μ : R} {x : M} (h : has_eigenvector f μ x) :
+  has_eigenvalue f μ :=
+begin
+  rw [has_eigenvalue, submodule.ne_bot_iff],
+  use x, exact h,
+end
+
 lemma mem_eigenspace_iff {f : End R M} {μ : R} {x : M} : x ∈ eigenspace f μ ↔ f x = μ • x :=
 by rw [eigenspace, linear_map.mem_ker, linear_map.sub_apply, algebra_map_End_apply,
   sub_eq_zero]
@@ -108,7 +115,7 @@ begin
   { intros p q hp hq, simp [hp, hq, add_smul] },
   { intros n a hna,
     rw [mul_comm, pow_succ, mul_assoc, alg_hom.map_mul, linear_map.mul_apply, mul_comm, hna],
-    simp [algebra_map_End_apply, mem_eigenspace_iff.1 h.2, smul_smul, mul_comm] }
+    simp [algebra_map_End_apply, mem_eigenspace_iff.1 h.1, smul_smul, mul_comm] }
 end
 
 section minpoly
@@ -118,7 +125,7 @@ theorem is_root_of_has_eigenvalue {f : End K V} {μ : K} (h : f.has_eigenvalue 
 begin
   rcases (submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩,
   refine or.resolve_right (smul_eq_zero.1 _) ne0,
-  simp [← aeval_apply_of_has_eigenvector ⟨ne0, H⟩, minpoly.aeval K f],
+  simp [← aeval_apply_of_has_eigenvector ⟨H, ne0⟩, minpoly.aeval K f],
 end
 
 variables [finite_dimensional K V] (f : End K V)
@@ -155,40 +162,15 @@ theorem has_eigenvalue_iff_is_root :
 end minpoly
 
 /-- Every linear operator on a vector space over an algebraically closed field has
-    an eigenvalue. (Lemma 5.21 of [axler2015]) -/
+    an eigenvalue. -/
+-- This is Lemma 5.21 of [axler2015], although we are no longer following that proof.
 lemma exists_eigenvalue [is_alg_closed K] [finite_dimensional K V] [nontrivial V] (f : End K V) :
   ∃ (c : K), f.has_eigenvalue c :=
 begin
-  -- Since the vector space is finite dimensional,
-  -- there must be a nonzero polynomial `p` such that `aeval f p = 0` and hence not invertible.
-  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := f.is_integral,
-  have h_eval_p_not_unit : aeval f p ∉ is_unit.submonoid (End K V),
-  { rw ←aeval_def at h_eval_p,
-    rw [h_eval_p, is_unit.mem_submonoid_iff],
-    exact not_is_unit_zero, },
-  -- Hence, there must be a factor `q` of `p` such that `aeval f q` is not invertible.
-  obtain ⟨q, hq_factor, hq_nonunit⟩ : ∃ q, q ∈ factors p ∧ ¬ is_unit (aeval f q),
-  { simp only [←not_imp, (is_unit.mem_submonoid_iff _).symm],
-    apply not_forall.1 (λ h, h_eval_p_not_unit
-      (ring_hom_mem_submonoid_of_factors_subset_of_units_subset
-      (eval₂_ring_hom' (algebra_map _ _) f _)
-      (is_unit.submonoid (End K V)) p h_mon.ne_zero h _)),
-    simp only [is_unit.mem_submonoid_iff, linear_map.is_unit_iff],
-    apply ker_aeval_ring_hom'_unit_polynomial },
-  -- Since the field is algebraically closed, `q` has degree 1.
-  have h_deg_q : q.degree = 1 := is_alg_closed.degree_eq_one_of_irreducible _
-    (ne_zero_of_mem_factors h_mon.ne_zero hq_factor)
-    ((factors_spec p h_mon.ne_zero).1 q hq_factor),
-  -- Then the kernel of `aeval f q` is an eigenspace.
-  have h_eigenspace: eigenspace f (-q.coeff 0 / q.leading_coeff) = (aeval f q).ker,
-    from eigenspace_aeval_polynomial_degree_1 f q h_deg_q,
-  -- Since `aeval f q` is not invertible, the kernel is not `⊥`,
-  -- and thus there exists an eigenvalue.
-  show ∃ (c : K), f.has_eigenvalue c,
-  { use -q.coeff 0 / q.leading_coeff,
-    rw [has_eigenvalue, h_eigenspace],
-    intro h_eval_ker,
-    exact hq_nonunit ((linear_map.is_unit_iff (aeval f q)).2 h_eval_ker) }
+  obtain ⟨c, nu⟩ := exists_spectrum_of_is_alg_closed_of_finite_dimensional K f,
+  use c,
+  rw linear_map.is_unit_iff at nu,
+  exact has_eigenvalue_of_has_eigenvector (exists_mem_ne_zero_of_ne_bot nu).some_spec,
 end
 
 /-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
@@ -234,7 +216,7 @@ begin
     have total_l' : finsupp.total μs V K xs l' = 0,
     { let g := f - algebra_map K (End K V) μ₀,
       have h_gμ₀: g (l μ₀ • xs μ₀) = 0,
-        by rw [linear_map.map_smul, linear_map.sub_apply, mem_eigenspace_iff.1 (h_eigenvec _).2,
+        by rw [linear_map.map_smul, linear_map.sub_apply, mem_eigenspace_iff.1 (h_eigenvec _).1,
           algebra_map_End_apply, sub_self, smul_zero],
       have h_useless_filter : finset.filter (λ (a : μs), l'_f a ≠ 0) l_support' = l_support',
       { rw finset.filter_congr _,
@@ -244,7 +226,7 @@ begin
       have bodies_eq : ∀ (μ : μs), l'_f μ • xs μ = g (l μ • xs μ),
       { intro μ,
         dsimp only [g, l'_f],
-        rw [linear_map.map_smul, linear_map.sub_apply, mem_eigenspace_iff.1 (h_eigenvec _).2,
+        rw [linear_map.map_smul, linear_map.sub_apply, mem_eigenspace_iff.1 (h_eigenvec _).1,
           algebra_map_End_apply, ←sub_smul, smul_smul, mul_comm] },
       rw [←linear_map.map_zero g, ←hl, finsupp.total_apply, finsupp.total_apply,
           finsupp.sum, finsupp.sum, linear_map.map_sum, h_l_support,
@@ -279,7 +261,7 @@ begin
     { rw [finsupp.total_apply, finsupp.sum, h_l_support,
           finset.sum_insert hμ₀, h_sum_l_support'_eq_0, add_zero] at hl,
       by_contra h,
-      exact (h_eigenvec μ₀).1 ((smul_eq_zero.1 hl).resolve_left h) },
+      exact (h_eigenvec μ₀).2 ((smul_eq_zero.1 hl).resolve_left h) },
     -- Thus, all coefficients in `l` are `0`.
     show l = 0,
     { ext μ,