English
From a module structure over MonoidAlgebra k G on M, construct a representation of G on the restricted scalars of M.
Русский
Из структуры модуля над MonoidAlgebra k G на M построим представление G на ограниченных скалярами M.
LaTeX
$$ofModule : Representation k G (RestrictScalars k (MonoidAlgebra k G) M)$$
Lean4
/-- Build a `Representation k G M` from a `[Module (MonoidAlgebra k G) M]`.
This version is not always what we want, as it relies on an existing `[Module k M]`
instance, along with a `[IsScalarTower k (MonoidAlgebra k G) M]` instance.
We remedy this below in `ofModule`
(with the tradeoff that the representation is defined
only on a type synonym of the original module.)
-/
noncomputable def ofModule' (M : Type*) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M]
[IsScalarTower k (MonoidAlgebra k G) M] : Representation k G M :=
(MonoidAlgebra.lift k G (M →ₗ[k] M)).symm (Algebra.lsmul k k M)
