# Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

# 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.

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) ()
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.sum Finset.univ 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.

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.

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) () = 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) () = 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.sum Finset.univ 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.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.

Instances For
noncomputable def Matrix.isRepresentation.toEnd {ι : Type u_1} [] {M : Type u_2} [] (R : Type u_3) [] [Module R M] (b : ιM) (hb : = ) [] :
{ x // } →ₐ[R]

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

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 : { x // }) :
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 : { x // }) {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, ↑() M = f ∀ (i j : ι), M 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, (∀ (k : ), I ^ ()) ↑() 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 = 0