The characteristic polynomial and the fixed submodule

For an endomorphism f of a finite-dimensional vector space V, the fixed submodule f.fixedSubmodule is the eigenspace of f for the eigenvalue 1 (Module.End.eigenspace_one_eq_fixedSubmodule). Its dimension is therefore at most the multiplicity of 1 as a root of the characteristic polynomial, with equality when f is semisimple (Module.End.IsFinitelySemisimple.rootMultiplicity_charpoly), for example when f has finite order invertible in the field.

These multiplicities are read here on the reverse characteristic polynomial det(1 - t f) = f.charpoly.reverse, the denominator in Molien's formula. If f is semisimple with fixed space of dimension m, then det(1 - t f) = (1 - t) ^ m * R(t) with R(1) ≠ 0, which is the order of the pole of det(1 - t f)⁻¹ at t = 1. If the fixed space is a hyperplane, then det(1 - t f) = (1 - t) ^ (dim V - 1) * (1 - det(f) t) exactly, whether or not f is semisimple. Comparing the poles at t = 1 of Molien's series is how the degrees of the basic invariants of a pseudoreflection group are related to the order of the group and to its number of pseudoreflections.

Main results

• Module.End.IsFinitelySemisimple.rootMultiplicity_one_charpoly: for a semisimple endomorphism, the multiplicity of the root 1 of the characteristic polynomial is the dimension of the fixed submodule.
• Module.End.IsFinitelySemisimple.exists_reverse_charpoly_eq_one_sub_X_pow_mul: for a semisimple endomorphism, det(1 - t f) = (1 - t) ^ m * R(t) with m = dim V^f and R(1) ≠ 0.
• Module.End.reverse_charpoly_of_finrank_fixedSubmodule_add_one: if the fixed submodule is a hyperplane, then det(1 - t f) = (1 - t) ^ (dim V - 1) * (1 - det(f) t).

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge Studies in Advanced Mathematics 29, Cambridge University Press (1990), § 3.9.

theorem Module.End.finrank_fixedSubmodule_le_rootMultiplicity_one_charpoly {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) : finrank K ↥(LinearMap.fixedSubmodule f) ≤ Polynomial.rootMultiplicity 1 (LinearMap.charpoly f)

The dimension of the fixed submodule of an endomorphism is at most the multiplicity of 1 as a root of its characteristic polynomial.

theorem Module.End.IsFinitelySemisimple.rootMultiplicity_one_charpoly {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} (hf : f.IsFinitelySemisimple) : Polynomial.rootMultiplicity 1 (LinearMap.charpoly f) = finrank K ↥(LinearMap.fixedSubmodule f)

For a semisimple endomorphism, the multiplicity of 1 as a root of the characteristic polynomial is the dimension of the fixed submodule.

theorem Module.End.IsFinitelySemisimple.exists_reverse_charpoly_eq_one_sub_X_pow_mul {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : End K V} (hf : f.IsFinitelySemisimple) : ∃ (R : Polynomial K), (LinearMap.charpoly f).reverse = (1 - Polynomial.X) ^ finrank K ↥(LinearMap.fixedSubmodule f) * R ∧ Polynomial.eval 1 R ≠ 0

For a semisimple endomorphism f whose fixed submodule has dimension m, the reverse characteristic polynomial det(1 - t f) is (1 - t) ^ m times a polynomial that does not vanish at t = 1.

theorem Module.End.reverse_charpoly_of_finrank_fixedSubmodule_add_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : End K V) (h : finrank K ↥(LinearMap.fixedSubmodule f) + 1 = finrank K V) : (LinearMap.charpoly f).reverse = (1 - Polynomial.X) ^ finrank K ↥(LinearMap.fixedSubmodule f) * (1 - Polynomial.C (LinearMap.det f) * Polynomial.X)

If the fixed submodule of f is a hyperplane, of dimension m = dim V - 1, then the reverse characteristic polynomial is det(1 - t f) = (1 - t) ^ m * (1 - det(f) t). No semisimplicity is needed: a transvection, with det f = 1, gives (1 - t) ^ dim V.