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}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
[DecidableEq ι]
:
The composition of a matrix (as an endomorphism of ι → R) with the projection
(ι → R) →ₗ[R] M.
Equations
- PiToModule.fromMatrix R b = (LinearMap.llcomp R (ι → R) (ι → R) M) ((Fintype.total R R) b) ∘ₗ AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')
Instances For
theorem
PiToModule.fromMatrix_apply
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
[DecidableEq ι]
(A : Matrix ι ι R)
(w : ι → R)
:
((PiToModule.fromMatrix R b) A) w = ((Fintype.total R R) b) (Matrix.mulVec A w)
theorem
PiToModule.fromMatrix_apply_single_one
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
[DecidableEq ι]
(A : Matrix ι ι R)
(j : ι)
:
((PiToModule.fromMatrix R b) A) (Pi.single j 1) = Finset.sum Finset.univ fun (i : ι) => A i j • b i
def
PiToModule.fromEnd
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
:
Module.End R M →ₗ[R] (ι → R) →ₗ[R] M
The endomorphisms of M acts on (ι → R) →ₗ[R] M, and takes the projection
to a (ι → R) →ₗ[R] M.
Equations
- PiToModule.fromEnd R b = LinearMap.lcomp R M ((Fintype.total R R) b)
Instances For
theorem
PiToModule.fromEnd_apply
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(f : Module.End R M)
(w : ι → R)
:
((PiToModule.fromEnd R b) f) w = f (((Fintype.total R R) b) w)
theorem
PiToModule.fromEnd_apply_single_one
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
[DecidableEq ι]
(f : Module.End R M)
(i : ι)
:
((PiToModule.fromEnd R b) f) (Pi.single i 1) = f (b i)
theorem
PiToModule.fromEnd_injective
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(hb : Submodule.span R (Set.range b) = ⊤)
:
def
Matrix.Represents
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
(b : ι → M)
[DecidableEq ι]
(A : Matrix ι ι R)
(f : Module.End R M)
:
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 = ((PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f)
Instances For
theorem
Matrix.Represents.congr_fun
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
{A : Matrix ι ι R}
{f : Module.End R M}
(h : Matrix.Represents b A f)
(x : ι → R)
:
((Fintype.total R R) b) (Matrix.mulVec A x) = f (((Fintype.total R R) b) x)
theorem
Matrix.represents_iff
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
{A : Matrix ι ι R}
{f : Module.End R M}
:
Matrix.Represents b A f ↔ ∀ (x : ι → R), ((Fintype.total R R) b) (Matrix.mulVec A x) = f (((Fintype.total R R) b) x)
theorem
Matrix.represents_iff'
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
{A : Matrix ι ι R}
{f : Module.End R M}
:
Matrix.Represents b A f ↔ ∀ (j : ι), (Finset.sum Finset.univ fun (i : ι) => A i j • b i) = f (b j)
theorem
Matrix.Represents.mul
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
{A : Matrix ι ι R}
{A' : Matrix ι ι R}
{f : Module.End R M}
{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}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
:
Matrix.Represents b 1 1
theorem
Matrix.Represents.add
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
{A : Matrix ι ι R}
{A' : Matrix ι ι R}
{f : Module.End R M}
{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}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
:
Matrix.Represents b 0 0
theorem
Matrix.Represents.smul
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
{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.algebraMap
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
[DecidableEq ι]
(r : R)
:
Matrix.Represents b ((algebraMap R (Matrix ι ι R)) r) ((algebraMap R (Module.End R M)) r)
theorem
Matrix.Represents.eq
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
{R : Type u_3}
[CommRing R]
[Module R M]
{b : ι → M}
(hb : Submodule.span R (Set.range b) = ⊤)
[DecidableEq ι]
{A : Matrix ι ι R}
{f : Module.End R M}
{f' : Module.End R M}
(h : Matrix.Represents b A f)
(h' : Matrix.Represents b A f')
:
f = f'
def
Matrix.isRepresentation
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
[DecidableEq ι]
:
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}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(hb : Submodule.span R (Set.range b) = ⊤)
[DecidableEq ι]
:
↥(Matrix.isRepresentation R b) →ₐ[R] Module.End R M
The map sending a matrix to the endomorphism it represents. This is an R-algebra morphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Matrix.isRepresentation.toEnd_represents
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(hb : Submodule.span R (Set.range b) = ⊤)
[DecidableEq ι]
(A : ↥(Matrix.isRepresentation R b))
:
Matrix.Represents b (↑A) ((Matrix.isRepresentation.toEnd R b hb) A)
theorem
Matrix.isRepresentation.eq_toEnd_of_represents
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(hb : Submodule.span R (Set.range b) = ⊤)
[DecidableEq ι]
(A : ↥(Matrix.isRepresentation R b))
{f : Module.End R M}
(h : Matrix.Represents b (↑A) f)
:
(Matrix.isRepresentation.toEnd R b hb) A = f
theorem
Matrix.isRepresentation.toEnd_exists_mem_ideal
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(hb : Submodule.span R (Set.range b) = ⊤)
[DecidableEq ι]
(f : Module.End R M)
(I : Ideal R)
(hI : LinearMap.range f ≤ I • ⊤)
:
∃ (M_1 : ↥(Matrix.isRepresentation R b)), (Matrix.isRepresentation.toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
theorem
Matrix.isRepresentation.toEnd_surjective
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
(b : ι → M)
(hb : Submodule.span R (Set.range b) = ⊤)
[DecidableEq ι]
:
theorem
LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
[Module.Finite R M]
(f : Module.End R M)
(I : Ideal R)
(hI : LinearMap.range f ≤ I • ⊤)
:
∃ (p : Polynomial R),
Polynomial.Monic p ∧ (∀ (k : ℕ), Polynomial.coeff p k ∈ I ^ (Polynomial.natDegree p - k)) ∧ (Polynomial.aeval f) 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}
[AddCommGroup M]
(R : Type u_3)
[CommRing R]
[Module R M]
[Module.Finite R M]
(f : Module.End R M)
:
∃ (p : Polynomial R), Polynomial.Monic p ∧ (Polynomial.aeval f) p = 0