Monoid algebras

When the domain of a Finsupp has a multiplicative or additive structure, we can define a convolution product. To mathematicians this structure is known as the "monoid algebra", i.e. the finite formal linear combinations over a given semiring of elements of a monoid M. The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.

In fact the construction of the "monoid algebra" makes sense when M is not even a monoid, but merely a magma, i.e., when M carries a multiplication which is not required to satisfy any conditions at all. In this case the construction yields a not-necessarily-unital, not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such algebras to magmas, and we prove this as MonoidAlgebra.liftMagma.

In this file we define MonoidAlgebra R M := M →₀ R, and AddMonoidAlgebra R M in the same way, and then define the convolution product on these.

When the domain is additive, this is used to define polynomials:

Polynomial R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)

Note: Polynomial R is currently a wrapper around AddMonoidAlgebra R ℕ and not defeq to it. There is ongoing work to make it defeq. See https://github.com/leanprover-community/mathlib4/pull/25273

When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

Notation

We introduce the notation R[M] for both MonoidAlgebra R M and AddMonoidAlgebra R M. The notations are scoped to their respective namespaces, and which one R[M] resolves to therefore depends on which of the two namespaces is open.

def MonoidAlgebra (R : Type u_8) (M : Type u_9) [Semiring R] : Type (max u_8 u_9)

The monoid algebra over a semiring R generated by the monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

Equations

• MonoidAlgebra R M = (M →₀ R)

def AddMonoidAlgebra (R : Type u_8) (M : Type u_9) [Semiring R] : Type (max u_8 u_9)

The additive monoid algebra over a semiring R generated by the additive monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

Equations

• AddMonoidAlgebra R M = (M →₀ R)

def AddMonoidAlgebra.«term__[_]» : Lean.TrailingParserDescr

The additive monoid algebra over a semiring R generated by the additive monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

Equations

• One or more equations did not get rendered due to their size.

def AddMonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for AddMonoidAlgebra.

Equations

• One or more equations did not get rendered due to their size.

def MonoidAlgebra.«term__[_]» : Lean.TrailingParserDescr

The monoid algebra over a semiring R generated by the monoid M.

It is the type of finite formal R-linear combinations of terms of M, endowed with the convolution product.

Equations

• One or more equations did not get rendered due to their size.

def MonoidAlgebra.unexpander : Lean.PrettyPrinter.Unexpander

Unexpander for MonoidAlgebra.

Equations

• One or more equations did not get rendered due to their size.

instance MonoidAlgebra.inhabited {M : Type u_2} {R : Type u_6} [Semiring R] : Inhabited (MonoidAlgebra R M)

Equations

• MonoidAlgebra.inhabited = inferInstanceAs (Inhabited (M →₀ R))

instance AddMonoidAlgebra.inhabited {M : Type u_2} {R : Type u_6} [Semiring R] : Inhabited (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.inhabited = inferInstanceAs (Inhabited (M →₀ R))

instance MonoidAlgebra.nontrivial {M : Type u_2} {R : Type u_6} [Semiring R] [Nontrivial R] [Nonempty M] : Nontrivial (MonoidAlgebra R M)

instance AddMonoidAlgebra.nontrivial {M : Type u_2} {R : Type u_6} [Semiring R] [Nontrivial R] [Nonempty M] : Nontrivial (AddMonoidAlgebra R M)

instance MonoidAlgebra.unique {M : Type u_2} {R : Type u_6} [Semiring R] [Subsingleton R] : Unique (MonoidAlgebra R M)

Equations

• MonoidAlgebra.unique = inferInstanceAs (Unique (M →₀ R))

instance AddMonoidAlgebra.unique {M : Type u_2} {R : Type u_6} [Semiring R] [Subsingleton R] : Unique (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.unique = inferInstanceAs (Unique (M →₀ R))

instance MonoidAlgebra.addCommMonoid {M : Type u_2} {R : Type u_6} [Semiring R] : AddCommMonoid (MonoidAlgebra R M)

Equations

• MonoidAlgebra.addCommMonoid = inferInstanceAs (AddCommMonoid (M →₀ R))

instance AddMonoidAlgebra.addAddCommMonoid {M : Type u_2} {R : Type u_6} [Semiring R] : AddCommMonoid (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.addAddCommMonoid = inferInstanceAs (AddCommMonoid (M →₀ R))

instance MonoidAlgebra.instIsCancelAdd {M : Type u_2} {R : Type u_6} [Semiring R] [IsCancelAdd R] : IsCancelAdd (MonoidAlgebra R M)

instance AddMonoidAlgebra.instIsCancelAdd {M : Type u_2} {R : Type u_6} [Semiring R] [IsCancelAdd R] : IsCancelAdd (AddMonoidAlgebra R M)

instance MonoidAlgebra.instCoeFun {M : Type u_2} {R : Type u_6} [Semiring R] : CoeFun (MonoidAlgebra R M) fun (x : MonoidAlgebra R M) => M → R

Equations

• MonoidAlgebra.instCoeFun = inferInstanceAs (CoeFun (M →₀ R) fun (x : M →₀ R) => M → R)

instance AddMonoidAlgebra.instCoeFun {M : Type u_2} {R : Type u_6} [Semiring R] : CoeFun (AddMonoidAlgebra R M) fun (x : AddMonoidAlgebra R M) => M → R

Equations

• AddMonoidAlgebra.instCoeFun = inferInstanceAs (CoeFun (M →₀ R) fun (x : M →₀ R) => M → R)

theorem MonoidAlgebra.ext {M : Type u_2} {R : Type u_6} [Semiring R] ⦃f g : MonoidAlgebra R M⦄ (hfg : ∀ (m : M), f m = g m) : f = g

A copy of Finsupp.ext for MonoidAlgebra.

theorem AddMonoidAlgebra.ext {M : Type u_2} {R : Type u_6} [Semiring R] ⦃f g : AddMonoidAlgebra R M⦄ (hfg : ∀ (m : M), f m = g m) : f = g

A copy of Finsupp.ext for AddMonoidAlgebra.

theorem MonoidAlgebra.ext_iff {M : Type u_2} {R : Type u_6} [Semiring R] {f g : MonoidAlgebra R M} : f = g ↔ ∀ (m : M), f m = g m

theorem AddMonoidAlgebra.ext_iff {M : Type u_2} {R : Type u_6} [Semiring R] {f g : AddMonoidAlgebra R M} : f = g ↔ ∀ (m : M), f m = g m

@[reducible, inline]

abbrev MonoidAlgebra.single {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) (r : R) : MonoidAlgebra R M

MonoidAlgebra.single m r for m : M, r : R is the element rm : R[M].

Equations

• MonoidAlgebra.single m r = Finsupp.single m r

@[reducible, inline]

abbrev AddMonoidAlgebra.single {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) (r : R) : AddMonoidAlgebra R M

AddMonoidAlgebra.single m r for m : M, r : R is the element rm : R[M].

Equations

• AddMonoidAlgebra.single m r = Finsupp.single m r

Basic scalar multiplication instances

This section collects instances needed for the algebraic structure of Polynomial, which is defined in terms of MonoidAlgebra. Further results on scalar multiplication can be found in Mathlib/Algebra/MonoidAlgebra/Module.lean.

instance MonoidAlgebra.smulZeroClass {M : Type u_2} {R : Type u_6} [Semiring R] {A : Type u_8} [SMulZeroClass A R] : SMulZeroClass A (MonoidAlgebra R M)

Equations

• MonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass

instance AddMonoidAlgebra.smulZeroClass {M : Type u_2} {R : Type u_6} [Semiring R] {A : Type u_8} [SMulZeroClass A R] : SMulZeroClass A (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass

@[simp]

theorem MonoidAlgebra.smul_apply {M : Type u_2} {R : Type u_6} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : MonoidAlgebra R M) (m : M) : (a • x) m = a • x m

@[simp]

theorem AddMonoidAlgebra.coeff_smul {M : Type u_2} {R : Type u_6} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (x : AddMonoidAlgebra R M) (m : M) : (a • x) m = a • x m

@[simp]

theorem MonoidAlgebra.smul_single {M : Type u_2} {R : Type u_6} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (m : M) (r : R) : a • single m r = single m (a • r)

@[simp]

theorem AddMonoidAlgebra.smul_single {M : Type u_2} {R : Type u_6} [Semiring R] {A : Type u_8} [SMulZeroClass A R] (a : A) (m : M) (r : R) : a • single m r = single m (a • r)

theorem MonoidAlgebra.smul_single' {M : Type u_2} {R : Type u_6} [Semiring R] (r' : R) (m : M) (r : R) : r' • single m r = single m (r' * r)

theorem AddMonoidAlgebra.smul_single' {M : Type u_2} {R : Type u_6} [Semiring R] (r' : R) (m : M) (r : R) : r' • single m r = single m (r' * r)

instance MonoidAlgebra.distribSMul {M : Type u_2} {N : Type u_3} {R : Type u_6} [Semiring R] [DistribSMul N R] : DistribSMul N (MonoidAlgebra R M)

Equations

• MonoidAlgebra.distribSMul = Finsupp.distribSMul M R

instance AddMonoidAlgebra.distribSMul {M : Type u_2} {N : Type u_3} {R : Type u_6} [Semiring R] [DistribSMul N R] : DistribSMul N (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.distribSMul = Finsupp.distribSMul M R

instance MonoidAlgebra.isScalarTower {M : Type u_2} {N : Type u_3} {O : Type u_4} {R : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] : IsScalarTower N O (MonoidAlgebra R M)

instance AddMonoidAlgebra.isScalarTower {M : Type u_2} {N : Type u_3} {O : Type u_4} {R : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] : IsScalarTower N O (AddMonoidAlgebra R M)

instance MonoidAlgebra.smulCommClass {M : Type u_2} {N : Type u_3} {O : Type u_4} {R : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] : SMulCommClass N O (MonoidAlgebra R M)

instance AddMonoidAlgebra.smulCommClass {M : Type u_2} {N : Type u_3} {O : Type u_4} {R : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] : SMulCommClass N O (AddMonoidAlgebra R M)

instance MonoidAlgebra.isCentralScalar {M : Type u_2} {N : Type u_3} {R : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] : IsCentralScalar N (MonoidAlgebra R M)

instance AddMonoidAlgebra.isCentralScalar {M : Type u_2} {N : Type u_3} {R : Type u_6} [Semiring R] [SMulZeroClass N R] [SMulZeroClass Nᵐᵒᵖ R] [IsCentralScalar N R] : IsCentralScalar N (AddMonoidAlgebra R M)

@[simp]

theorem MonoidAlgebra.coe_add {G : Type u_1} {R : Type u_6} [Semiring R] (f g : MonoidAlgebra R G) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem AddMonoidAlgebra.coe_add {G : Type u_1} {R : Type u_6} [Semiring R] (f g : AddMonoidAlgebra R G) : ⇑(f + g) = ⇑f + ⇑g

theorem MonoidAlgebra.single_zero {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) : single m 0 = 0

theorem AddMonoidAlgebra.single_zero {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) : single m 0 = 0

theorem MonoidAlgebra.single_add {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂

theorem AddMonoidAlgebra.single_add {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) (r₁ r₂ : R) : single m (r₁ + r₂) = single m r₁ + single m r₂

def MonoidAlgebra.singleAddHom {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) : R →+ MonoidAlgebra R M

MonoidAlgebra.single as an AddMonoidHom.

TODO: Rename to singleAddMonoidHom.

Equations

• MonoidAlgebra.singleAddHom m = { toFun := MonoidAlgebra.single m, map_zero' := ⋯, map_add' := ⋯ }

def AddMonoidAlgebra.singleAddHom {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) : R →+ AddMonoidAlgebra R M

AddMonoidAlgebra.single as an AddMonoidHom.

TODO: Rename to singleAddMonoidHom.

Equations

• AddMonoidAlgebra.singleAddHom m = { toFun := AddMonoidAlgebra.single m, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidAlgebra.singleAddHom_apply {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) (r : R) : (singleAddHom m) r = single m r

@[simp]

theorem AddMonoidAlgebra.singleAddHom_apply {M : Type u_2} {R : Type u_6} [Semiring R] (m : M) (r : R) : (singleAddHom m) r = single m r

theorem MonoidAlgebra.addHom_ext' {M : Type u_2} {R : Type u_6} [Semiring R] {N : Type u_8} [AddZeroClass N] ⦃f g : MonoidAlgebra R M →+ N⦄ (hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g

If two additive homomorphisms from R[M] are equal on each single r m, then they are equal.

We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is ℕ or ℤ, then it suffices to verify f (single a 1) = g (single a 1).

TODO: Rename to addMonoidHom_ext'.

theorem AddMonoidAlgebra.addHom_ext' {M : Type u_2} {R : Type u_6} [Semiring R] {N : Type u_8} [AddZeroClass N] ⦃f g : AddMonoidAlgebra R M →+ N⦄ (hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)) : f = g

If two additive homomorphisms from R[M] are equal on each single r m, then they are equal.

We formulate this using equality of AddMonoidHoms so that ext tactic can apply a type-specific extensionality lemma after this one. E.g., if the fiber M is ℕ or ℤ, then it suffices to verify f (single a 1) = g (single a 1).

TODO: Rename to addMonoidHom_ext'.

theorem AddMonoidAlgebra.addHom_ext'_iff {M : Type u_2} {R : Type u_6} [Semiring R] {N : Type u_8} [AddZeroClass N] {f g : AddMonoidAlgebra R M →+ N} : f = g ↔ ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)

theorem MonoidAlgebra.addHom_ext'_iff {M : Type u_2} {R : Type u_6} [Semiring R] {N : Type u_8} [AddZeroClass N] {f g : MonoidAlgebra R M →+ N} : f = g ↔ ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)

theorem MonoidAlgebra.sum_single_index {M : Type u_2} {N : Type u_3} {R : Type u_6} [Semiring R] [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) : Finsupp.sum (single m r) h = h m r

theorem AddMonoidAlgebra.sum_single_index {M : Type u_2} {N : Type u_3} {R : Type u_6} [Semiring R] [AddCommMonoid N] {m : M} {r : R} {h : M → R → N} (h_zero : h m 0 = 0) : Finsupp.sum (single m r) h = h m r

@[simp]

theorem MonoidAlgebra.sum_single {M : Type u_2} {R : Type u_6} [Semiring R] (x : MonoidAlgebra R M) : Finsupp.sum x single = x

@[simp]

theorem AddMonoidAlgebra.sum_single {M : Type u_2} {R : Type u_6} [Semiring R] (x : AddMonoidAlgebra R M) : Finsupp.sum x single = x

theorem MonoidAlgebra.single_apply {M : Type u_2} {R : Type u_6} [Semiring R] {a a' : M} {b : R} [Decidable (a = a')] : (single a b) a' = if a = a' then b else 0

theorem AddMonoidAlgebra.single_apply {M : Type u_2} {R : Type u_6} [Semiring R] {a a' : M} {b : R} [Decidable (a = a')] : (single a b) a' = if a = a' then b else 0

@[simp]

theorem MonoidAlgebra.single_eq_zero {M : Type u_2} {R : Type u_6} [Semiring R] {r : R} {m : M} : single m r = 0 ↔ r = 0

@[simp]

theorem AddMonoidAlgebra.single_eq_zero {M : Type u_2} {R : Type u_6} [Semiring R] {r : R} {m : M} : single m r = 0 ↔ r = 0

theorem MonoidAlgebra.single_ne_zero {M : Type u_2} {R : Type u_6} [Semiring R] {r : R} {m : M} : single m r ≠ 0 ↔ r ≠ 0

theorem AddMonoidAlgebra.single_ne_zero {M : Type u_2} {R : Type u_6} [Semiring R] {r : R} {m : M} : single m r ≠ 0 ↔ r ≠ 0

theorem MonoidAlgebra.induction_linear {M : Type u_2} {R : Type u_6} [Semiring R] {p : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (zero : p 0) (add : ∀ (x y : MonoidAlgebra R M), p x → p y → p (x + y)) (single : ∀ (m : M) (r : R), p (single m r)) : p x

theorem AddMonoidAlgebra.induction_linear {M : Type u_2} {R : Type u_6} [Semiring R] {p : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M) (zero : p 0) (add : ∀ (x y : AddMonoidAlgebra R M), p x → p y → p (x + y)) (single : ∀ (m : M) (r : R), p (single m r)) : p x

instance MonoidAlgebra.one {M : Type u_2} {R : Type u_6} [Semiring R] [One M] : One (MonoidAlgebra R M)

The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and 0 elsewhere.

Equations

• MonoidAlgebra.one = { one := MonoidAlgebra.single 1 1 }

instance AddMonoidAlgebra.zero {M : Type u_2} {R : Type u_6} [Semiring R] [Zero M] : One (AddMonoidAlgebra R M)

The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and 0 elsewhere.

Equations

• AddMonoidAlgebra.zero = { one := AddMonoidAlgebra.single 0 1 }

theorem MonoidAlgebra.one_def {M : Type u_2} {R : Type u_6} [Semiring R] [One M] : 1 = single 1 1

theorem AddMonoidAlgebra.one_def {M : Type u_2} {R : Type u_6} [Semiring R] [Zero M] : 1 = single 0 1

@[irreducible]

def MonoidAlgebra.mul' {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) : MonoidAlgebra R M

The multiplication in a monoid algebra.

We make it irreducible so that Lean doesn't unfold it when trying to unify two different things.

Equations

• x.mul' y = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => MonoidAlgebra.single (m₁ * m₂) (r₁ * r₂)

instance AddMonoidAlgebra.instMul {M : Type u_2} {R : Type u_6} [Semiring R] [Add M] : Mul (AddMonoidAlgebra R M)

The product of f g : k[G] is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x + y = a. (Think of the product of multivariate polynomials where α is the additive monoid of monomial exponents.)

Equations

• AddMonoidAlgebra.instMul = { mul := fun (f g : AddMonoidAlgebra R M) => MonoidAlgebra.mul' f g }

instance MonoidAlgebra.instMul {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] : Mul (MonoidAlgebra R M)

The product of x y : R[M] is the finitely supported function whose value at m is the sum of x m₁ * y m₂ over all pairs m₁, m₂ such that m₁ * m₂ = m.

(Think of the group ring of a group.)

Equations

• MonoidAlgebra.instMul = { mul := MonoidAlgebra.mul' }

theorem MonoidAlgebra.mul_def {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) : x * y = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => single (m₁ * m₂) (r₁ * r₂)

theorem AddMonoidAlgebra.mul_def {M : Type u_2} {R : Type u_6} [Semiring R] [Add M] (x y : AddMonoidAlgebra R M) : x * y = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => single (m₁ + m₂) (r₁ * r₂)

instance MonoidAlgebra.nonUnitalNonAssocSemiring {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] : NonUnitalNonAssocSemiring (MonoidAlgebra R M)

Equations

• MonoidAlgebra.nonUnitalNonAssocSemiring = { toAddCommMonoid := MonoidAlgebra.addCommMonoid, toMul := MonoidAlgebra.instMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

instance AddMonoidAlgebra.nonUnitalNonAssocSemiring {M : Type u_2} {R : Type u_6} [Semiring R] [Add M] : NonUnitalNonAssocSemiring (AddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

theorem MonoidAlgebra.mul_apply {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] [DecidableEq M] (x y : MonoidAlgebra R M) (m : M) : (x * y) m = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => if m₁ * m₂ = m then r₁ * r₂ else 0

theorem AddMonoidAlgebra.mul_apply {M : Type u_2} {R : Type u_6} [Semiring R] [Add M] [DecidableEq M] (x y : AddMonoidAlgebra R M) (m : M) : (x * y) m = Finsupp.sum x fun (m₁ : M) (r₁ : R) => Finsupp.sum y fun (m₂ : M) (r₂ : R) => if m₁ + m₂ = m then r₁ * r₂ else 0

theorem MonoidAlgebra.mul_apply_antidiagonal {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] (x y : MonoidAlgebra R M) (m : M) (s : Finset (M × M)) (hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m) : (x * y) m = ∑ p ∈ s, x p.1 * y p.2

theorem AddMonoidAlgebra.mul_apply_antidiagonal {M : Type u_2} {R : Type u_6} [Semiring R] [Add M] (x y : AddMonoidAlgebra R M) (m : M) (s : Finset (M × M)) (hs : ∀ {p : M × M}, p ∈ s ↔ p.1 + p.2 = m) : (x * y) m = ∑ p ∈ s, x p.1 * y p.2

@[simp]

theorem MonoidAlgebra.single_mul_single {M : Type u_2} {R : Type u_6} [Semiring R] [Mul M] (m₁ m₂ : M) (r₁ r₂ : R) : single m₁ r₁ * single m₂ r₂ = single (m₁ * m₂) (r₁ * r₂)

@[simp]

theorem AddMonoidAlgebra.single_mul_single {M : Type u_2} {R : Type u_6} [Semiring R] [Add M] (m₁ m₂ : M) (r₁ r₂ : R) : single m₁ r₁ * single m₂ r₂ = single (m₁ + m₂) (r₁ * r₂)

@[simp]

theorem MonoidAlgebra.single_commute_single {M : Type u_2} {R : Type u_6} [Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} [Mul M] (hm : Commute m₁ m₂) (hr : Commute r₁ r₂) : Commute (single m₁ r₁) (single m₂ r₂)

@[simp]

theorem AddMonoidAlgebra.single_commute_single {M : Type u_2} {R : Type u_6} [Semiring R] {r₁ r₂ : R} {m₁ m₂ : M} [Add M] (hm : AddCommute m₁ m₂) (hr : Commute r₁ r₂) : Commute (single m₁ r₁) (single m₂ r₂)

@[simp]

theorem MonoidAlgebra.single_commute {M : Type u_2} {R : Type u_6} [Semiring R] {r : R} {m : M} [Mul M] (hm : ∀ (m' : M), Commute m m') (hr : ∀ (r' : R), Commute r r') (x : MonoidAlgebra R M) : Commute (single m r) x

@[simp]

theorem AddMonoidAlgebra.single_commute {M : Type u_2} {R : Type u_6} [Semiring R] {r : R} {m : M} [Add M] (hm : ∀ (m' : M), AddCommute m m') (hr : ∀ (r' : R), Commute r r') (x : AddMonoidAlgebra R M) : Commute (single m r) x

theorem MonoidAlgebra.mul_single_apply_aux {M : Type u_2} {R : Type u_6} [Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Mul M] (H : ∀ m' ∈ x.support, m' * m = m₁ ↔ m' = m₂) : (x * single m r) m₁ = x m₂ * r

theorem AddMonoidAlgebra.mul_single_apply_aux {M : Type u_2} {R : Type u_6} [Semiring R] {x : AddMonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Add M] (H : ∀ m' ∈ x.support, m' + m = m₁ ↔ m' = m₂) : (x * single m r) m₁ = x m₂ * r

theorem MonoidAlgebra.single_mul_apply_aux {M : Type u_2} {R : Type u_6} [Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Mul M] (H : ∀ m' ∈ x.support, m * m' = m₁ ↔ m' = m₂) : (single m r * x) m₁ = r * x m₂

theorem AddMonoidAlgebra.single_mul_apply_aux {M : Type u_2} {R : Type u_6} [Semiring R] {x : AddMonoidAlgebra R M} {r : R} {m m₁ m₂ : M} [Add M] (H : ∀ m' ∈ x.support, m + m' = m₁ ↔ m' = m₂) : (single m r * x) m₁ = r * x m₂

@[simp]

theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul {M : Type u_2} {R : Type u_6} [Semiring R] {m m' : M} [Mul M] (r : R) (x : MonoidAlgebra R M) (h : ¬∃ (d : M), m' = d * m) : (x * single m r) m' = 0

@[simp]

theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add {M : Type u_2} {R : Type u_6} [Semiring R] {m m' : M} [Add M] (r : R) (x : AddMonoidAlgebra R M) (h : ¬∃ (d : M), m' = d + m) : (x * single m r) m' = 0

@[simp]

theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul {M : Type u_2} {R : Type u_6} [Semiring R] {m m' : M} [Mul M] (r : R) (x : MonoidAlgebra R M) (h : ¬∃ (d : M), m' = m * d) : (single m r * x) m' = 0

@[simp]

theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add {M : Type u_2} {R : Type u_6} [Semiring R] {m m' : M} [Add M] (r : R) (x : AddMonoidAlgebra R M) (h : ¬∃ (d : M), m' = m + d) : (single m r * x) m' = 0

def MonoidAlgebra.ofMagma (R : Type u_8) (M : Type u_9) [Semiring R] [Mul M] : M →ₙ* MonoidAlgebra R M

The embedding of a magma into its magma algebra.

Equations

• MonoidAlgebra.ofMagma R M = { toFun := fun (a : M) => MonoidAlgebra.single a 1, map_mul' := ⋯ }

@[simp]

theorem MonoidAlgebra.ofMagma_apply (R : Type u_8) (M : Type u_9) [Semiring R] [Mul M] (a : M) : (ofMagma R M) a = single a 1

instance MonoidAlgebra.nonUnitalSemiring {M : Type u_2} {R : Type u_6} [Semiring R] [Semigroup M] : NonUnitalSemiring (MonoidAlgebra R M)

Equations

• MonoidAlgebra.nonUnitalSemiring = { toNonUnitalNonAssocSemiring := MonoidAlgebra.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }

instance AddMonoidAlgebra.nonUnitalSemiring {M : Type u_2} {R : Type u_6} [Semiring R] [AddSemigroup M] : NonUnitalSemiring (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.nonUnitalSemiring = { toNonUnitalNonAssocSemiring := AddMonoidAlgebra.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }

instance MonoidAlgebra.nonAssocSemiring {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] : NonAssocSemiring (MonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance AddMonoidAlgebra.nonAssocSemiring {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] : NonAssocSemiring (AddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

theorem MonoidAlgebra.natCast_def {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] (n : ℕ) : ↑n = single 1 ↑n

theorem AddMonoidAlgebra.natCast_def {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (n : ℕ) : ↑n = single 0 ↑n

theorem MonoidAlgebra.mul_single_one_apply {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M) : (x * single 1 r) m = x m * r

theorem AddMonoidAlgebra.mul_single_zero_apply {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (x : AddMonoidAlgebra R M) (r : R) (m : M) : (x * single 0 r) m = x m * r

theorem MonoidAlgebra.single_one_mul_apply {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] (x : MonoidAlgebra R M) (r : R) (m : M) : (single 1 r * x) m = r * x m

theorem AddMonoidAlgebra.single_zero_mul_apply {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (x : AddMonoidAlgebra R M) (r : R) (m : M) : (single 0 r * x) m = r * x m

def MonoidAlgebra.of (R : Type u_8) (M : Type u_9) [Semiring R] [MulOneClass M] : M →* MonoidAlgebra R M

The embedding of a unital magma into its magma algebra.

Equations

• MonoidAlgebra.of R M = { toFun := fun (m : M) => MonoidAlgebra.single m 1, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidAlgebra.of_apply (R : Type u_8) (M : Type u_9) [Semiring R] [MulOneClass M] (m : M) : (of R M) m = single m 1

theorem MonoidAlgebra.of_injective {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] [Nontrivial R] : Function.Injective ⇑(of R M)

theorem MonoidAlgebra.of_commute {M : Type u_2} {R : Type u_6} [Semiring R] {m : M} [MulOneClass M] (h : ∀ (m' : M), Commute m m') (f : MonoidAlgebra R M) : Commute ((of R M) m) f

def MonoidAlgebra.singleHom {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] : R × M →* MonoidAlgebra R M

MonoidAlgebra.single as a MonoidHom from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of MonoidAlgebra.single.

Equations

• MonoidAlgebra.singleHom = { toFun := fun (a : R × M) => MonoidAlgebra.single a.2 a.1, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidAlgebra.singleHom_apply {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] (a : R × M) : singleHom a = single a.2 a.1

def MonoidAlgebra.singleOneRingHom {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] : R →+* MonoidAlgebra R M

MonoidAlgebra.single 1 as a RingHom

Equations

• MonoidAlgebra.singleOneRingHom = { toFun := MonoidAlgebra.single 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

def AddMonoidAlgebra.singleZeroRingHom {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] : R →+* AddMonoidAlgebra R M

AddMonoidAlgebra.single 1 as a RingHom

Equations

• AddMonoidAlgebra.singleZeroRingHom = { toFun := AddMonoidAlgebra.single 0, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidAlgebra.singleOneRingHom_apply {M : Type u_2} {R : Type u_6} [Semiring R] [MulOneClass M] (r : R) : singleOneRingHom r = single 1 r

@[simp]

theorem AddMonoidAlgebra.singleZeroRingHom_apply {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (r : R) : singleZeroRingHom r = single 0 r

theorem MonoidAlgebra.ringHom_ext {M : Type u_2} {R : Type u_6} {S : Type u_7} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} (h₁ : ∀ (r : R), f (single 1 r) = g (single 1 r)) (h_of : ∀ (m : M), f (single m 1) = g (single m 1)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 1 r, then they are equal.

theorem AddMonoidAlgebra.ringHom_ext {M : Type u_2} {R : Type u_6} {S : Type u_7} [Semiring R] [AddZeroClass M] [Semiring S] {f g : AddMonoidAlgebra R M →+* S} (h₁ : ∀ (r : R), f (single 0 r) = g (single 0 r)) (h_of : ∀ (m : M), f (single m 1) = g (single m 1)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 0 r, then they are equal.

theorem MonoidAlgebra.ringHom_ext' {M : Type u_2} {R : Type u_6} {S : Type u_7} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom) (h_of : (↑f).comp (of R M) = (↑g).comp (of R M)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 1 r, then they are equal.

See note [partially-applied ext lemmas].

theorem MonoidAlgebra.ringHom_ext'_iff {M : Type u_2} {R : Type u_6} {S : Type u_7} [Semiring R] [MulOneClass M] [Semiring S] {f g : MonoidAlgebra R M →+* S} : f = g ↔ f.comp singleOneRingHom = g.comp singleOneRingHom ∧ (↑f).comp (of R M) = (↑g).comp (of R M)

instance MonoidAlgebra.semiring {M : Type u_2} {R : Type u_6} [Semiring R] [Monoid M] : Semiring (MonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance AddMonoidAlgebra.semiring {M : Type u_2} {R : Type u_6} [Semiring R] [AddMonoid M] : Semiring (AddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MonoidAlgebra.single_pow {M : Type u_2} {R : Type u_6} [Semiring R] [Monoid M] (m : M) (r : R) (n : ℕ) : single m r ^ n = single (m ^ n) (r ^ n)

@[simp]

theorem AddMonoidAlgebra.single_pow {M : Type u_2} {R : Type u_6} [Semiring R] [AddMonoid M] (m : M) (r : R) (n : ℕ) : single m r ^ n = single (n • m) (r ^ n)

theorem MonoidAlgebra.induction_on {M : Type u_2} {R : Type u_6} [Semiring R] [Monoid M] {p : MonoidAlgebra R M → Prop} (x : MonoidAlgebra R M) (hM : ∀ (m : M), p ((of R M) m)) (hadd : ∀ (x y : MonoidAlgebra R M), p x → p y → p (x + y)) (hsmul : ∀ (r : R) (x : MonoidAlgebra R M), p x → p (r • x)) : p x

instance MonoidAlgebra.isLocalHom_singleOneRingHom {M : Type u_2} {R : Type u_6} [Semiring R] [Monoid M] : IsLocalHom singleOneRingHom

instance AddMonoidAlgebra.isLocalHom_singleZeroRingHom {M : Type u_2} {R : Type u_6} [Semiring R] [AddMonoid M] : IsLocalHom singleZeroRingHom

@[simp]

theorem MonoidAlgebra.mul_single_apply {G : Type u_1} {R : Type u_6} [Semiring R] [Group G] (x : MonoidAlgebra R G) (r : R) (g h : G) : (x * single g r) h = x (h * g⁻¹) * r

@[simp]

theorem AddMonoidAlgebra.mul_single_apply {G : Type u_1} {R : Type u_6} [Semiring R] [AddGroup G] (x : AddMonoidAlgebra R G) (r : R) (g h : G) : (x * single g r) h = x (h + -g) * r

@[simp]

theorem MonoidAlgebra.single_mul_apply {G : Type u_1} {R : Type u_6} [Semiring R] [Group G] (x : MonoidAlgebra R G) (r : R) (g h : G) : (single g r * x) h = r * x (g⁻¹ * h)

@[simp]

theorem AddMonoidAlgebra.single_mul_apply {G : Type u_1} {R : Type u_6} [Semiring R] [AddGroup G] (x : AddMonoidAlgebra R G) (r : R) (g h : G) : (single g r * x) h = r * x (-g + h)

theorem MonoidAlgebra.mul_apply_left {G : Type u_1} {R : Type u_6} [Semiring R] [Group G] (x y : MonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum x fun (h : G) (r : R) => r * y (h⁻¹ * g)

theorem AddMonoidAlgebra.mul_apply_left {G : Type u_1} {R : Type u_6} [Semiring R] [AddGroup G] (x y : AddMonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum x fun (h : G) (r : R) => r * y (-h + g)

theorem MonoidAlgebra.mul_apply_right {G : Type u_1} {R : Type u_6} [Semiring R] [Group G] (x y : MonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum y fun (h : G) (r : R) => x (g * h⁻¹) * r

theorem AddMonoidAlgebra.mul_apply_right {G : Type u_1} {R : Type u_6} [Semiring R] [AddGroup G] (x y : AddMonoidAlgebra R G) (g : G) : (x * y) g = Finsupp.sum y fun (h : G) (r : R) => x (g + -h) * r

instance MonoidAlgebra.nonUnitalCommSemiring {M : Type u_2} {R : Type u_6} [CommSemiring R] [CommSemigroup M] : NonUnitalCommSemiring (MonoidAlgebra R M)

Equations

• MonoidAlgebra.nonUnitalCommSemiring = { toNonUnitalSemiring := MonoidAlgebra.nonUnitalSemiring, mul_comm := ⋯ }

instance AddMonoidAlgebra.nonUnitalCommSemiring {M : Type u_2} {R : Type u_6} [CommSemiring R] [AddCommSemigroup M] : NonUnitalCommSemiring (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.nonUnitalCommSemiring = { toNonUnitalSemiring := AddMonoidAlgebra.nonUnitalSemiring, mul_comm := ⋯ }

theorem MonoidAlgebra.single_one_comm {M : Type u_2} {R : Type u_6} [CommSemiring R] [MulOneClass M] (r : R) (f : MonoidAlgebra R M) : single 1 r * f = f * single 1 r

theorem AddMonoidAlgebra.single_zero_comm {M : Type u_2} {R : Type u_6} [CommSemiring R] [AddZeroClass M] (r : R) (f : AddMonoidAlgebra R M) : single 0 r * f = f * single 0 r

instance MonoidAlgebra.commSemiring {M : Type u_2} {R : Type u_6} [CommSemiring R] [CommMonoid M] : CommSemiring (MonoidAlgebra R M)

Equations

• MonoidAlgebra.commSemiring = { toSemiring := MonoidAlgebra.semiring, mul_comm := ⋯ }

instance AddMonoidAlgebra.commSemiring {M : Type u_2} {R : Type u_6} [CommSemiring R] [AddCommMonoid M] : CommSemiring (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.commSemiring = { toSemiring := AddMonoidAlgebra.semiring, mul_comm := ⋯ }

theorem MonoidAlgebra.prod_single {M : Type u_2} {ι : Type u_5} {R : Type u_6} [CommSemiring R] [CommMonoid M] (s : Finset ι) (m : ι → M) (r : ι → R) : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)

theorem AddMonoidAlgebra.prod_single {M : Type u_2} {ι : Type u_5} {R : Type u_6} [CommSemiring R] [AddCommMonoid M] (s : Finset ι) (m : ι → M) (r : ι → R) : ∏ i ∈ s, single (m i) (r i) = single (∑ i ∈ s, m i) (∏ i ∈ s, r i)

instance MonoidAlgebra.addCommGroup {M : Type u_2} {R : Type u_6} [Ring R] : AddCommGroup (MonoidAlgebra R M)

Equations

• MonoidAlgebra.addCommGroup = inferInstanceAs (AddCommGroup (M →₀ R))

instance AddMonoidAlgebra.addAddCommGroup {M : Type u_2} {R : Type u_6} [Ring R] : AddCommGroup (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.addAddCommGroup = inferInstanceAs (AddCommGroup (M →₀ R))

@[simp]

theorem MonoidAlgebra.neg_apply {M : Type u_2} {R : Type u_6} [Ring R] (m : M) (x : MonoidAlgebra R M) : (-x) m = -x m

@[simp]

theorem AddMonoidAlgebra.neg_apply {M : Type u_2} {R : Type u_6} [Ring R] (m : M) (x : AddMonoidAlgebra R M) : (-x) m = -x m

theorem MonoidAlgebra.single_neg {M : Type u_2} {R : Type u_6} [Ring R] (m : M) (r : R) : single m (-r) = -single m r

theorem AddMonoidAlgebra.single_neg {M : Type u_2} {R : Type u_6} [Ring R] (m : M) (r : R) : single m (-r) = -single m r

instance MonoidAlgebra.nonUnitalNonAssocRing {M : Type u_2} {R : Type u_6} [Ring R] [Mul M] : NonUnitalNonAssocRing (MonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance AddMonoidAlgebra.nonUnitalNonAssocRing {M : Type u_2} {R : Type u_6} [Ring R] [Add M] : NonUnitalNonAssocRing (AddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance MonoidAlgebra.nonUnitalRing {M : Type u_2} {R : Type u_6} [Ring R] [Semigroup M] : NonUnitalRing (MonoidAlgebra R M)

Equations

• MonoidAlgebra.nonUnitalRing = { toNonUnitalNonAssocRing := MonoidAlgebra.nonUnitalNonAssocRing, mul_assoc := ⋯ }

instance AddMonoidAlgebra.nonUnitalRing {M : Type u_2} {R : Type u_6} [Ring R] [AddSemigroup M] : NonUnitalRing (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.nonUnitalRing = { toNonUnitalNonAssocRing := AddMonoidAlgebra.nonUnitalNonAssocRing, mul_assoc := ⋯ }

instance MonoidAlgebra.nonAssocRing {M : Type u_2} {R : Type u_6} [Ring R] [MulOneClass M] : NonAssocRing (MonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance AddMonoidAlgebra.nonAssocRing {M : Type u_2} {R : Type u_6} [Ring R] [AddZeroClass M] : NonAssocRing (AddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

theorem MonoidAlgebra.intCast_def {M : Type u_2} {R : Type u_6} [Ring R] [MulOneClass M] (z : ℤ) : ↑z = single 1 ↑z

theorem AddMonoidAlgebra.intCast_def {M : Type u_2} {R : Type u_6} [Ring R] [AddZeroClass M] (z : ℤ) : ↑z = single 0 ↑z

instance MonoidAlgebra.ring {M : Type u_2} {R : Type u_6} [Ring R] [Monoid M] : Ring (MonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance AddMonoidAlgebra.ring {M : Type u_2} {R : Type u_6} [Ring R] [AddMonoid M] : Ring (AddMonoidAlgebra R M)

Equations

• One or more equations did not get rendered due to their size.

instance MonoidAlgebra.nonUnitalCommRing {M : Type u_2} {R : Type u_6} [CommRing R] [CommSemigroup M] : NonUnitalCommRing (MonoidAlgebra R M)

Equations

• MonoidAlgebra.nonUnitalCommRing = { toNonUnitalRing := MonoidAlgebra.nonUnitalRing, mul_comm := ⋯ }

instance AddMonoidAlgebra.nonUnitalCommRing {M : Type u_2} {R : Type u_6} [CommRing R] [AddCommSemigroup M] : NonUnitalCommRing (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.nonUnitalCommRing = { toNonUnitalRing := AddMonoidAlgebra.nonUnitalRing, mul_comm := ⋯ }

instance MonoidAlgebra.commRing {M : Type u_2} {R : Type u_6} [CommRing R] [CommMonoid M] : CommRing (MonoidAlgebra R M)

Equations

• MonoidAlgebra.commRing = { toRing := MonoidAlgebra.ring, mul_comm := ⋯ }

instance AddMonoidAlgebra.commRing {M : Type u_2} {R : Type u_6} [CommRing R] [AddCommMonoid M] : CommRing (AddMonoidAlgebra R M)

Equations

• AddMonoidAlgebra.commRing = { toRing := AddMonoidAlgebra.ring, mul_comm := ⋯ }

Additive monoids

def AddMonoidAlgebra.ofMagma (R : Type u_8) (M : Type u_9) [Semiring R] [Add M] : Multiplicative M →ₙ* AddMonoidAlgebra R M

The embedding of an additive magma into its additive magma algebra.

Equations

• AddMonoidAlgebra.ofMagma R M = { toFun := fun (a : Multiplicative M) => AddMonoidAlgebra.single a 1, map_mul' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.ofMagma_apply (R : Type u_8) (M : Type u_9) [Semiring R] [Add M] (a : Multiplicative M) : (ofMagma R M) a = single a 1

def AddMonoidAlgebra.of (R : Type u_8) (M : Type u_9) [Semiring R] [AddZeroClass M] : Multiplicative M →* AddMonoidAlgebra R M

Embedding of a magma with zero into its magma algebra.

Equations

• AddMonoidAlgebra.of R M = { toFun := fun (a : Multiplicative M) => AddMonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidAlgebra.of' (R : Type u_8) (M : Type u_9) [Semiring R] : M → AddMonoidAlgebra R M

Embedding of a magma with zero M, into its magma algebra, having M as source.

Equations

• AddMonoidAlgebra.of' R M m = AddMonoidAlgebra.single m 1

@[simp]

theorem AddMonoidAlgebra.of_apply {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (a : Multiplicative M) : (of R M) a = single (Multiplicative.toAdd a) 1

@[simp]

theorem AddMonoidAlgebra.of'_apply {M : Type u_2} {R : Type u_6} [Semiring R] (a : M) : of' R M a = single a 1

theorem AddMonoidAlgebra.of'_eq_of {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (a : M) : of' R M a = (of R M) (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.of_injective {M : Type u_2} {R : Type u_6} [Semiring R] [Nontrivial R] [AddZeroClass M] : Function.Injective ⇑(of R M)

theorem AddMonoidAlgebra.of'_commute {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] {a : M} (h : ∀ (a' : M), AddCommute a a') (f : AddMonoidAlgebra R M) : Commute (of' R M a) f

def AddMonoidAlgebra.singleHom {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] : R × Multiplicative M →* AddMonoidAlgebra R M

Finsupp.single as a MonoidHom from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of Finsupp.single.

Equations

• AddMonoidAlgebra.singleHom = { toFun := fun (a : R × Multiplicative M) => AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.singleHom_apply {M : Type u_2} {R : Type u_6} [Semiring R] [AddZeroClass M] (a : R × Multiplicative M) : singleHom a = single (Multiplicative.toAdd a.2) a.1

theorem AddMonoidAlgebra.induction_on {M : Type u_2} {R : Type u_6} [Semiring R] [AddMonoid M] {p : AddMonoidAlgebra R M → Prop} (x : AddMonoidAlgebra R M) (hM : ∀ (m : M), p ((of R M) (Multiplicative.ofAdd m))) (hadd : ∀ (x y : AddMonoidAlgebra R M), p x → p y → p (x + y)) (hsmul : ∀ (r : R) (x : AddMonoidAlgebra R M), p x → p (r • x)) : p x

Algebra structure

theorem AddMonoidAlgebra.ringHom_ext' {M : Type u_2} {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] [AddMonoid M] {f g : AddMonoidAlgebra R M →+* S} (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom) (h_of : (↑f).comp (of R M) = (↑g).comp (of R M)) : f = g

If two ring homomorphisms from R[M] are equal on all single m 1 and single 0 r, then they are equal.

See note [partially-applied ext lemmas].

theorem AddMonoidAlgebra.ringHom_ext'_iff {M : Type u_2} {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] [AddMonoid M] {f g : AddMonoidAlgebra R M →+* S} : f = g ↔ f.comp singleZeroRingHom = g.comp singleZeroRingHom ∧ (↑f).comp (of R M) = (↑g).comp (of R M)