English
Let k be a commutative semiring, G a monoid, and α a type. The free k[G]-module on α, denoted free k G α, carries a natural k[G]-basis indexed by α; this basis is realized inside the representation (free k G α).asModule via a canonical linear equivalence.
Русский
Пусть k — коммутативное полугруппа, G — моноид, α — множество. Свободный модуль над k[G] на α, обозначаемый free k G α, имеет естественную k[G]-базу, индексируемую α; эта база реализуется внутри представления (free k G α).asModule через каноническое линейное подобие.
LaTeX
$$$\exists \mathcal B: \text{Basis } \alpha \ (\operatorname{MonoidAlgebra} \, k \ G)\, (\mathrm{Representation.free}\ k\ G\ \alpha).\mathrm{asModule},$$$
Lean4
/-- `α` gives a `k[G]`-basis of the representation `free k G α`. -/
noncomputable def freeAsModuleBasis : Basis α (MonoidAlgebra k G) (free k G α).asModule where
repr := (finsuppLEquivFreeAsModule k G α).symm
