English
There exists a linear isomorphism of k[G]-modules between the k[G]-module structure on the left action of G on itself and the regular k[G]-module MonoidAlgebra k G. In other words, the left action of G on itself (viewed as a k[G]-module) is isomorphic to the regular representation of G on the group algebra.
Русский
Существует линейное изоморфизм модулей над k[G] между структурой модуля левого действия G на G и обычной k[G]-модулю MonoidAlgebra k G. Иными словами, левое действие G на самом G как модуль над k[G] изоморфно регулярному представлению G на групповой алгебре.
LaTeX
$$$ (\\text{ofMulAction } k G G).asModule \\simeq_{\\mathrm{MonoidAlgebra } k G} \\ MonoidAlgebra k G $$$
Lean4
/-- If we equip `k[G]` with the `k`-linear `G`-representation induced by the left regular action of
`G` on itself, the resulting object is isomorphic as a `k[G]`-module to `k[G]` with its natural
`k[G]`-module structure. -/
@[simps]
noncomputable def ofMulActionSelfAsModuleEquiv : (ofMulAction k G G).asModule ≃ₗ[MonoidAlgebra k G] MonoidAlgebra k G :=
{ (asModuleEquiv _).toAddEquiv with map_smul' := ofMulAction_self_smul_eq_mul }
