English
The lift map from MonoidAlgebra to A is defined by transporting the G-action to a k-algebra homomorphism, i.e., lift k G A F = liftNC (algebraMap k A) F.
Русский
Карта lift из MonoidAlgebra в A задается переносом действия G в алгеброгомоморфизм над k: lift k G A F = liftNC (algebraMap k A) F.
LaTeX
$$$ \\text{lift} \\, k\\, G\\, A\\, F = \\text{liftNC}\\left( (\\mathrm{algebraMap}\\ k\\, A) \right) F $$$
Lean4
/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
`k[G] →ₐ[k] A`. -/
def lift : (Multiplicative G →* A) ≃ (k[G] →ₐ[k] A)
where
__ := MonoidAlgebra.lift k (Multiplicative G) A
invFun f := (f : k[G] →* A).comp (of k G)
toFun
F :=
{ MonoidAlgebra.lift k (Multiplicative G) A F with
toFun := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _ }
