English
Under a compatibility condition h_comm ensuring commutativity of the coefficients, the map liftNC is multiplicative: liftNC f g (a · b) = liftNC f g a · liftNC f g b for a, b in the skew-monoid algebra.
Русский
При условии совместимости h_comm, гарантирующей совместность коэффициентов, отображение liftNC умножает: liftNC f g (a · b) = liftNC f g a · liftNC f g b для любых a, b в алгебре SkewMonoidAlgebra.
LaTeX
$$$ liftNC (f : k \to+ R) g (a * b) = liftNC (f : k \to+ R) g a * liftNC (f : k \to+ R) g b $$$
Lean4
theorem liftNC_mul {g_hom : Type*} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom)
(a b : SkewMonoidAlgebra k G)
(h_comm : ∀ {x y}, y ∈ a.support → (f (y • b.coeff x)) * g y = (g y) * (f (b.coeff x))) :
liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b :=
by
conv_rhs => rw [← sum_single a, ← sum_single b]
simp_rw [mul_def, map_sum, liftNC_single, sum_mul, mul_sum]
refine sum_congr fun y hy ↦ sum_congr fun x _hx ↦ ?_
simp only [AddMonoidHom.coe_coe, map_mul]
rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]
