English
The lifting construction liftNC provides a functorial way to extend linear/semiring homomorphisms from the base ring and the group to the monoid algebra, reflecting the rule on basis elements: liftNC f g (single a b) = f(b) · g(a).
Русский
Осуществляется поднимающее преобразование liftNC, расширяющее отображения из базы в моноидную алгебру, так что на базисном элементе выполняется правило: liftNC f g (single a b) = f(b) · g(a).
LaTeX
$$$liftNC\ f\ g : MonoidAlgebra k G \to R$ с нормируемыми свойствами, и на базисных элементах: \ liftNC\ f\ g(\text{single}(a,b)) = f b \cdot g a$$$
Lean4
@[simp]
theorem liftNC_single (f : k →+ R) (g : G → R) (a : G) (b : k) : liftNC f g (single a b) = f b * g a :=
liftAddHom_apply_single _ _ _
