Theorems · Theorem · ring theory

SkewMonoidAlgebra.lift_unique

∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  (F : SkewMonoidAlgebra k G →ₐ[k] A) (f : SkewMonoidAlgebra k G),
  F f = f.sum fun a b => b • F (SkewMonoidAlgebra.single a 1)

Decomposition of a k-algebra homomorphism from SkewMonoidAlgebra k G by its values on F (single a 1).

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Lift

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringMonoidSemiringAlgebraMulSemiringActionSMulCommClass