The faithfulness trick #
An element of the group algebra that kills every simple submodule
of the regular module is zero: by Maschke the regular module is a
supremum of simple submodules, so 1 decomposes as a finite sum
of elements of simples, and left multiplication kills each
summand.
theorem
RS.eq_zero_of_kills_simples
{G : Type u_1}
[Group G]
[Finite G]
(x : MonoidAlgebra ℂ G)
(hx :
∀ (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)), IsSimpleModule (MonoidAlgebra ℂ G) ↥S → ∀ s ∈ S, x * s = 0)
:
The faithfulness trick: killing every simple submodule of the regular module forces vanishing.