feat(LinearAlgebra/Eigenspace/Minpoly): reduce typeclass assumptions (#29898)

Co-authored-by: Aristotle Harmonic <aristotle-harmonic@harmonic.fun>

Author: llllvvuu

Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

@@ -3,8 +3,10 @@ Copyright (c) 2020 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp
 -/
+import Mathlib.Algebra.Polynomial.Roots
+import Mathlib.FieldTheory.Minpoly.Basic
 import Mathlib.LinearAlgebra.Eigenspace.Basic
-import Mathlib.FieldTheory.Minpoly.Field
+import Mathlib.RingTheory.IntegralClosure.Algebra.Basic
 
 /-!
 # Eigenvalues are the roots of the minimal polynomial.
@@ -25,29 +27,22 @@ open Polynomial Module
 
 open scoped Polynomial
 
-variable {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V]
+section CommSemiring
 
-theorem eigenspace_aeval_polynomial_degree_1 (f : End K V) (q : K[X]) (hq : degree q = 1) :
-    eigenspace f (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker (aeval f q) :=
-  calc
-    eigenspace f (-q.coeff 0 / q.leadingCoeff)
-    _ = LinearMap.ker (q.leadingCoeff • f - algebraMap K (End K V) (-q.coeff 0)) := by
-          rw [eigenspace_div]
-          intro h
-          rw [leadingCoeff_eq_zero_iff_deg_eq_bot.1 h] at hq
-          cases hq
-    _ = LinearMap.ker (aeval f (C q.leadingCoeff * X + C (q.coeff 0))) := by
-          rw [C_mul', aeval_def]; simp [algebraMap, Algebra.algebraMap]
-    _ = LinearMap.ker (aeval f q) := by rwa [← eq_X_add_C_of_degree_eq_one]
+variable {R : Type v} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+theorem ker_aeval_ring_hom'_unit_polynomial (f : End R M) (c : R[X]ˣ) :
+    LinearMap.ker (aeval f (c : R[X])) = ⊥ :=
+  LinearMap.ker_eq_bot'.mpr fun m hm ↦ by
+    simpa [← mul_apply, ← aeval_mul] using congr(c⁻¹.1.aeval f $hm)
 
-theorem ker_aeval_ring_hom'_unit_polynomial (f : End K V) (c : K[X]ˣ) :
-    LinearMap.ker (aeval f (c : K[X])) = ⊥ := by
-  rw [Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
-  simp only [aeval_def, eval₂_C]
-  apply ker_algebraMap_end
-  apply coeff_coe_units_zero_ne_zero c
+end CommSemiring
 
-theorem aeval_apply_of_hasEigenvector {f : End K V} {p : K[X]} {μ : K} {x : V}
+section CommRing
+
+variable {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {μ : R}
+
+theorem aeval_apply_of_hasEigenvector {f : End R M} {p : R[X]} {μ : R} {x : M}
     (h : f.HasEigenvector μ x) : aeval f p x = p.eval μ • x := by
   refine p.induction_on ?_ ?_ ?_
   · intro a; simp [Module.algebraMap_end_apply]
@@ -57,41 +52,41 @@ theorem aeval_apply_of_hasEigenvector {f : End K V} {p : K[X]} {μ : K} {x : V}
     simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X,
       LinearMap.map_smulₛₗ, RingHom.id_apply, mul_comm]
 
-theorem isRoot_of_hasEigenvalue {f : End K V} {μ : K} (h : f.HasEigenvalue μ) :
-    (minpoly K f).IsRoot μ := by
+theorem isRoot_of_hasEigenvalue [NoZeroSMulDivisors R M] {f : End R M} {μ : R}
+    (h : f.HasEigenvalue μ) : (minpoly R f).IsRoot μ := by
   rcases (Submodule.ne_bot_iff _).1 h with ⟨w, ⟨H, ne0⟩⟩
   refine Or.resolve_right (smul_eq_zero.1 ?_) ne0
-  simp [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩, minpoly.aeval K f]
-
-variable [FiniteDimensional K V] (f : End K V)
-variable {f} {μ : K}
-
-theorem hasEigenvalue_of_isRoot (h : (minpoly K f).IsRoot μ) : f.HasEigenvalue μ := by
-  obtain ⟨p, hp⟩ := dvd_iff_isRoot.2 h
-  rw [hasEigenvalue_iff, eigenspace_def]
-  intro con
-  obtain ⟨u, hu⟩ := (LinearMap.isUnit_iff_ker_eq_bot _).2 con
-  have p_ne_0 : p ≠ 0 := by
-    intro con
-    apply minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := K) f)
-    rw [hp, con, mul_zero]
-  have : (aeval f) p = 0 := by
-    have h_aeval := minpoly.aeval K f
-    revert h_aeval
-    simp [hp, ← hu, Algebra.algebraMap_eq_smul_one]
-  have h_deg := minpoly.degree_le_of_ne_zero K f p_ne_0 this
-  rw [hp, degree_mul, degree_X_sub_C, Polynomial.degree_eq_natDegree p_ne_0] at h_deg
-  norm_cast at h_deg
-  cutsat
-
-theorem hasEigenvalue_iff_isRoot : f.HasEigenvalue μ ↔ (minpoly K f).IsRoot μ :=
+  rw [← aeval_apply_of_hasEigenvector ⟨H, ne0⟩]
+  simp
+
+section IsDomain
+
+variable [IsDomain R] [Module.Finite R M]
+
+theorem hasEigenvalue_of_isRoot (h : (minpoly R f).IsRoot μ) : f.HasEigenvalue μ := by
+  obtain ⟨q, hq⟩ := dvd_iff_isRoot.mpr h
+  obtain ⟨v, hv⟩ : ∃ v : M, q.aeval f v ≠ 0 := by
+    by_contra! h_contra
+    have := minpoly.min R f
+      ((monic_X_sub_C μ).of_mul_monic_left (hq ▸ minpoly.monic (Algebra.IsIntegral.isIntegral f)))
+      (LinearMap.ext h_contra)
+    rw [hq, degree_mul, degree_X_sub_C, degree_eq_natDegree] at this
+    · norm_cast at this; grind
+    · rintro rfl
+      exact minpoly.ne_zero (Algebra.IsIntegral.isIntegral f) (mul_zero (X - C μ) ▸ hq)
+  refine Module.End.hasEigenvalue_of_hasEigenvector (hasEigenvector_iff.mpr ⟨?_, hv⟩)
+  simpa [sub_eq_zero, hq] using congr($(minpoly.aeval R f) v)
+
+variable [NoZeroSMulDivisors R M]
+
+theorem hasEigenvalue_iff_isRoot : f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ :=
   ⟨isRoot_of_hasEigenvalue, hasEigenvalue_of_isRoot⟩
 
 variable (f)
 
 lemma finite_hasEigenvalue : Set.Finite f.HasEigenvalue := by
-  have h : minpoly K f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := K) f)
-  convert (minpoly K f).rootSet_finite K
+  have h : minpoly R f ≠ 0 := minpoly.ne_zero (Algebra.IsIntegral.isIntegral (R := R) f)
+  convert (minpoly R f).rootSet_finite R
   ext μ
   change f.HasEigenvalue μ ↔ _
   rw [hasEigenvalue_iff_isRoot, mem_rootSet_of_ne h, IsRoot, coe_aeval_eq_eval]
@@ -100,6 +95,29 @@ lemma finite_hasEigenvalue : Set.Finite f.HasEigenvalue := by
 noncomputable instance : Fintype f.Eigenvalues :=
   Set.Finite.fintype f.finite_hasEigenvalue
 
+end IsDomain
+
+end CommRing
+
+section Field
+
+variable {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V]
+
+theorem eigenspace_aeval_polynomial_degree_1 (f : End K V) (q : K[X]) (hq : degree q = 1) :
+    eigenspace f (-q.coeff 0 / q.leadingCoeff) = LinearMap.ker (aeval f q) :=
+  calc
+    eigenspace f (-q.coeff 0 / q.leadingCoeff)
+    _ = LinearMap.ker (q.leadingCoeff • f - algebraMap K (End K V) (-q.coeff 0)) := by
+          rw [eigenspace_div]
+          intro h
+          rw [leadingCoeff_eq_zero_iff_deg_eq_bot.1 h] at hq
+          cases hq
+    _ = LinearMap.ker (aeval f (C q.leadingCoeff * X + C (q.coeff 0))) := by
+          rw [C_mul', aeval_def]; simp [algebraMap, Algebra.algebraMap]
+    _ = LinearMap.ker (aeval f q) := by rwa [← eq_X_add_C_of_degree_eq_one]
+
+end Field
+
 end End
 
 end Module