Theorems · Theorem · linear algebra

LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero

∀ {M : Type u_2} [inst : AddCommGroup M] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  (f : Module.End R M) (I : Ideal R),
  LinearMap.range f ≤ I • ⊤ →
    ∃ p,
      p.Monic ∧
        p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0

The Cayley-Hamilton Theorem for f.g. modules over arbitrary rings states that for each 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 in [Matsumura 2.1][matsumura1987], which is stronger than those in [Eisenbud 4.3][Eisenbud1995] and [Atiyah-Macdonald 2.4][atiyah-macdonald].

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

Cited by

2 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupCommRingModuleModule.Finite