English
For a finite module M over a ring and endomorphism f with range contained in I M, there exists a monic polynomial p with coefficients in powers of I such that p(f)=0.
Русский
Для конечного модуля M над кольцом и конечномерного отображения f, удовлетворяющего условию диапазона, существует моническое полиномное p с коэффициентами в I^k, такое что p(f)=0.
LaTeX
$$$\\exists p\\in R[x], p\\text{ Monic} \\land (\\forall k, p\\text{ coeff }k \\in I^{(p.natDegree-k)}) \\land Polynomial.aeval\\, f\\, p = 0$$$
Lean4
/-- 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`.
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.
-/
theorem exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul [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
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]
