English
The graded structure on gradeR by f is internally realized within the direct-sum decomposition, ensuring multiplication respects the grading.
Русский
Градиационная структура gradeR по f реализуется внутри прямого разложения, гарантирующая совместимость умножения с градацией.
LaTeX
$$$\mathrm{IsInternal}(\mathrm{grade}\;R)$$$
Lean4
/-- A non-commutative version of `MonoidAlgebra.lift`: given an additive homomorphism `f : k →+ R`
and a homomorphism `g : G → R`, returns the additive homomorphism from
`MonoidAlgebra 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
`MonoidAlgebra.lift`. -/
def liftNC (f : k →+ R) (g : G → R) : MonoidAlgebra k G →+ R :=
liftAddHom fun x : G => (AddMonoidHom.mulRight (g x)).comp f
