Products of endomorphisms #
This file proves that nilpotence and semisimplicity are preserved by componentwise products of endomorphisms.
Main declarations #
IsNilpotent.prodMap: a product of nilpotent endomorphisms is nilpotent.Module.End.IsSemisimple.prodMap: a product of semisimple endomorphisms is semisimple.
theorem
IsNilpotent.prodMap
{K : Type u}
{V : Type v}
{W : Type w}
[Semiring K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid W]
[Module K W]
{f : Module.End K V}
{g : Module.End K W}
(hf : IsNilpotent f)
(hg : IsNilpotent g)
:
IsNilpotent (LinearMap.prodMap f g)
The componentwise product of two nilpotent endomorphisms is nilpotent.
theorem
Module.End.IsSemisimple.prodMap
{K : Type u}
{V : Type v}
{W : Type w}
[CommRing K]
[AddCommGroup V]
[Module K V]
[AddCommGroup W]
[Module K W]
{f : End K V}
{g : End K W}
(hf : f.IsSemisimple)
(hg : g.IsSemisimple)
:
The componentwise product of two semisimple endomorphisms is semisimple.