mathlib3 documentation

linear_algebra.charpoly.basic

Characteristic polynomial #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 linear_algebra/charpoly/to_matrix.

Main definition #

source
noncomputable def linear_map.charpoly {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group 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
source
theorem linear_map.charpoly_def {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M] [module.free R M] [module.finite R M] (f : M →ₗ[R] M) :
f.charpoly = (⇑(linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R M)) f).charpoly
source
theorem linear_map.charpoly_monic {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M] [module.free R M] [module.finite R M] (f : M →ₗ[R] M) :
f.charpoly.monic
source
theorem linear_map.aeval_self_charpoly {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group 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 linear_map.is_integral {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M] [module.free R M] [module.finite R M] (f : M →ₗ[R] M) :
is_integral R f
source
theorem linear_map.minpoly_dvd_charpoly {K : Type u} {M : Type v} [field K] [add_comm_group M] [module K M] [finite_dimensional K M] (f : M →ₗ[K] M) :
minpoly K f ∣ f.charpoly
source
theorem linear_map.aeval_eq_aeval_mod_charpoly {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group 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 linear_map.pow_eq_aeval_mod_charpoly {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group 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 linear_map.minpoly_coeff_zero_of_injective {R : Type u} {M : Type v} [comm_ring R] [nontrivial R] [add_comm_group M] [module R M] [module.free R M] [module.finite R M] {f : M →ₗ[R] M} (hf : function.injective ⇑f) :
(minpoly R f).coeff 0 ≠ 0