feat: strengthen Cayley-Hamilton (#37872)

* Strengthen the statement of Cayley-Hamilton to bound the degree of the annihilating polynomial by the number of generators
* Generalise `minpoly.natDegree_le` to non-free modules: `minpoly.natDegree_le_spanFinrank`

Author: artie2000

Mathlib.lean

@@ -4395,6 +4395,7 @@ public import Mathlib.FieldTheory.LinearDisjoint
 public import Mathlib.FieldTheory.Minpoly.Basic
 public import Mathlib.FieldTheory.Minpoly.ConjRootClass
 public import Mathlib.FieldTheory.Minpoly.Field
+public import Mathlib.FieldTheory.Minpoly.Finite
 public import Mathlib.FieldTheory.Minpoly.IsConjRoot
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.FieldTheory.Minpoly.MinpolyDiv

Mathlib/Algebra/Module/SpanRank.lean

@@ -189,6 +189,15 @@ theorem FG.exists_span_set_encard_eq_spanFinrank {p : Submodule R M} (h : p.FG)
   rw [Set.encard, ENat.card, spanFinrank, hs₁, this]
   simp
 
+/-- Constructs a generating finset with cardinality equal to the `spanFinrank` of the submodule
+  when the submodule is finitely generated. -/
+theorem FG.exists_span_finset_card_eq_spanFinrank {p : Submodule R M} (h : p.FG) :
+    ∃ s : Finset M, s.card = p.spanFinrank ∧ span R s = p := by
+  obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_encard_eq_spanFinrank h
+  have s_f := Set.finite_of_encard_eq_coe hs₁
+  refine ⟨s_f.toFinset, ⟨?_, by simpa using hs₂⟩⟩
+  simpa [s_f.encard_eq_coe_toFinset_card, ENat.coe_inj] using hs₁
+
 lemma lift_spanRank_le_iff_exists_span_set_card_le (p : Submodule R M) {a : Cardinal.{max u v}} :
     Cardinal.lift.{v} p.spanRank ≤ a ↔ ∃ s : Set M, Cardinal.lift.{v} #s ≤ a ∧ span R s = p := by
   constructor
@@ -220,6 +229,15 @@ lemma spanRank_bot : (⊥ : Ideal R).spanRank = 0 := Submodule.spanRank_eq_zero_
 @[simp]
 lemma spanFinrank_bot : (⊥ : Submodule R M).spanFinrank = 0 := by simp [spanFinrank]
 
+@[nontriviality]
+lemma spanRank_subsingleton [Subsingleton R] (p : Submodule R M) : p.spanRank = 0 := by
+  simp [nontriviality]
+
+@[nontriviality]
+lemma spanFinrank_subsingleton [Subsingleton R] (p : Submodule R M) : p.spanFinrank = 0 := by
+  have := Module.subsingleton R M
+  simp [Submodule.eq_bot_of_subsingleton]
+
 /-- Generating elements for the submodule of minimum cardinality. -/
 noncomputable def generators (p : Submodule R M) : Set M :=
   Classical.choose (exists_span_set_card_eq_spanRank p)

Mathlib/Analysis/Complex/Polynomial/Basic.lean

@@ -10,7 +10,6 @@ public import Mathlib.Analysis.Complex.Liouville
 public import Mathlib.FieldTheory.PolynomialGaloisGroup
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.Topology.Algebra.Polynomial
-public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # The fundamental theorem of algebra
@@ -199,7 +198,7 @@ lemma Irreducible.natDegree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree
   obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 :=
     IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'
   rw [← finrank_real_complex]
-  suffices p.natDegree = (minpoly ℝ z).natDegree from this ▸ minpoly.natDegree_le (R := ℝ) z
+  suffices p.natDegree = (minpoly ℝ z).natDegree from this ▸ minpoly.natDegree_le (A := ℝ) z
   rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
     natDegree_C, add_zero]
 

Mathlib/FieldTheory/Minpoly/Finite.lean

@@ -0,0 +1,43 @@
+/-
+Copyright (c) 2026 Artie Khovanov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Artie Khovanov
+-/
+module
+
+public import Mathlib.FieldTheory.Minpoly.Basic
+public import Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
+public import Mathlib.RingTheory.FiniteType
+
+/-!
+# Minimal polynomials on a finite algebra
+
+This file proves the bound on the degree of a minimal polynomial on an algebra that is finite as a module.
+
+-/
+
+@[expose] public section
+
+variable {A B : Type*} [CommRing A] [Ring B] [Algebra A B] [Module.Finite A B] (x : B)
+
+open Polynomial
+
+namespace minpoly
+
+variable (A) in
+theorem natDegree_le_spanFinrank :
+    (minpoly A x).natDegree ≤ (⊤ : Submodule A B).spanFinrank := by
+  rcases LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero _ (Algebra.lmul A _ x) with
+    ⟨f, f_monic, f_deg, f_aeval⟩
+  refine f_deg ▸ (natDegree_le_natDegree <| minpoly.min _ _ f_monic ?_)
+  rw [aeval_algHom_apply] at f_aeval
+  exact Algebra.lmul_injective (R := A) <| by simpa using f_aeval
+
+theorem natDegree_le [Module.Free A B] : (minpoly A x).natDegree ≤ Module.finrank A B := by
+  nontriviality A
+  simpa [Module.finrank_eq_spanFinrank_of_free] using natDegree_le_spanFinrank A x
+
+theorem degree_le [Module.Free A B] : (minpoly A x).degree ≤ Module.finrank A B :=
+  degree_le_of_natDegree_le <| natDegree_le x
+
+end minpoly

Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

@@ -5,10 +5,9 @@ Authors: Andrew Yang
 -/
 module
 
+public import Mathlib.FieldTheory.Minpoly.Finite
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.FieldTheory.PrimitiveElement
-public import Mathlib.FieldTheory.IsAlgClosed.Basic
-public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Results about `minpoly R x / (X - C x)`

Mathlib/FieldTheory/Normal/Basic.lean

@@ -6,10 +6,9 @@ Authors: Kenny Lau, Thomas Browning, Patrick Lutz
 module
 
 public import Mathlib.FieldTheory.Extension
-public import Mathlib.FieldTheory.Normal.Defs
-public import Mathlib.GroupTheory.Solvable
+public import Mathlib.FieldTheory.Minpoly.Finite
 public import Mathlib.FieldTheory.SplittingField.Construction
-public import Mathlib.LinearAlgebra.Charpoly.Basic
+public import Mathlib.GroupTheory.Solvable
 
 /-!
 # Normal field extensions

Mathlib/FieldTheory/PurelyInseparable/Exponent.lean

@@ -6,7 +6,6 @@ Authors: Michal Staromiejski
 module
 
 public import Mathlib.FieldTheory.PurelyInseparable.Basic
-public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 

Mathlib/LinearAlgebra/Charpoly/Basic.lean

@@ -5,10 +5,8 @@ Authors: Riccardo Brasca
 -/
 module
 
-public import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
-public import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
-public import Mathlib.LinearAlgebra.Determinant
 public import Mathlib.FieldTheory.Minpoly.Field
+public import Mathlib.LinearAlgebra.Determinant
 
 /-!
 
@@ -144,16 +142,4 @@ theorem Algebra.aeval_self_charpoly_lmul (α : M) :
   Algebra.lmul_injective (R := R) <| by
     simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α
 
-theorem minpoly.natDegree_le (α : M) :
-    (minpoly R α).natDegree ≤ Module.finrank R M := by
-  nontriviality R
-  let f := Algebra.lmul R _ α
-  have : (minpoly R α).natDegree ≤ f.charpoly.natDegree := natDegree_le_natDegree <|
-    minpoly.min _ _ f.charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
-  simpa [← (Algebra.lmul _ _ α).charpoly_natDegree]
-
-theorem minpoly.degree_le (α : M) :
-    (minpoly R α).degree ≤ Module.finrank R M :=
-  degree_le_of_natDegree_le (minpoly.natDegree_le α)
-
 end Algebra

Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
 public import Mathlib.LinearAlgebra.Matrix.ToLin
+public import Mathlib.Algebra.Module.SpanRank
 
 /-!
 
@@ -198,34 +199,46 @@ theorem Matrix.isRepresentation.toEnd_surjective :
 end
 
 /-- The **Cayley-Hamilton Theorem** for f.g. modules over arbitrary rings states that for each
-`R`-endomorphism `φ` of an `R`-module `M` such that `φ(M) ≤ I • M` for some ideal `I`, there
-exists some `n` and some `aᵢ ∈ Iⁱ` such that `φⁿ + a₁ φⁿ⁻¹ + ⋯ + aₙ = 0`.
+`R`-endomorphism `φ` of an `R`-module `M` generated by `n` elements such that `φ(M) ≤ I • M`
+for some ideal `I`, there exist some `aᵢ ∈ Iⁱ` such that `φⁿ + a₁ φⁿ⁻¹ + ⋯ + aₙ = 0`.
 
-This is the version found in Eisenbud 4.3, which is slightly weaker than Matsumura 2.1
-(this lacks the constraint on `n`), and is slightly stronger than Atiyah-Macdonald 2.4.
+This is the version in [Matsumura 2.1][matsumura1987], which is stronger than those in
+[Eisenbud 4.3][Eisenbud1995] and [Atiyah-Macdonald 2.4][atiyah-macdonald].
 -/
-theorem LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
+theorem LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero
     [Module.Finite R M] (f : Module.End R M) (I : Ideal R) (hI : LinearMap.range f ≤ I • ⊤) :
-    ∃ p : R[X], p.Monic ∧ (∀ k, p.coeff k ∈ I ^ (p.natDegree - k)) ∧ Polynomial.aeval f p = 0 := by
+    ∃ p : R[X], p.Monic ∧ p.natDegree = (⊤ : Submodule R M).spanFinrank ∧
+                (∀ k, p.coeff k ∈ I ^ (p.natDegree - k)) ∧ Polynomial.aeval f p = 0 := by
   classical
     cases subsingleton_or_nontrivial R
-    · exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩
-    obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ :=
-      Module.Finite.fg_top (R := R) (M := M)
-    have : Submodule.span R (Set.range ((↑) : { x // x ∈ s } → M)) = ⊤ := by
-      rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]
-    obtain ⟨A, rfl, h⟩ :=
-      Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
-    refine ⟨A.1.charpoly, A.1.charpoly_monic, ?_, ?_⟩
-    · rw [A.1.charpoly_natDegree_eq_dim]
-      exact coeff_charpoly_mem_ideal_pow h
-    · rw [Polynomial.aeval_algHom_apply,
-        ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
-      congr 1
-      ext1
-      rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
+    · exact ⟨0, by simp [nontriviality]⟩
+    obtain ⟨s, hs_card, hs_span⟩ :=
+      Submodule.FG.exists_span_finset_card_eq_spanFinrank (R := R) (M := M) Module.Finite.fg_top
+    have : Submodule.span R (Set.range ((↑) : s → M)) = ⊤ := by simp [hs_span]
+    obtain ⟨A, rfl, h⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M) this f I hI
+    refine ⟨A.1.charpoly, A.1.charpoly_monic, by simp [hs_card],
+            by simpa using coeff_charpoly_mem_ideal_pow h, ?_⟩
+    rw [Polynomial.aeval_algHom_apply,
+      ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) this)]
+    congr 1
+    ext1
+    rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
+
+@[deprecated
+"strengthened conclusion to
+`LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero`"
+(since := "2026-04-10")] alias
+LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul :=
+  LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero
+
+theorem LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero
+    [Module.Finite R M] (f : Module.End R M) :
+    ∃ p : R[X], p.Monic ∧ p.natDegree = (⊤ : Submodule R M).spanFinrank ∧
+                Polynomial.aeval f p = 0 :=
+  (LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero R f ⊤ (by simp)).imp
+    fun _ h ↦ h.imp_right (And.imp_right And.right)
 
 theorem LinearMap.exists_monic_and_aeval_eq_zero [Module.Finite R M] (f : Module.End R M) :
     ∃ p : R[X], p.Monic ∧ Polynomial.aeval f p = 0 :=
-  (LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul R f ⊤ (by simp)).imp
+  (LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero R f).imp
     fun _ h => h.imp_right And.right

Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Algebra.Algebra.Hom.Rat
 public import Mathlib.Analysis.Complex.Polynomial.Basic
 public import Mathlib.NumberTheory.NumberField.Basic
-public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Embeddings of number fields