Documentation

Mathlib.LinearAlgebra.Charpoly.Basic

Characteristic polynomial #

We define the characteristic polynomial of f : M →ₗ[R] M, where M is a finite and free R-module. The proof that f.charpoly is the characteristic polynomial of the matrix of f in any basis is in LinearAlgebra/Charpoly/ToMatrix.

Main definition #

source
def LinearMap.charpoly {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
Polynomial R

The characteristic polynomial of f : M →ₗ[R] M.

Equations
Instances For
    source
    theorem LinearMap.charpoly_def {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
    f.charpoly = ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly
    source
    theorem LinearMap.eval_charpoly {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (t : R) :
    Polynomial.eval t f.charpoly = LinearMap.det ((algebraMap R (M →ₗ[R] M)) t - f)
    source
    @[simp]
    theorem LinearMap.charpoly_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] :
    charpoly 0 = Polynomial.X ^ Module.finrank R M
    source
    theorem LinearMap.charpoly_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] :
    charpoly 1 = (Polynomial.X - 1) ^ Module.finrank R M
    source
    theorem LinearMap.charpoly_monic {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
    f.charpoly.Monic
    source
    theorem LinearMap.charpoly_natDegree {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) [Nontrivial R] [StrongRankCondition R] :
    f.charpoly.natDegree = Module.finrank R M
    source
    theorem LinearMap.aeval_self_charpoly {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
    (Polynomial.aeval f) f.charpoly = 0

    The Cayley-Hamilton Theorem, that the characteristic polynomial of a linear map, applied to the linear map itself, is zero.

    See Matrix.aeval_self_charpoly for the equivalent statement about matrices.

    source
    theorem LinearMap.isIntegral {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) :
    IsIntegral R f
    source
    theorem LinearMap.minpoly_dvd_charpoly {K : Type u} {M : Type v} [Field K] [AddCommGroup M] [Module K M] [FiniteDimensional K M] (f : M →ₗ[K] M) :
    minpoly K f ∣ f.charpoly
    source
    theorem LinearMap.aeval_eq_aeval_mod_charpoly {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (p : Polynomial R) :
    (Polynomial.aeval f) p = (Polynomial.aeval f) (p %ₘ f.charpoly)

    Any endomorphism polynomial p is equivalent under evaluation to p %ₘ f.charpoly; that is, p is equivalent to a polynomial with degree less than the dimension of the module.

    source
    theorem LinearMap.pow_eq_aeval_mod_charpoly {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) (k : ℕ) :
    f ^ k = (Polynomial.aeval f) (Polynomial.X ^ k %ₘ f.charpoly)

    Any endomorphism power can be computed as the sum of endomorphism powers less than the dimension of the module.

    source
    theorem LinearMap.minpoly_coeff_zero_of_injective {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M} [Nontrivial R] (hf : Function.Injective ⇑f) :
    (minpoly R f).coeff 0 ≠ 0