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.linearCombination R b) ∘ₗ algEquivMatrix'.symm.toLinearMap
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)
:
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 : ι)
:
def
PiToModule.fromEnd
{ι : Type u_1}
[Fintype ι]
{M : Type u_2}
[AddCommGroup M]
(R : Type u_3)
[CommRing 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
- PiToModule.fromEnd R b = LinearMap.lcomp R M (Fintype.linearCombination 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)
:
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 : ι)
:
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) = ⊤)
:
Function.Injective ⇑(fromEnd R 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 : Represents b A f)
(x : ι → R)
:
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}
:
Represents b A f ↔ ∀ (x : ι → R), (Fintype.linearCombination R b) (A.mulVec x) = f ((Fintype.linearCombination 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}
:
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 A' : Matrix ι ι R}
{f f' : Module.End R M}
(h : Represents b A f)
(h' : Represents b A' f')
:
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 ι]
:
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 A' : Matrix ι ι R}
{f f' : Module.End R M}
(h : Represents b A f)
(h' : Represents b A' f')
:
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 ι]
:
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 : Represents b A f)
(r : R)
:
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)
:
Represents b ((_root_.algebraMap R (Matrix ι ι R)) r) ((_root_.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}
[DecidableEq ι]
(hb : Submodule.span R (Set.range b) = ⊤)
{A : Matrix ι ι R}
{f f' : Module.End R M}
(h : Represents b A f)
(h' : Represents b A 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)
[DecidableEq ι]
(hb : Submodule.span R (Set.range b) = ⊤)
:
The map sending a matrix to the endomorphism it represents. This is an R-algebra morphism.
Equations
- Matrix.isRepresentation.toEnd R b hb = { toFun := fun (A : ↥(Matrix.isRepresentation R b)) => Exists.choose ⋯, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
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)
[DecidableEq ι]
(hb : Submodule.span R (Set.range b) = ⊤)
(A : ↥(isRepresentation R b))
:
Represents b (↑A) ((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)
[DecidableEq ι]
(hb : Submodule.span R (Set.range b) = ⊤)
(A : ↥(isRepresentation R b))
{f : Module.End R M}
(h : Represents b (↑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)
[DecidableEq ι]
(hb : Submodule.span R (Set.range b) = ⊤)
(f : Module.End R M)
(I : Ideal R)
(hI : LinearMap.range f ≤ I • ⊤)
:
∃ (M_1 : ↥(isRepresentation R b)), (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)
[DecidableEq ι]
(hb : Submodule.span R (Set.range b) = ⊤)
:
Function.Surjective ⇑(toEnd R b hb)
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 : 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
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), p.Monic ∧ (Polynomial.aeval f) p = 0