The characteristic polynomial on an invariant submodule and its quotient

An endomorphism f of a module V that preserves a submodule W restricts to an endomorphism f.restrict _ of W and induces an endomorphism Submodule.mapQ W W f _ of V ⧸ W. When W and V ⧸ W are free of finite rank, the characteristic polynomial of f is the product of those of the two induced endomorphisms. In a basis of V made of a basis of W and a lift of a basis of V ⧸ W (Module.Basis.sumQuot), the matrix of f is block upper triangular with these two endomorphisms on the diagonal. This is the characteristic-polynomial analogue of Mathlib's LinearMap.det_eq_det_mul_det, and its proof is the same.

No complement of W is chosen, so W need not be a direct summand stable under f: over a field this computes the characteristic polynomial of f on W from those of f on V and on V ⧸ W in every characteristic.

Main results

• LinearMap.charpoly_eq_charpoly_restrict_mul_charpoly_mapQ: the characteristic polynomial of f is the product of those of its restriction to W and of the endomorphism it induces on V ⧸ W.

theorem LinearMap.charpoly_eq_charpoly_restrict_mul_charpoly_mapQ {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] [Module.Finite R V] (W : Submodule R V) [Module.Free R ↥W] [Module.Finite R ↥W] [Module.Free R (V ⧸ W)] [Module.Finite R (V ⧸ W)] (f : V →ₗ[R] V) (hf : W ≤ Submodule.comap f W) : f.charpoly = (f.restrict hf).charpoly * (W.mapQ W f hf).charpoly

The characteristic polynomial is multiplicative on an invariant submodule and its quotient. If f preserves W, then the characteristic polynomial of f is the product of the characteristic polynomials of the restriction of f to W and of the endomorphism of V ⧸ W induced by f.