English
The liftNC map respects multiplication up to commutativity constraints; for suitable h_comm, liftNC(f) (a*b) = liftNC(f) a · liftNC(f) b.
Русский
Правило умножения для liftNC сохраняется под соответствующими ограничениями на коммутативность: liftNC( a*b ) = liftNC(a)·liftNC(b).
LaTeX
$$$liftNC\ f\ g (a*b) = liftNC\ f\ g\ a \cdot liftNC\ f\ 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 : MonoidAlgebra k G) (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g y)) :
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_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
simp [mul_assoc, (h_comm hy).left_comm]
