Theorems · Definition · ring theory

SkewMonoidAlgebra.liftNC

{k : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid k] →
      {R : Type u_5} → [inst_1 : NonUnitalNonAssocSemiring R] → (k →+ R) → (G → R) → SkewMonoidAlgebra k G →+ R

A non-commutative version of SkewMonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a homomorphism g : G → R, returns the additive homomorphism from SkewMonoidAlgebra k G such that liftNC f g (single a b) = f b * g a. If k is a semiring and f is a ring homomorphism and for all x : R, y : G the equality (f (y • x)) * g y = (g y) * (f x)) holds, then the result is a ring homomorphism (see SkewMonoidAlgebra.liftNCRingHom). If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called SkewMonoidAlgebra.lift.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddCommMonoidNonUnitalNonAssocSemiring