Every simple module embeds in the regular module #
Every simple ℂ[G]-module is isomorphic (as a module) to a simple
submodule of the regular module MonoidAlgebra ℂ G.
theorem
RS.exists_simple_submodule_linearEquiv
{G : Type u_1}
[Group G]
[Finite G]
(M : Type u_2)
[AddCommGroup M]
[Module (MonoidAlgebra ℂ G) M]
(hM : IsSimpleModule (MonoidAlgebra ℂ G) M)
:
∃ (S : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)),
IsSimpleModule (MonoidAlgebra ℂ G) ↥S ∧ Nonempty (↥S ≃ₗ[MonoidAlgebra ℂ G] M)
Every simple ℂ[G]-module is isomorphic to a simple submodule
of the regular module.