Semisimple linear endomorphisms

Given an R-module M together with an R-linear endomorphism f : M → M, the following two conditions are equivalent:

1. Every f-invariant submodule of M has an f-invariant complement.
2. M is a semisimple R[X]-module, where the action of the polynomial ring is induced by f.

A linear endomorphism f satisfying these equivalent conditions is known as a semisimple endomorphism. We provide basic definitions and results about such endomorphisms in this file.

Main definitions / results:

• Module.End.IsSemisimple: the definition that a linear endomorphism is semisimple
• Module.End.isSemisimple_iff: the characterisation of semisimplicity in terms of invariant submodules.
• Module.End.eq_zero_of_isNilpotent_isSemisimple: the zero endomorphism is the only endomorphism that is both nilpotent and semisimple.
• Module.End.isSemisimple_of_squarefree_aeval_eq_zero: an endomorphism that is a root of a square-free polynomial is semisimple (in finite dimensions over a field).

TODO

In finite dimensions over a field:

• Sum / difference / product of commuting semisimple endomorphisms is semisimple
• If semisimple then generalized eigenspace is eigenspace
• Converse of Module.End.isSemisimple_of_squarefree_aeval_eq_zero
• Restriction of semisimple endomorphism is semisimple
• Triangularizable iff diagonalisable for semisimple endomorphisms

@[inline, reducible]

abbrev Module.End.IsSemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) : Prop

A linear endomorphism of an R-module M is called semisimple if the induced R[X]-module structure on M is semisimple. This is equivalent to saying that every f-invariant R-submodule of M has an f-invariant complement: see Module.End.isSemisimple_iff.

Equations

• Module.End.IsSemisimple f = IsSemisimpleModule (Polynomial R) (Module.AEval' f)

theorem Module.End.isSemisimple_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : Module.End.IsSemisimple f ↔ ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q

@[simp]

theorem Module.End.isSemisimple_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : Module.End.IsSemisimple 0

@[simp]

theorem Module.End.isSemisimple_id {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : Module.End.IsSemisimple LinearMap.id

@[simp]

theorem Module.End.isSemisimple_neg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : Module.End.IsSemisimple (-f) ↔ Module.End.IsSemisimple f

theorem Module.End.eq_zero_of_isNilpotent_isSemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (hn : IsNilpotent f) (hs : Module.End.IsSemisimple f) : f = 0

theorem Module.End.IsSemisimple_smul_iff {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {t : K} (ht : t ≠ 0) : Module.End.IsSemisimple (t • f) ↔ Module.End.IsSemisimple f

theorem Module.End.IsSemisimple_smul {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} (t : K) (h : Module.End.IsSemisimple f) : Module.End.IsSemisimple (t • f)

theorem Module.End.isSemisimple_of_squarefree_aeval_eq_zero {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] {p : Polynomial K} (hp : Squarefree p) (hpf : (Polynomial.aeval f) p = 0) : Module.End.IsSemisimple f