liftNCRingHom — Mathlib

English

There exists a RingHom liftNCRingHom f g h_comm from AddMonoidAlgebra k G to R, built from liftNC with the given commuting hypothesis.

Русский

Существует кольцевой гомоморфизм liftNCRingHom f g h_comm из AddMonoidAlgebra k G в R, построенный на liftNC при условии commuting.

LaTeX

$$$ liftNCRingHom\; f\; g\; h\; :\; AddMonoidAlgebra\; k\; G \to+* R $$$

Lean4

/-- `liftNC` as a `RingHom`, for when `f` and `g` commute -/
def liftNCRingHom (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) : k[G] →+* R :=
  { liftNC (f : k →+ R) g with
    map_one' := liftNC_one _ _
    map_mul' := fun _a _b => liftNC_mul _ _ _ _ fun {_ _} _ => h_comm _ _ }

Похожие утверждения