# mathlib3documentation

linear_algebra.matrix.charpoly.linear_map

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a fixed finite spanning set b : ι → M of a 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 pi_to_module.from_matrix {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) [decidable_eq ι] :
ι R →ₗ[R] R) →ₗ[R] M

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

Equations
theorem pi_to_module.from_matrix_apply {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) [decidable_eq ι] (A : ι R) (w : ι R) :
( A) w = ( R) b) (A.mul_vec w)
theorem pi_to_module.from_matrix_apply_single_one {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) [decidable_eq ι] (A : ι R) (j : ι) :
( A) 1) = finset.univ.sum (λ (i : ι), A i j b i)
def pi_to_module.from_End {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) :
M →ₗ[R] R) →ₗ[R] M

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

Equations
theorem pi_to_module.from_End_apply {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (f : M) (w : ι R) :
( f) w = f (( R) b) w)
theorem pi_to_module.from_End_apply_single_one {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) [decidable_eq ι] (f : M) (i : ι) :
( f) 1) = f (b i)
theorem pi_to_module.from_End_injective {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (hb : (set.range b) = ) :
def matrix.represents {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] (b : ι M) [decidable_eq ι] (A : ι R) (f : M) :
Prop

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
theorem matrix.represents.congr_fun {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] {A : ι R} {f : M} (h : f) (x : ι R) :
( R) b) (A.mul_vec x) = f (( R) b) x)
theorem matrix.represents_iff {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] {A : ι R} {f : M} :
f (x : ι R), ( R) b) (A.mul_vec x) = f (( R) b) x)
theorem matrix.represents_iff' {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] {A : ι R} {f : M} :
f (j : ι), finset.univ.sum (λ (i : ι), A i j b i) = f (b j)
theorem matrix.represents.mul {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] {A A' : ι R} {f f' : M} (h : f) (h' : f') :
(A * A') (f * f')
theorem matrix.represents.one {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] :
1
theorem matrix.represents.add {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] {A A' : ι R} {f f' : M} (h : f) (h' : f') :
(A + A') (f + f')
theorem matrix.represents.zero {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] :
0
theorem matrix.represents.smul {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} [decidable_eq ι] {A : ι R} {f : M} (h : f) (r : R) :
(r A) (r f)
theorem matrix.represents.eq {ι : Type u_1} [fintype ι] {M : Type u_2} {R : Type u_3} [comm_ring R] [ M] {b : ι M} (hb : (set.range b) = ) [decidable_eq ι] {A : ι R} {f f' : M} (h : f) (h' : f') :
f = f'
def matrix.is_representation {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) [decidable_eq ι] :
(matrix ι ι R)

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

Equations
noncomputable def matrix.is_representation.to_End {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (hb : (set.range b) = ) [decidable_eq ι] :

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

Equations
theorem matrix.is_representation.to_End_represents {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (hb : (set.range b) = ) [decidable_eq ι] (A : ) :
( hb) A)
theorem matrix.is_representation.eq_to_End_of_represents {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (hb : (set.range b) = ) [decidable_eq ι] (A : ) {f : M} (h : f) :
hb) A = f
theorem matrix.is_representation.to_End_exists_mem_ideal {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (hb : (set.range b) = ) [decidable_eq ι] (f : M) (I : ideal R) (hI : I ) :
(M_1 : b)), hb) M_1 = f (i j : ι), M_1.val i j I
theorem matrix.is_representation.to_End_surjective {ι : Type u_1} [fintype ι] {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] (b : ι M) (hb : (set.range b) = ) [decidable_eq ι] :
theorem linear_map.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] [ M] (f : M) (I : ideal R) (hI : I ) :
(p : , p.monic ( (k : ), p.coeff k I ^ (p.nat_degree - 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 linear_map.exists_monic_and_aeval_eq_zero {M : Type u_2} (R : Type u_3) [comm_ring R] [ M] [ M] (f : M) :
(p : , p.monic p = 0