Transporting semisimplicity of an endomorphism along an injection #
LinearEquiv.isSemisimple_iff transports semisimplicity between two endomorphisms intertwined by
a linear equivalence. For one of the two directions an injection is enough: an endomorphism that
embeds equivariantly into a semisimple one is semisimple, just as a submodule of a semisimple
module is semisimple.
Main results #
Module.End.IsSemisimple.of_injective: semisimplicity passes to an endomorphism that admits an injective intertwiner into a semisimple one.
theorem
Module.End.IsSemisimple.of_injective
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[AddCommGroup N]
[Module R N]
{f : End R M}
{g : End R N}
(hg : g.IsSemisimple)
(i : M →ₗ[R] N)
(hi : Function.Injective ⇑i)
(hcomm : i ∘ₗ f = g ∘ₗ i)
:
Semisimplicity descends along an injective intertwiner. If i is injective and carries
f to g, and g is semisimple, then so is f.