Group-like weight spaces for monoid-algebra comodules #
This file identifies the group-like weight space indexed by single g 1 with the usual weight
space of a comodule over a monoid algebra.
Main declaration #
TauCeti.Comodule.groupLikeWeightSpace_single_one: the group-like and monoid-algebra weight spaces agree.
@[simp]
theorem
TauCeti.Comodule.groupLikeWeightSpace_single_one
{R : Type u}
{G : Type v}
{M : Type w}
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
[Comodule R (MonoidAlgebra R G) M]
(g : G)
:
The generic group-like weight space at single g 1 is the usual monoid-algebra weight
space.