English
Let f be a ring hom f: k →+* R and g a multiplicative hom from G to R. For elements a, b in k[G], if for every x ∈ G and every y with y in the support of a the images f(b x) and g(ofAdd y) commute, then the liftNC map is multiplicative on a and b: liftNC (f) g (a b) = liftNC (f) g a · liftNC (f) g b.
Русский
Пусть f — кольцевый однородный гомоморфизм f: k →+* R и g — мультипликативный гомоморфизм из G в R. Для элементов a, b ∈ k[G], если для всех x ∈ G и всех y ∈ supp(a) изображения f(b x) и g(ofAdd y) коммутируют, тогда отображение liftNC является умножением на этих элементах: liftNC (f) g (a b) = liftNC (f) g a · liftNC (f) g b.
LaTeX
$$$\forall f:\; k \to+* R,\; g:\; (Multiplicative\ G) \to* R,\; a,b:\; k[G],\; (\forall x\, y,\ y \in a.supp \Rightarrow Commute (f (b x)) (g \; (Multiplicative.ofAdd\ y))) \\Rightarrow liftNC (f) g (a b) = liftNC (f) g a \cdot liftNC (f) g b$$$
Lean4
theorem liftNC_mul {g_hom : Type*} [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R]
(f : k →+* R) (g : g_hom) (a b : k[G])
(h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g <| Multiplicative.ofAdd y)) :
liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b :=
MonoidAlgebra.liftNC_mul f g _ _ @h_comm
