English
On a basis element, liftNC sends (f,g) to f(b) · g(a) according to the coefficient and the multiplicative image.
Русский
На базисном элементе liftNC отправляет f(b) · g(a) согласно коэффициенту и образу по мультипликативному отображению.
LaTeX
$$$\\text{liftNC}(f,g)(\\mathrm{single}(a,b)) = f(b) \\cdot g(\\mathrm{Multiplicative.ofAdd}(a)).$$$
Lean4
/-- A non-commutative version of `AddMonoidAlgebra.lift`: given an additive homomorphism
`f : k →+ R` and a map `g : Multiplicative G → R`, returns the additive
homomorphism from `k[G]` such that `liftNC f g (single a b) = f b * g a`. If `f`
is a ring homomorphism and the range of either `f` or `g` is in center of `R`, then the result is a
ring homomorphism. If `R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra
homomorphism called `AddMonoidAlgebra.lift`. -/
def liftNC (f : k →+ R) (g : Multiplicative G → R) : k[G] →+ R :=
liftAddHom fun x : G => (AddMonoidHom.mulRight (g <| Multiplicative.ofAdd x)).comp f
