# Cayley-Hamilton theorem for f.g. modules. #

Given a fixed finite spanning set b : ι → M of an R-module M, we say that a matrix M represents an endomorphism f : M →ₗ[R] M if the matrix as an endomorphism of ι → R commutes with f via the projection (ι → R) →ₗ[R] M given by b.

We show that every endomorphism has a matrix representation, and if f.range ≤ I • ⊤ for some ideal I, we may furthermore obtain a matrix representation whose entries fall in I.

This is used to conclude the Cayley-Hamilton theorem for f.g. modules over arbitrary rings.

def PiToModule.fromMatrix {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) [] :
Matrix ι ι R →ₗ[R] (ιR) →ₗ[R] M

The composition of a matrix (as an endomorphism of ι → R) with the projection (ι → R) →ₗ[R] M.

Equations
• = (LinearMap.llcomp R (ιR) (ιR) M) (() b) ∘ₗ algEquivMatrix'.symm.toLinearMap
Instances For
theorem PiToModule.fromMatrix_apply {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) [] (A : Matrix ι ι R) (w : ιR) :
(() A) w = (() b) (A.mulVec w)
theorem PiToModule.fromMatrix_apply_single_one {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) [] (A : Matrix ι ι R) (j : ι) :
(() A) () = Finset.univ.sum fun (i : ι) => A i j b i
def PiToModule.fromEnd {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) :
→ₗ[R] (ιR) →ₗ[R] M

The endomorphisms of M acts on (ι → R) →ₗ[R] M, and takes the projection to a (ι → R) →ₗ[R] M.

Equations
Instances For
theorem PiToModule.fromEnd_apply {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (f : ) (w : ιR) :
(() f) w = f ((() b) w)
theorem PiToModule.fromEnd_apply_single_one {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) [] (f : ) (i : ι) :
(() f) () = f (b i)
theorem PiToModule.fromEnd_injective {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) :
def Matrix.Represents {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] (b : ιM) [] (A : Matrix ι ι R) (f : ) :

We say that a matrix represents an endomorphism of M if the matrix acting on ι → R is equal to f via the projection (ι → R) →ₗ[R] M given by a fixed (spanning) set.

Equations
• = (() A = () f)
Instances For
theorem Matrix.Represents.congr_fun {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] {A : Matrix ι ι R} {f : } (h : ) (x : ιR) :
(() b) (A.mulVec x) = f ((() b) x)
theorem Matrix.represents_iff {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] {A : Matrix ι ι R} {f : } :
∀ (x : ιR), (() b) (A.mulVec x) = f ((() b) x)
theorem Matrix.represents_iff' {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] {A : Matrix ι ι R} {f : } :
∀ (j : ι), (Finset.univ.sum fun (i : ι) => A i j b i) = f (b j)
theorem Matrix.Represents.mul {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] {A : Matrix ι ι R} {A' : Matrix ι ι R} {f : } {f' : } (h : ) (h' : Matrix.Represents b A' f') :
Matrix.Represents b (A * A') (f * f')
theorem Matrix.Represents.one {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] :
theorem Matrix.Represents.add {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] {A : Matrix ι ι R} {A' : Matrix ι ι R} {f : } {f' : } (h : ) (h' : Matrix.Represents b A' f') :
Matrix.Represents b (A + A') (f + f')
theorem Matrix.Represents.zero {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] :
theorem Matrix.Represents.smul {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] {A : Matrix ι ι R} {f : } (h : ) (r : R) :
Matrix.Represents b (r A) (r f)
theorem Matrix.Represents.algebraMap {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} [] (r : R) :
Matrix.Represents b ((algebraMap R (Matrix ι ι R)) r) ((algebraMap R ()) r)
theorem Matrix.Represents.eq {ι : Type u_1} [] {M : Type u_2} [] {R : Type u_3} [] [Module R M] {b : ιM} (hb : = ) [] {A : Matrix ι ι R} {f : } {f' : } (h : ) (h' : ) :
f = f'
def Matrix.isRepresentation {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) [] :
Subalgebra R (Matrix ι ι R)

The subalgebra of Matrix ι ι R that consists of matrices that actually represent endomorphisms on M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Matrix.isRepresentation.toEnd {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) [] :
() →ₐ[R]

The map sending a matrix to the endomorphism it represents. This is an R-algebra morphism.

Equations
• = { toFun := fun (A : ()) => , map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
theorem Matrix.isRepresentation.toEnd_represents {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) [] (A : ()) :
Matrix.Represents b (A) (() A)
theorem Matrix.isRepresentation.eq_toEnd_of_represents {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) [] (A : ()) {f : } (h : Matrix.Represents b (A) f) :
() A = f
theorem Matrix.isRepresentation.toEnd_exists_mem_ideal {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) [] (f : ) (I : ) (hI : I ) :
∃ (M_1 : ()), () M_1 = f ∀ (i j : ι), M_1 i j I
theorem Matrix.isRepresentation.toEnd_surjective {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) [] :
theorem LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul {M : Type u_2} [] (R : Type u_3) [] [Module R M] [] (f : ) (I : ) (hI : I ) :
∃ (p : ), p.Monic (∀ (k : ), p.coeff k I ^ (p.natDegree - k)) () p = 0

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 LinearMap.exists_monic_and_aeval_eq_zero {M : Type u_2} [] (R : Type u_3) [] [Module R M] [] (f : ) :
∃ (p : ), p.Monic () p = 0