English
There is a canonical RingHom from SkewMonoidAlgebra k G to R provided RingHom f: k →+ R and MonoidHom g: G →* R with a commutativity condition h_comm between f and g; this RingHom is named liftNCRingHom and uses liftNC on coefficients.
Русский
Существует каноническое кольцо-однозначное отображение (RingHom) из SkewMonoidAlgebra k G в R, заданное RingHom f: k →+ R и MonoidHom g: G →* R при условии совместимости h_comm; отображение называется liftNCRingHom и реализуется через liftNC на коэффициентах.
LaTeX
$$$ liftNCRingHom (f) (g) (h\_comm) : SkewMonoidAlgebra k G \to+* R $$$
Lean4
/-- `liftNC` as a `RingHom`, for when `f x` and `g y` commute -/
def liftNCRingHom (f : k →+* R) (g : G →* R) (h_comm : ∀ {x y}, (f (y • x)) * g y = (g y) * (f x)) :
SkewMonoidAlgebra k G →+* R where
__ := liftNC (f : k →+ R) g
map_one' := liftNC_one _ _
map_mul' _ _ := liftNC_mul _ _ _ _ fun {_ _} _ ↦ h_comm
