English
There is a natural equivalence between MonoidHom (Multiplicative G) A and k[G] →ₐ[k] A, given by lifting a monoid homomorphism to an algebra homomorphism (liftMagma), with inverse given by restriction to of k G.
Русский
Существует естественное биекция между моноидоманохомоморфизмами и алгебраическими гомоморфизмами, реализуемая преобразованием liftMagma и его обратной функцией.
LaTeX
$$$ (\\mathrm{liftMagma}\\ k\\ G\\ A) : (Multiplicative G \\to\\* A) \\simeq (k[G] \\to\\_{k} A) $$$
Lean4
/-- The functor `G ↦ k[G]`, from the category of magmas to the category of
non-unital, non-associative algebras over `k` is adjoint to the forgetful functor in the other
direction. -/
@[simps apply_apply symm_apply]
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (Multiplicative G →ₙ* A) ≃ (k[G] →ₙₐ[k] A) :=
{
(MonoidAlgebra.liftMagma k :
(Multiplicative G →ₙ* A) ≃
(_ →ₙₐ[k]
A)) with
toFun := fun f =>
{ (MonoidAlgebra.liftMagma k f :) with toFun := fun a => sum a fun m t => t • f (Multiplicative.ofAdd m) }
invFun := fun F => F.toMulHom.comp (ofMagma k G) }
