Theorems · Definition · ring theory

MonoidAlgebra.liftNC

{k : Type u₁} →
  {G : Type u₂} →
    {R : Type u_2} →
      [inst : Semiring k] → [inst_1 : NonUnitalNonAssocSemiring R] → (k →+ R) → (G → R) → MonoidAlgebra k G →+ R

A non-commutative version of MonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a homomorphism g : G → R, returns the additive homomorphism from k[G] such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called MonoidAlgebra.lift.

Defined in

Mathlib.Algebra.MonoidAlgebra.Lift

Cited by

6 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringNonUnitalNonAssocSemiring