English
There is a linear equivalence between the free k[G]-module on α and the finsupp representation on α with MonoidAlgebra k G as the base ring; i.e., the free module on α is isomorphic to Representation.free k G α as a MonoidAlgebra k G-module.
Русский
Существует линейное эквивалентности между свободным k[G]-модулем на α и представлением finsupp на α, основанным на MonoidAlgebra k G; то есть свободный модуль на α изоморфен Representation.free k G α как модуль MonoidAlgebra k G.
LaTeX
$$$ (\\alpha \\to_0 \\ MonoidAlgebra k G) \\simeq_{{MonoidAlgebra k G}} (Representation.free k G α).asModule $$$
Lean4
/-- The representation on `α →₀ k[G]` defined pointwise by the left regular representation. -/
noncomputable abbrev free (k G : Type*) [CommSemiring k] [Monoid G] (α : Type*) : Representation k G (α →₀ G →₀ k) :=
finsupp (leftRegular k G) α
