Theorems · Definition · ring theory

AddMonoidAlgebra.liftNC

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

A non-commutative version of AddMonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a map g : Multiplicative 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 AddMonoidAlgebra.lift.

Defined in

Mathlib.Algebra.MonoidAlgebra.Lift

Cited by

7 results in Mathlib

Foundations

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

Assumes

SemiringNonUnitalNonAssocSemiring