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 ι] :
The composition of a matrix (as an endomporphism of ι → R) with the projection
(ι → R) →ₗ[R] M.
Equations
- pi_to_module.from_matrix R b = (⇑(linear_map.llcomp R (ι → R) (ι → R) M) (⇑(fintype.total R R) b)).comp alg_equiv_matrix'.symm.to_linear_map
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) :
⇑(⇑(pi_to_module.from_matrix R b) A) w = ⇑(⇑(fintype.total R R) b) (A.mul_vec w)
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
- pi_to_module.from_End R b = linear_map.lcomp R M (⇑(fintype.total R R) b)
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) :
⇑(⇑(pi_to_module.from_End R b) f) w = ⇑f (⇑(⇑(fintype.total R R) b) w)
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
- matrix.represents b A f = (⇑(pi_to_module.from_matrix R b) A = ⇑(pi_to_module.from_End R b) f)
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 ι] :
matrix.represents b 1 1
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 ι] :
matrix.represents b 0 0
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
- matrix.is_representation R b = {carrier := {A : matrix ι ι R | ∃ (f : module.End R M), matrix.represents b A f}, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
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 ι] :
↥(matrix.is_representation R b) →ₐ[R] module.End R M
The map sending a matrix to the endomorphism it represents. This is an R-algebra morphism.
Equations
- matrix.is_representation.to_End R b hb = {to_fun := λ (A : ↥(matrix.is_representation R b)), Exists.some _, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
matrix.is_representation.to_End_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)) :
matrix.represents b ↑A (⇑(matrix.is_representation.to_End R b hb) A)
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) :
⇑(matrix.is_representation.to_End R b hb) 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 • ⊤) :
theorem
matrix.is_representation.to_End_surjective
{ι : 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 ι] :
theorem
linear_map.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
{M : Type u_2}
[add_comm_group M]
(R : Type u_3)
[comm_ring R]
[module R M]
[module.finite R M]
(f : module.End R M)
(I : ideal R)
(hI : linear_map.range f ≤ 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.
theorem
linear_map.exists_monic_and_aeval_eq_zero
{M : Type u_2}
[add_comm_group M]
(R : Type u_3)
[comm_ring R]
[module R M]
[module.finite R M]
(f : module.End R M) :
∃ (p : polynomial R), p.monic ∧ ⇑(polynomial.aeval f) p = 0