Semisimple representations

This file defines the typeclass IsSemisimpleRepresentation for semisimple monoid representations.

@[reducible, inline]

abbrev Representation.IsSemisimpleRepresentation {k : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Prop

A representation is semisimple when every subrepresentation has a complement.

Equations

• ρ.IsSemisimpleRepresentation = ComplementedLattice (Subrepresentation ρ)

theorem Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [Monoid G] [Field k] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : ρ.IsSemisimpleRepresentation ↔ IsSemisimpleModule (MonoidAlgebra k G) ρ.asModule

theorem Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule {k : Type u_1} {G : Type u_2} [Monoid G] [Field k] (M : Type u_4) [AddCommGroup M] [Module (MonoidAlgebra k G) M] : IsSemisimpleModule (MonoidAlgebra k G) M ↔ (ofModule M).IsSemisimpleRepresentation