mathlib3 documentation

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} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) [decidable_eq ι] :
matrix ι ι 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} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) [decidable_eq ι] (A : matrix ι ι R) (w : ι R) :
theorem pi_to_module.from_matrix_apply_single_one {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) [decidable_eq ι] (A : matrix ι ι R) (j : ι) :
((pi_to_module.from_matrix R b) A) (pi.single j 1) = finset.univ.sum (λ (i : ι), A i j b i)
def pi_to_module.from_End {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι 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} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) (f : module.End R M) (w : ι R) :
theorem pi_to_module.from_End_apply_single_one {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) [decidable_eq ι] (f : module.End R M) (i : ι) :
theorem pi_to_module.from_End_injective {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) (hb : submodule.span R (set.range b) = ) :
def matrix.represents {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] (b : ι M) [decidable_eq ι] (A : matrix ι ι R) (f : module.End R 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} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] {A : matrix ι ι R} {f : module.End R M} (h : matrix.represents b A f) (x : ι R) :
((fintype.total R R) b) (A.mul_vec x) = f (((fintype.total R R) b) x)
theorem matrix.represents_iff {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] {A : matrix ι ι R} {f : module.End R M} :
matrix.represents b A f (x : ι R), ((fintype.total R R) b) (A.mul_vec x) = f (((fintype.total R R) b) x)
theorem matrix.represents_iff' {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] {A : matrix ι ι R} {f : module.End R M} :
matrix.represents b A 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} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] {A A' : matrix ι ι R} {f f' : module.End R M} (h : matrix.represents b A f) (h' : matrix.represents b A' f') :
matrix.represents b (A * A') (f * f')
theorem matrix.represents.one {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] :
theorem matrix.represents.add {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] {A A' : matrix ι ι R} {f f' : module.End R M} (h : matrix.represents b A f) (h' : matrix.represents b A' f') :
matrix.represents b (A + A') (f + f')
theorem matrix.represents.zero {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] :
theorem matrix.represents.smul {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} [decidable_eq ι] {A : matrix ι ι R} {f : module.End R M} (h : matrix.represents b A f) (r : R) :
matrix.represents b (r A) (r f)
theorem matrix.represents.eq {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] {R : Type u_3} [comm_ring R] [module R M] {b : ι M} (hb : submodule.span R (set.range b) = ) [decidable_eq ι] {A : matrix ι ι R} {f f' : module.End R M} (h : matrix.represents b A f) (h' : matrix.represents b A f') :
f = f'
def matrix.is_representation {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) [decidable_eq ι] :
subalgebra R (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} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) (hb : submodule.span R (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.eq_to_End_of_represents {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) (hb : submodule.span R (set.range b) = ) [decidable_eq ι] (A : (matrix.is_representation R b)) {f : module.End R M} (h : matrix.represents b A f) :
theorem matrix.is_representation.to_End_exists_mem_ideal {ι : Type u_1} [fintype ι] {M : Type u_2} [add_comm_group M] (R : Type u_3) [comm_ring R] [module R M] (b : ι M) (hb : submodule.span R (set.range b) = ) [decidable_eq ι] (f : module.End R M) (I : ideal R) (hI : linear_map.range f I ) :
(M_1 : (matrix.is_representation R b)), (matrix.is_representation.to_End R b hb) M_1 = f (i j : ι), M_1.val i j I

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.