English
A k-algebra homomorphism from MonoidAlgebra k G to A is determined by its values on the basis elements single x 1.
Русский
К алгебра-гомоморфизму над полем k от MonoidAlgebra k G к A достаточно знать значения на базисных элементах single x 1.
LaTeX
$$$\\forall x \\; \\phi_1(\\mathrm{single}\\ x\\ 1) = \\phi_2(\\mathrm{single}\\ x\\ 1) \\Rightarrow \\phi_1 = \\phi_2$$$
Lean4
/-- The instance `Algebra k (MonoidAlgebra A G)` whenever we have `Algebra k A`.
In particular this provides the instance `Algebra k (MonoidAlgebra k G)`.
-/
@[to_additive (dont_translate := k A) /-- The instance `Algebra R k[G]` whenever we have `Algebra R k`.
In particular this provides the instance `Algebra k k[G]`. -/
]
instance algebra {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : Algebra k (MonoidAlgebra A G)
where
algebraMap := singleOneRingHom.comp (algebraMap k A)
smul_def' := fun r a => by
ext
dsimp
rw [single_one_mul_apply, Algebra.smul_def]
commutes' := fun r f => by
ext
dsimp
rw [single_one_mul_apply, mul_single_one_apply, Algebra.commutes]
