Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap

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 ι] :
Matrix ι ι R →ₗ[R] (ιR) →ₗ[R] M

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

Equations
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) (A.mulVec 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) = 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
    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
      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) (A.mulVec 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) (A.mulVec 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 : ι), 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 ι] :
        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 ι] :
        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 ι] :

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

          Equations
          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)) :
            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) :
            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), p.Monic (∀ (k : ), p.coeff k I ^ (p.natDegree - 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), p.Monic (Polynomial.aeval f) p = 0