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 the monoid.
The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.
In fact the construction of the "monoid algebra" makes sense when G is not even a monoid, but
merely a magma, i.e., when G 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 k G := G →₀ k, and AddMonoidAlgebra k G
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 (σ →₀ ℕ)
When the domain is multiplicative, e.g. a group, this will be used to define the group ring.
Notation #
We introduce the notation R[A] for AddMonoidAlgebra R A.
Implementation note #
Unfortunately because additive and multiplicative structures both appear in both cases,
it doesn't appear to be possible to make much use of to_additive, and we just settle for
saying everything twice.
Similarly, I attempted to just define
k[G] := MonoidAlgebra k (Multiplicative G), but the definitional equality
Multiplicative G = G leaks through everywhere, and seems impossible to use.
Multiplicative monoids #
The monoid algebra over a semiring k generated by the monoid G.
It is the type of finite formal k-linear combinations of terms of G,
endowed with the convolution product.
Equations
- MonoidAlgebra k G = (G →₀ k)
instance
MonoidAlgebra.inhabited
(k : Type u₁)
(G : Type u₂)
[Semiring k]
:
Inhabited (MonoidAlgebra k G)
Equations
- MonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))
instance
MonoidAlgebra.addCommMonoid
(k : Type u₁)
(G : Type u₂)
[Semiring k]
:
AddCommMonoid (MonoidAlgebra k G)
Equations
- MonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))
instance
MonoidAlgebra.instIsCancelAdd
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[IsCancelAdd k]
:
IsCancelAdd (MonoidAlgebra k G)
instance
MonoidAlgebra.coeFun
(k : Type u₁)
(G : Type u₂)
[Semiring k]
:
CoeFun (MonoidAlgebra k G) fun (x : MonoidAlgebra k G) => G → k
Equations
- MonoidAlgebra.coeFun k G = inferInstanceAs (CoeFun (G →₀ k) fun (x : G →₀ k) => G → k)
@[reducible, inline]
abbrev
MonoidAlgebra.single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
(b : k)
:
MonoidAlgebra k G
Equations
- MonoidAlgebra.single a b = Finsupp.single a b
theorem
MonoidAlgebra.single_zero
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
:
MonoidAlgebra.single a 0 = 0
theorem
MonoidAlgebra.single_add
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
(b₁ b₂ : k)
:
MonoidAlgebra.single a (b₁ + b₂) = MonoidAlgebra.single a b₁ + MonoidAlgebra.single a b₂
@[simp]
theorem
MonoidAlgebra.sum_single_index
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{N : Type u_3}
[AddCommMonoid N]
{a : G}
{b : k}
{h : G → k → N}
(h_zero : h a 0 = 0)
:
Finsupp.sum (MonoidAlgebra.single a b) h = h a b
@[simp]
theorem
MonoidAlgebra.single_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{a a' : G}
{b : k}
[Decidable (a = a')]
:
(MonoidAlgebra.single a b) a' = if a = a' then b else 0
@[simp]
theorem
MonoidAlgebra.single_eq_zero
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{a : G}
{b : k}
:
MonoidAlgebra.single a b = 0 ↔ b = 0
@[reducible, inline]
abbrev
MonoidAlgebra.mapDomain
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{G' : Type u_3}
(f : G → G')
(v : MonoidAlgebra k G)
:
MonoidAlgebra k G'
Equations
theorem
MonoidAlgebra.mapDomain_sum
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{k' : Type u_3}
{G' : Type u_4}
[Semiring k']
{f : G → G'}
{s : MonoidAlgebra k' G}
{v : G → k' → MonoidAlgebra k G}
:
MonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : G) (b : k') => MonoidAlgebra.mapDomain f (v a b)
def
MonoidAlgebra.liftNC
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[NonUnitalNonAssocSemiring R]
(f : k →+ R)
(g : 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
MonoidAlgebra 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.
Equations
- MonoidAlgebra.liftNC f g = Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g x)).comp f
@[simp]
theorem
MonoidAlgebra.liftNC_single
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[NonUnitalNonAssocSemiring R]
(f : k →+ R)
(g : G → R)
(a : G)
(b : k)
:
(MonoidAlgebra.liftNC f g) (MonoidAlgebra.single a b) = f b * g a
@[irreducible]
def
MonoidAlgebra.mul'
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
(f g : MonoidAlgebra k G)
:
MonoidAlgebra k G
The multiplication in a monoid algebra. We make it irreducible so that Lean doesn't unfold it trying to unify two things that are different.
Equations
- f.mul' g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
instance
MonoidAlgebra.instMul
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
:
Mul (MonoidAlgebra k G)
The product of f g : MonoidAlgebra 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 group ring of a group.)
Equations
- MonoidAlgebra.instMul = { mul := MonoidAlgebra.mul' }
theorem
MonoidAlgebra.mul_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
{f g : MonoidAlgebra k G}
:
f * g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
Equations
theorem
MonoidAlgebra.liftNC_mul
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[Mul G]
[Semiring R]
{g_hom : Type u_3}
[FunLike g_hom G R]
[MulHomClass g_hom G R]
(f : k →+* R)
(g : g_hom)
(a b : MonoidAlgebra k G)
(h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y))
:
(MonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (MonoidAlgebra.liftNC ↑f ⇑g) a * (MonoidAlgebra.liftNC ↑f ⇑g) b
Equations
instance
MonoidAlgebra.one
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[One G]
:
One (MonoidAlgebra k G)
The unit of the multiplication is single 1 1, i.e. the function
that is 1 at 1 and zero elsewhere.
Equations
- MonoidAlgebra.one = { one := MonoidAlgebra.single 1 1 }
theorem
MonoidAlgebra.one_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[One G]
:
1 = MonoidAlgebra.single 1 1
@[simp]
theorem
MonoidAlgebra.liftNC_one
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[NonAssocSemiring R]
[Semiring k]
[One G]
{g_hom : Type u_3}
[FunLike g_hom G R]
[OneHomClass g_hom G R]
(f : k →+* R)
(g : g_hom)
:
(MonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
Equations
theorem
MonoidAlgebra.natCast_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(n : ℕ)
:
↑n = MonoidAlgebra.single 1 ↑n
@[deprecated MonoidAlgebra.natCast_def (since := "2024-04-17")]
theorem
MonoidAlgebra.nat_cast_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(n : ℕ)
:
↑n = MonoidAlgebra.single 1 ↑n
Alias of MonoidAlgebra.natCast_def.
Semiring structure #
instance
MonoidAlgebra.semiring
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Monoid G]
:
Semiring (MonoidAlgebra k G)
Equations
- MonoidAlgebra.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯
def
MonoidAlgebra.liftNCRingHom
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[Monoid G]
[Semiring R]
(f : k →+* R)
(g : G →* R)
(h_comm : ∀ (x : k) (y : G), Commute (f x) (g y))
:
MonoidAlgebra k G →+* R
liftNC as a RingHom, for when f x and g y commute
Equations
- MonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(MonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
instance
MonoidAlgebra.nonUnitalCommSemiring
{k : Type u₁}
{G : Type u₂}
[CommSemiring k]
[CommSemigroup G]
:
instance
MonoidAlgebra.nontrivial
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Nontrivial k]
[Nonempty G]
:
Nontrivial (MonoidAlgebra k G)
Derived instances #
instance
MonoidAlgebra.commSemiring
{k : Type u₁}
{G : Type u₂}
[CommSemiring k]
[CommMonoid G]
:
CommSemiring (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.unique
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Subsingleton k]
:
Unique (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.addCommGroup
{k : Type u₁}
{G : Type u₂}
[Ring k]
:
AddCommGroup (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.nonUnitalRing
{k : Type u₁}
{G : Type u₂}
[Ring k]
[Semigroup G]
:
NonUnitalRing (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.nonAssocRing
{k : Type u₁}
{G : Type u₂}
[Ring k]
[MulOneClass G]
:
NonAssocRing (MonoidAlgebra k G)
Equations
- MonoidAlgebra.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
MonoidAlgebra.intCast_def
{k : Type u₁}
{G : Type u₂}
[Ring k]
[MulOneClass G]
(z : ℤ)
:
↑z = MonoidAlgebra.single 1 ↑z
@[deprecated MonoidAlgebra.intCast_def (since := "2024-04-17")]
theorem
MonoidAlgebra.int_cast_def
{k : Type u₁}
{G : Type u₂}
[Ring k]
[MulOneClass G]
(z : ℤ)
:
↑z = MonoidAlgebra.single 1 ↑z
Alias of MonoidAlgebra.intCast_def.
instance
MonoidAlgebra.ring
{k : Type u₁}
{G : Type u₂}
[Ring k]
[Monoid G]
:
Ring (MonoidAlgebra k G)
Equations
- MonoidAlgebra.ring = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
MonoidAlgebra.nonUnitalCommRing
{k : Type u₁}
{G : Type u₂}
[CommRing k]
[CommSemigroup G]
:
Equations
instance
MonoidAlgebra.commRing
{k : Type u₁}
{G : Type u₂}
[CommRing k]
[CommMonoid G]
:
CommRing (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.smulZeroClass
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[SMulZeroClass R k]
:
SMulZeroClass R (MonoidAlgebra k G)
instance
MonoidAlgebra.noZeroSMulDivisors
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Zero R]
[Semiring k]
[SMulZeroClass R k]
[NoZeroSMulDivisors R k]
:
NoZeroSMulDivisors R (MonoidAlgebra k G)
instance
MonoidAlgebra.distribSMul
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
:
DistribSMul R (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.distribMulAction
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Monoid R]
[Semiring k]
[DistribMulAction R k]
:
DistribMulAction R (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.module
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring R]
[Semiring k]
[Module R k]
:
Module R (MonoidAlgebra k G)
Equations
instance
MonoidAlgebra.faithfulSMul
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[SMulZeroClass R k]
[FaithfulSMul R k]
[Nonempty G]
:
FaithfulSMul R (MonoidAlgebra k G)
instance
MonoidAlgebra.isScalarTower
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{S : Type u_3}
[Semiring k]
[SMulZeroClass R k]
[SMulZeroClass S k]
[SMul R S]
[IsScalarTower R S k]
:
IsScalarTower R S (MonoidAlgebra k G)
instance
MonoidAlgebra.smulCommClass
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{S : Type u_3}
[Semiring k]
[SMulZeroClass R k]
[SMulZeroClass S k]
[SMulCommClass R S k]
:
SMulCommClass R S (MonoidAlgebra k G)
instance
MonoidAlgebra.isCentralScalar
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[SMulZeroClass R k]
[SMulZeroClass Rᵐᵒᵖ k]
[IsCentralScalar R k]
:
IsCentralScalar R (MonoidAlgebra k G)
def
MonoidAlgebra.comapDistribMulActionSelf
{k : Type u₁}
{G : Type u₂}
[Group G]
[Semiring k]
:
DistribMulAction G (MonoidAlgebra k G)
This is not an instance as it conflicts with MonoidAlgebra.distribMulAction when G = kˣ.
Copies of ext lemmas and bundled singles from Finsupp #
As MonoidAlgebra is a type synonym, ext will not unfold it to find ext lemmas.
We need bundled version of Finsupp.single with the right types to state these lemmas.
It is good practice to have those, regardless of the ext issue.
theorem
MonoidAlgebra.ext
{k : Type u₁}
{G : Type u₂}
[Semiring k]
⦃f g : MonoidAlgebra k G⦄
(H : ∀ (x : G), f x = g x)
:
f = g
A copy of Finsupp.ext for MonoidAlgebra.
@[reducible, inline]
abbrev
MonoidAlgebra.singleAddHom
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
:
k →+ MonoidAlgebra k G
A copy of Finsupp.singleAddHom for MonoidAlgebra.
Equations
@[simp]
theorem
MonoidAlgebra.singleAddHom_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
(b : k)
:
(MonoidAlgebra.singleAddHom a) b = MonoidAlgebra.single a b
theorem
MonoidAlgebra.addHom_ext'
{k : Type u₁}
{G : Type u₂}
{N : Type u_3}
[Semiring k]
[AddZeroClass N]
⦃f g : MonoidAlgebra k G →+ N⦄
(H : ∀ (x : G), f.comp (MonoidAlgebra.singleAddHom x) = g.comp (MonoidAlgebra.singleAddHom x))
:
f = g
A copy of Finsupp.addHom_ext' for MonoidAlgebra.
theorem
MonoidAlgebra.distribMulActionHom_ext'
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{N : Type u_3}
[Monoid R]
[Semiring k]
[AddMonoid N]
[DistribMulAction R N]
[DistribMulAction R k]
{f g : MonoidAlgebra k G →+[R] N}
(h : ∀ (a : G), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a))
:
f = g
A copy of Finsupp.distribMulActionHom_ext' for MonoidAlgebra.
@[reducible, inline]
abbrev
MonoidAlgebra.lsingle
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring R]
[Semiring k]
[Module R k]
(a : G)
:
k →ₗ[R] MonoidAlgebra k G
A copy of Finsupp.lsingle for MonoidAlgebra.
Equations
@[simp]
theorem
MonoidAlgebra.lsingle_apply
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring R]
[Semiring k]
[Module R k]
(a : G)
(b : k)
:
(MonoidAlgebra.lsingle a) b = MonoidAlgebra.single a b
theorem
MonoidAlgebra.lhom_ext'
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{N : Type u_3}
[Semiring R]
[Semiring k]
[AddCommMonoid N]
[Module R N]
[Module R k]
⦃f g : MonoidAlgebra k G →ₗ[R] N⦄
(H : ∀ (x : G), f ∘ₗ MonoidAlgebra.lsingle x = g ∘ₗ MonoidAlgebra.lsingle x)
:
f = g
A copy of Finsupp.lhom_ext' for MonoidAlgebra.
theorem
MonoidAlgebra.mul_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[DecidableEq G]
[Mul G]
(f g : MonoidAlgebra k G)
(x : G)
:
(f * g) x = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => if a₁ * a₂ = x then b₁ * b₂ else 0
@[simp]
theorem
MonoidAlgebra.single_mul_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
{a₁ a₂ : G}
{b₁ b₂ : k}
:
MonoidAlgebra.single a₁ b₁ * MonoidAlgebra.single a₂ b₂ = MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
theorem
MonoidAlgebra.single_commute_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
{a₁ a₂ : G}
{b₁ b₂ : k}
(ha : Commute a₁ a₂)
(hb : Commute b₁ b₂)
:
Commute (MonoidAlgebra.single a₁ b₁) (MonoidAlgebra.single a₂ b₂)
theorem
MonoidAlgebra.single_commute
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
{a : G}
{b : k}
(ha : ∀ (a' : G), Commute a a')
(hb : ∀ (b' : k), Commute b b')
(f : MonoidAlgebra k G)
:
Commute (MonoidAlgebra.single a b) f
@[simp]
theorem
MonoidAlgebra.single_pow
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Monoid G]
{a : G}
{b : k}
(n : ℕ)
:
MonoidAlgebra.single a b ^ n = MonoidAlgebra.single (a ^ n) (b ^ n)
@[simp]
theorem
MonoidAlgebra.mapDomain_one
{α : Type u_3}
{β : Type u_4}
{α₂ : Type u_5}
[Semiring β]
[One α]
[One α₂]
{F : Type u_6}
[FunLike F α α₂]
[OneHomClass F α α₂]
(f : F)
:
MonoidAlgebra.mapDomain (⇑f) 1 = 1
Like Finsupp.mapDomain_zero, but for the 1 we define in this file
theorem
MonoidAlgebra.mapDomain_mul
{α : Type u_3}
{β : Type u_4}
{α₂ : Type u_5}
[Semiring β]
[Mul α]
[Mul α₂]
{F : Type u_6}
[FunLike F α α₂]
[MulHomClass F α α₂]
(f : F)
(x y : MonoidAlgebra β α)
:
MonoidAlgebra.mapDomain (⇑f) (x * y) = MonoidAlgebra.mapDomain (⇑f) x * MonoidAlgebra.mapDomain (⇑f) y
Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file
The embedding of a magma into its magma algebra.
Equations
- MonoidAlgebra.ofMagma k G = { toFun := fun (a : G) => MonoidAlgebra.single a 1, map_mul' := ⋯ }
@[simp]
theorem
MonoidAlgebra.ofMagma_apply
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[Mul G]
(a : G)
:
(MonoidAlgebra.ofMagma k G) a = MonoidAlgebra.single a 1
def
MonoidAlgebra.of
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[MulOneClass G]
:
G →* MonoidAlgebra k G
The embedding of a unital magma into its magma algebra.
Equations
- MonoidAlgebra.of k G = { toFun := fun (a : G) => MonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }
@[simp]
theorem
MonoidAlgebra.of_apply
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[MulOneClass G]
(a : G)
:
(MonoidAlgebra.of k G) a = MonoidAlgebra.single a 1
@[simp]
theorem
MonoidAlgebra.smul_single'
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(c : k)
(a : G)
(b : k)
:
c • MonoidAlgebra.single a b = MonoidAlgebra.single a (c * b)
Copy of Finsupp.smul_single' that avoids the MonoidAlgebra = Finsupp defeq abuse.
theorem
MonoidAlgebra.smul_of
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(g : G)
(r : k)
:
r • (MonoidAlgebra.of k G) g = MonoidAlgebra.single g r
theorem
MonoidAlgebra.of_injective
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
[Nontrivial k]
:
theorem
MonoidAlgebra.of_commute
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
{a : G}
(h : ∀ (a' : G), Commute a a')
(f : MonoidAlgebra k G)
:
Commute ((MonoidAlgebra.of k G) a) f
def
MonoidAlgebra.singleHom
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
:
k × G →* MonoidAlgebra k G
Finsupp.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
Finsupp.single.
Equations
- MonoidAlgebra.singleHom = { toFun := fun (a : k × G) => MonoidAlgebra.single a.2 a.1, map_one' := ⋯, map_mul' := ⋯ }
@[simp]
theorem
MonoidAlgebra.singleHom_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(a : k × G)
:
MonoidAlgebra.singleHom a = MonoidAlgebra.single a.2 a.1
theorem
MonoidAlgebra.mul_single_apply_aux
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
(f : MonoidAlgebra k G)
{r : k}
{x y z : G}
(H : ∀ (a : G), a * x = z ↔ a = y)
:
(f * MonoidAlgebra.single x r) z = f y * r
theorem
MonoidAlgebra.mul_single_one_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(f : MonoidAlgebra k G)
(r : k)
(x : G)
:
(f * MonoidAlgebra.single 1 r) x = f x * r
theorem
MonoidAlgebra.mul_single_apply_of_not_exists_mul
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
(r : k)
{g g' : G}
(x : MonoidAlgebra k G)
(h : ¬∃ (d : G), g' = d * g)
:
(x * MonoidAlgebra.single g r) g' = 0
theorem
MonoidAlgebra.single_mul_apply_aux
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
(f : MonoidAlgebra k G)
{r : k}
{x y z : G}
(H : ∀ (a : G), x * a = y ↔ a = z)
:
(MonoidAlgebra.single x r * f) y = r * f z
theorem
MonoidAlgebra.single_one_mul_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(f : MonoidAlgebra k G)
(r : k)
(x : G)
:
(MonoidAlgebra.single 1 r * f) x = r * f x
theorem
MonoidAlgebra.single_mul_apply_of_not_exists_mul
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Mul G]
(r : k)
{g g' : G}
(x : MonoidAlgebra k G)
(h : ¬∃ (d : G), g' = g * d)
:
(MonoidAlgebra.single g r * x) g' = 0
theorem
MonoidAlgebra.liftNC_smul
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
{R : Type u_3}
[Semiring R]
(f : k →+* R)
(g : G →* R)
(c : k)
(φ : MonoidAlgebra k G)
:
(MonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (MonoidAlgebra.liftNC ↑f ⇑g) φ
Non-unital, non-associative algebra structure #
instance
MonoidAlgebra.isScalarTower_self
(k : Type u₁)
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
[Mul G]
[IsScalarTower R k k]
:
IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G)
instance
MonoidAlgebra.smulCommClass_self
(k : Type u₁)
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
[Mul G]
[SMulCommClass R k k]
:
SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G)
Note that if k is a CommSemiring then we have SMulCommClass k k k and so we can take
R = k in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication.
instance
MonoidAlgebra.smulCommClass_symm_self
(k : Type u₁)
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
[Mul G]
[SMulCommClass k R k]
:
SMulCommClass (MonoidAlgebra k G) R (MonoidAlgebra k G)
theorem
MonoidAlgebra.single_one_comm
{k : Type u₁}
{G : Type u₂}
[CommSemiring k]
[MulOneClass G]
(r : k)
(f : MonoidAlgebra k G)
:
MonoidAlgebra.single 1 r * f = f * MonoidAlgebra.single 1 r
def
MonoidAlgebra.singleOneRingHom
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
:
k →+* MonoidAlgebra k G
Finsupp.single 1 as a RingHom
Equations
- MonoidAlgebra.singleOneRingHom = { toFun := (↑(Finsupp.singleAddHom 1)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
MonoidAlgebra.singleOneRingHom_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[MulOneClass G]
(a✝ : k)
:
MonoidAlgebra.singleOneRingHom a✝ = (↑(Finsupp.singleAddHom 1)).toFun a✝
def
MonoidAlgebra.mapDomainRingHom
{G : Type u₂}
(k : Type u_3)
{H : Type u_4}
{F : Type u_5}
[Semiring k]
[Monoid G]
[Monoid H]
[FunLike F G H]
[MonoidHomClass F G H]
(f : F)
:
MonoidAlgebra k G →+* MonoidAlgebra k H
If f : G → H is a multiplicative homomorphism between two monoids, then
Finsupp.mapDomain f is a ring homomorphism between their monoid algebras.
Equations
- MonoidAlgebra.mapDomainRingHom k f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
MonoidAlgebra.mapDomainRingHom_apply
{G : Type u₂}
(k : Type u_3)
{H : Type u_4}
{F : Type u_5}
[Semiring k]
[Monoid G]
[Monoid H]
[FunLike F G H]
[MonoidHomClass F G H]
(f : F)
(a✝ : G →₀ k)
:
(MonoidAlgebra.mapDomainRingHom k f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝
theorem
MonoidAlgebra.ringHom_ext
{k : Type u₁}
{G : Type u₂}
{R : Type u_3}
[Semiring k]
[MulOneClass G]
[Semiring R]
{f g : MonoidAlgebra k G →+* R}
(h₁ : ∀ (b : k), f (MonoidAlgebra.single 1 b) = g (MonoidAlgebra.single 1 b))
(h_of : ∀ (a : G), f (MonoidAlgebra.single a 1) = g (MonoidAlgebra.single a 1))
:
f = g
If two ring homomorphisms from MonoidAlgebra k G are equal on all single a 1
and single 1 b, then they are equal.
theorem
MonoidAlgebra.ringHom_ext'
{k : Type u₁}
{G : Type u₂}
{R : Type u_3}
[Semiring k]
[MulOneClass G]
[Semiring R]
{f g : MonoidAlgebra k G →+* R}
(h₁ : f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom)
(h_of : (↑f).comp (MonoidAlgebra.of k G) = (↑g).comp (MonoidAlgebra.of k G))
:
f = g
If two ring homomorphisms from MonoidAlgebra k G are equal on all single a 1
and single 1 b, then they are equal.
See note [partially-applied ext lemmas].
theorem
MonoidAlgebra.induction_on
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Monoid G]
{p : MonoidAlgebra k G → Prop}
(f : MonoidAlgebra k G)
(hM : ∀ (g : G), p ((MonoidAlgebra.of k G) g))
(hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g))
(hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f))
:
p f
theorem
MonoidAlgebra.prod_single
{k : Type u₁}
{G : Type u₂}
{ι : Type ui}
[CommSemiring k]
[CommMonoid G]
{s : Finset ι}
{a : ι → G}
{b : ι → k}
:
∏ i ∈ s, MonoidAlgebra.single (a i) (b i) = MonoidAlgebra.single (∏ i ∈ s, a i) (∏ i ∈ s, b i)
@[simp]
theorem
MonoidAlgebra.mul_single_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Group G]
(f : MonoidAlgebra k G)
(r : k)
(x y : G)
:
@[simp]
theorem
MonoidAlgebra.single_mul_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Group G]
(r : k)
(x : G)
(f : MonoidAlgebra k G)
(y : G)
:
theorem
MonoidAlgebra.mul_apply_left
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Group G]
(f g : MonoidAlgebra k G)
(x : G)
:
theorem
MonoidAlgebra.mul_apply_right
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Group G]
(f g : MonoidAlgebra k G)
(x : G)
:
noncomputable def
MonoidAlgebra.opRingEquiv
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Monoid G]
:
(MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ
The opposite of a MonoidAlgebra R I equivalent as a ring to
the MonoidAlgebra Rᵐᵒᵖ Iᵐᵒᵖ over the opposite ring, taking elements to their opposite.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
MonoidAlgebra.opRingEquiv_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Monoid G]
(a✝ : (G →₀ k)ᵐᵒᵖ)
:
MonoidAlgebra.opRingEquiv a✝ = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝))
theorem
MonoidAlgebra.opRingEquiv_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Monoid G]
(r : k)
(x : G)
:
MonoidAlgebra.opRingEquiv (MulOpposite.op (MonoidAlgebra.single x r)) = MonoidAlgebra.single (MulOpposite.op x) (MulOpposite.op r)
def
MonoidAlgebra.submoduleOfSMulMem
{k : Type u₁}
{G : Type u₂}
[CommSemiring k]
[Monoid G]
{V : Type u_3}
[AddCommMonoid V]
[Module k V]
[Module (MonoidAlgebra k G) V]
[IsScalarTower k (MonoidAlgebra k G) V]
(W : Submodule k V)
(h : ∀ (g : G), ∀ v ∈ W, (MonoidAlgebra.of k G) g • v ∈ W)
:
Submodule (MonoidAlgebra k G) V
A submodule over k which is stable under scalar multiplication by elements of G is a
submodule over MonoidAlgebra k G
Equations
- MonoidAlgebra.submoduleOfSMulMem W h = { carrier := ↑W, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Additive monoids #
The monoid algebra over a semiring k generated by the additive monoid G.
It is the type of finite formal k-linear combinations of terms of G,
endowed with the convolution product.
Equations
- AddMonoidAlgebra k G = (G →₀ k)
The monoid algebra over a semiring k generated by the additive monoid G.
It is the type of finite formal k-linear combinations of terms of G,
endowed with the convolution product.
Equations
- One or more equations did not get rendered due to their size.
instance
AddMonoidAlgebra.inhabited
(k : Type u₁)
(G : Type u₂)
[Semiring k]
:
Inhabited (AddMonoidAlgebra k G)
Equations
- AddMonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))
Equations
- AddMonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))
instance
AddMonoidAlgebra.instIsCancelAdd
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[IsCancelAdd k]
:
IsCancelAdd (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.coeFun
(k : Type u₁)
(G : Type u₂)
[Semiring k]
:
CoeFun (AddMonoidAlgebra k G) fun (x : AddMonoidAlgebra k G) => G → k
Equations
- AddMonoidAlgebra.coeFun k G = inferInstanceAs (CoeFun (G →₀ k) fun (x : G →₀ k) => G → k)
@[reducible, inline]
abbrev
AddMonoidAlgebra.single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
(b : k)
:
AddMonoidAlgebra k G
Equations
- AddMonoidAlgebra.single a b = Finsupp.single a b
theorem
AddMonoidAlgebra.single_zero
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
:
AddMonoidAlgebra.single a 0 = 0
theorem
AddMonoidAlgebra.single_add
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
(b₁ b₂ : k)
:
AddMonoidAlgebra.single a (b₁ + b₂) = AddMonoidAlgebra.single a b₁ + AddMonoidAlgebra.single a b₂
@[simp]
theorem
AddMonoidAlgebra.sum_single_index
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{N : Type u_3}
[AddCommMonoid N]
{a : G}
{b : k}
{h : G → k → N}
(h_zero : h a 0 = 0)
:
Finsupp.sum (AddMonoidAlgebra.single a b) h = h a b
@[simp]
theorem
AddMonoidAlgebra.sum_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(f : AddMonoidAlgebra k G)
:
theorem
AddMonoidAlgebra.single_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{a a' : G}
{b : k}
[Decidable (a = a')]
:
(AddMonoidAlgebra.single a b) a' = if a = a' then b else 0
@[simp]
theorem
AddMonoidAlgebra.single_eq_zero
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{a : G}
{b : k}
:
AddMonoidAlgebra.single a b = 0 ↔ b = 0
@[reducible, inline]
abbrev
AddMonoidAlgebra.mapDomain
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{G' : Type u_3}
(f : G → G')
(v : AddMonoidAlgebra k G)
:
AddMonoidAlgebra k G'
Equations
theorem
AddMonoidAlgebra.mapDomain_sum
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{k' : Type u_3}
{G' : Type u_4}
[Semiring k']
{f : G → G'}
{s : AddMonoidAlgebra k' G}
{v : G → k' → AddMonoidAlgebra k G}
:
AddMonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : G) (b : k') => AddMonoidAlgebra.mapDomain f (v a b)
theorem
AddMonoidAlgebra.mapDomain_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{G' : Type u_3}
{f : G → G'}
{a : G}
{b : k}
:
AddMonoidAlgebra.mapDomain f (AddMonoidAlgebra.single a b) = AddMonoidAlgebra.single (f a) b
def
AddMonoidAlgebra.liftNC
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[NonUnitalNonAssocSemiring R]
(f : k →+ R)
(g : 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.
Equations
- AddMonoidAlgebra.liftNC f g = Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g (Multiplicative.ofAdd x))).comp f
@[simp]
theorem
AddMonoidAlgebra.liftNC_single
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[NonUnitalNonAssocSemiring R]
(f : k →+ R)
(g : Multiplicative G → R)
(a : G)
(b : k)
:
(AddMonoidAlgebra.liftNC f g) (AddMonoidAlgebra.single a b) = f b * g (Multiplicative.ofAdd a)
instance
AddMonoidAlgebra.hasMul
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
:
Mul (AddMonoidAlgebra k G)
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.hasMul = { mul := fun (f g : AddMonoidAlgebra k G) => MonoidAlgebra.mul' f g }
theorem
AddMonoidAlgebra.mul_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
{f g : AddMonoidAlgebra k G}
:
f * g = Finsupp.sum f fun (a₁ : G) (b₁ : k) =>
Finsupp.sum g fun (a₂ : G) (b₂ : k) => AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
instance
AddMonoidAlgebra.nonUnitalNonAssocSemiring
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
:
Equations
theorem
AddMonoidAlgebra.liftNC_mul
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[Add G]
[Semiring R]
{g_hom : Type u_3}
[FunLike g_hom (Multiplicative G) R]
[MulHomClass g_hom (Multiplicative G) R]
(f : k →+* R)
(g : g_hom)
(a b : AddMonoidAlgebra k G)
(h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g (Multiplicative.ofAdd y)))
:
(AddMonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (AddMonoidAlgebra.liftNC ↑f ⇑g) a * (AddMonoidAlgebra.liftNC ↑f ⇑g) b
instance
AddMonoidAlgebra.one
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Zero G]
:
One (AddMonoidAlgebra k G)
The unit of the multiplication is single 0 1, i.e. the function
that is 1 at 0 and zero elsewhere.
Equations
- AddMonoidAlgebra.one = { one := AddMonoidAlgebra.single 0 1 }
theorem
AddMonoidAlgebra.one_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Zero G]
:
1 = AddMonoidAlgebra.single 0 1
@[simp]
theorem
AddMonoidAlgebra.liftNC_one
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[Zero G]
[NonAssocSemiring R]
{g_hom : Type u_3}
[FunLike g_hom (Multiplicative G) R]
[OneHomClass g_hom (Multiplicative G) R]
(f : k →+* R)
(g : g_hom)
:
(AddMonoidAlgebra.liftNC ↑f ⇑g) 1 = 1
instance
AddMonoidAlgebra.nonUnitalSemiring
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddSemigroup G]
:
instance
AddMonoidAlgebra.nonAssocSemiring
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
:
Equations
theorem
AddMonoidAlgebra.natCast_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(n : ℕ)
:
↑n = AddMonoidAlgebra.single 0 ↑n
@[deprecated AddMonoidAlgebra.natCast_def (since := "2024-04-17")]
theorem
AddMonoidAlgebra.nat_cast_def
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(n : ℕ)
:
↑n = AddMonoidAlgebra.single 0 ↑n
Alias of AddMonoidAlgebra.natCast_def.
Semiring structure #
instance
AddMonoidAlgebra.smulZeroClass
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[SMulZeroClass R k]
:
SMulZeroClass R (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.noZeroSMulDivisors
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Zero R]
[Semiring k]
[SMulZeroClass R k]
[NoZeroSMulDivisors R k]
:
NoZeroSMulDivisors R (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.semiring
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddMonoid G]
:
Semiring (AddMonoidAlgebra k G)
Equations
- AddMonoidAlgebra.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯
def
AddMonoidAlgebra.liftNCRingHom
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[AddMonoid G]
[Semiring R]
(f : k →+* R)
(g : Multiplicative G →* R)
(h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y))
:
AddMonoidAlgebra k G →+* R
liftNC as a RingHom, for when f and g commute
Equations
- AddMonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(AddMonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
instance
AddMonoidAlgebra.nonUnitalCommSemiring
{k : Type u₁}
{G : Type u₂}
[CommSemiring k]
[AddCommSemigroup G]
:
instance
AddMonoidAlgebra.nontrivial
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Nontrivial k]
[Nonempty G]
:
Nontrivial (AddMonoidAlgebra k G)
Derived instances #
instance
AddMonoidAlgebra.commSemiring
{k : Type u₁}
{G : Type u₂}
[CommSemiring k]
[AddCommMonoid G]
:
CommSemiring (AddMonoidAlgebra k G)
Equations
instance
AddMonoidAlgebra.unique
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Subsingleton k]
:
Unique (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.addCommGroup
{k : Type u₁}
{G : Type u₂}
[Ring k]
:
AddCommGroup (AddMonoidAlgebra k G)
Equations
Equations
instance
AddMonoidAlgebra.nonAssocRing
{k : Type u₁}
{G : Type u₂}
[Ring k]
[AddZeroClass G]
:
NonAssocRing (AddMonoidAlgebra k G)
Equations
- AddMonoidAlgebra.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddMonoidAlgebra.intCast_def
{k : Type u₁}
{G : Type u₂}
[Ring k]
[AddZeroClass G]
(z : ℤ)
:
↑z = AddMonoidAlgebra.single 0 ↑z
@[deprecated AddMonoidAlgebra.intCast_def (since := "2024-04-17")]
theorem
AddMonoidAlgebra.int_cast_def
{k : Type u₁}
{G : Type u₂}
[Ring k]
[AddZeroClass G]
(z : ℤ)
:
↑z = AddMonoidAlgebra.single 0 ↑z
Alias of AddMonoidAlgebra.intCast_def.
instance
AddMonoidAlgebra.ring
{k : Type u₁}
{G : Type u₂}
[Ring k]
[AddMonoid G]
:
Ring (AddMonoidAlgebra k G)
Equations
- AddMonoidAlgebra.ring = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
AddMonoidAlgebra.nonUnitalCommRing
{k : Type u₁}
{G : Type u₂}
[CommRing k]
[AddCommSemigroup G]
:
instance
AddMonoidAlgebra.commRing
{k : Type u₁}
{G : Type u₂}
[CommRing k]
[AddCommMonoid G]
:
CommRing (AddMonoidAlgebra k G)
Equations
instance
AddMonoidAlgebra.distribSMul
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
:
DistribSMul R (AddMonoidAlgebra k G)
Equations
instance
AddMonoidAlgebra.distribMulAction
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Monoid R]
[Semiring k]
[DistribMulAction R k]
:
DistribMulAction R (AddMonoidAlgebra k G)
Equations
instance
AddMonoidAlgebra.faithfulSMul
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[SMulZeroClass R k]
[FaithfulSMul R k]
[Nonempty G]
:
FaithfulSMul R (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.module
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring R]
[Semiring k]
[Module R k]
:
Module R (AddMonoidAlgebra k G)
Equations
instance
AddMonoidAlgebra.isScalarTower
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{S : Type u_3}
[Semiring k]
[SMulZeroClass R k]
[SMulZeroClass S k]
[SMul R S]
[IsScalarTower R S k]
:
IsScalarTower R S (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.smulCommClass
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{S : Type u_3}
[Semiring k]
[SMulZeroClass R k]
[SMulZeroClass S k]
[SMulCommClass R S k]
:
SMulCommClass R S (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.isCentralScalar
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[SMulZeroClass R k]
[SMulZeroClass Rᵐᵒᵖ k]
[IsCentralScalar R k]
:
IsCentralScalar R (AddMonoidAlgebra k G)
It is hard to state the equivalent of DistribMulAction G k[G]
because we've never discussed actions of additive groups.
Copies of ext lemmas and bundled singles from Finsupp #
As AddMonoidAlgebra is a type synonym, ext will not unfold it to find ext lemmas.
We need bundled version of Finsupp.single with the right types to state these lemmas.
It is good practice to have those, regardless of the ext issue.
theorem
AddMonoidAlgebra.ext
{k : Type u₁}
{G : Type u₂}
[Semiring k]
⦃f g : AddMonoidAlgebra k G⦄
(H : ∀ (x : G), f x = g x)
:
f = g
A copy of Finsupp.ext for AddMonoidAlgebra.
@[reducible, inline]
abbrev
AddMonoidAlgebra.singleAddHom
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
:
k →+ AddMonoidAlgebra k G
A copy of Finsupp.singleAddHom for AddMonoidAlgebra.
Equations
@[simp]
theorem
AddMonoidAlgebra.singleAddHom_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
(b : k)
:
theorem
AddMonoidAlgebra.addHom_ext'
{k : Type u₁}
{G : Type u₂}
{N : Type u_3}
[Semiring k]
[AddZeroClass N]
⦃f g : AddMonoidAlgebra k G →+ N⦄
(H : ∀ (x : G), f.comp (AddMonoidAlgebra.singleAddHom x) = g.comp (AddMonoidAlgebra.singleAddHom x))
:
f = g
A copy of Finsupp.addHom_ext' for AddMonoidAlgebra.
theorem
AddMonoidAlgebra.distribMulActionHom_ext'
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{N : Type u_3}
[Monoid R]
[Semiring k]
[AddMonoid N]
[DistribMulAction R N]
[DistribMulAction R k]
{f g : AddMonoidAlgebra k G →+[R] N}
(h : ∀ (a : G), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a))
:
f = g
A copy of Finsupp.distribMulActionHom_ext' for AddMonoidAlgebra.
@[reducible, inline]
abbrev
AddMonoidAlgebra.lsingle
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring R]
[Semiring k]
[Module R k]
(a : G)
:
k →ₗ[R] AddMonoidAlgebra k G
A copy of Finsupp.lsingle for AddMonoidAlgebra.
Equations
@[simp]
theorem
AddMonoidAlgebra.lsingle_apply
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
[Semiring R]
[Semiring k]
[Module R k]
(a : G)
(b : k)
:
(AddMonoidAlgebra.lsingle a) b = AddMonoidAlgebra.single a b
theorem
AddMonoidAlgebra.lhom_ext'
{k : Type u₁}
{G : Type u₂}
{R : Type u_2}
{N : Type u_3}
[Semiring R]
[Semiring k]
[AddCommMonoid N]
[Module R N]
[Module R k]
⦃f g : AddMonoidAlgebra k G →ₗ[R] N⦄
(H : ∀ (x : G), f ∘ₗ AddMonoidAlgebra.lsingle x = g ∘ₗ AddMonoidAlgebra.lsingle x)
:
f = g
A copy of Finsupp.lhom_ext' for AddMonoidAlgebra.
theorem
AddMonoidAlgebra.mul_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[DecidableEq G]
[Add G]
(f g : AddMonoidAlgebra k G)
(x : G)
:
(f * g) x = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => if a₁ + a₂ = x then b₁ * b₂ else 0
theorem
AddMonoidAlgebra.single_mul_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
{a₁ a₂ : G}
{b₁ b₂ : k}
:
AddMonoidAlgebra.single a₁ b₁ * AddMonoidAlgebra.single a₂ b₂ = AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
theorem
AddMonoidAlgebra.single_commute_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
{a₁ a₂ : G}
{b₁ b₂ : k}
(ha : AddCommute a₁ a₂)
(hb : Commute b₁ b₂)
:
Commute (AddMonoidAlgebra.single a₁ b₁) (AddMonoidAlgebra.single a₂ b₂)
theorem
AddMonoidAlgebra.single_pow
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddMonoid G]
{a : G}
{b : k}
(n : ℕ)
:
AddMonoidAlgebra.single a b ^ n = AddMonoidAlgebra.single (n • a) (b ^ n)
@[simp]
theorem
AddMonoidAlgebra.mapDomain_one
{α : Type u_3}
{β : Type u_4}
{α₂ : Type u_5}
[Semiring β]
[Zero α]
[Zero α₂]
{F : Type u_6}
[FunLike F α α₂]
[ZeroHomClass F α α₂]
(f : F)
:
AddMonoidAlgebra.mapDomain (⇑f) 1 = 1
Like Finsupp.mapDomain_zero, but for the 1 we define in this file
theorem
AddMonoidAlgebra.mapDomain_mul
{α : Type u_3}
{β : Type u_4}
{α₂ : Type u_5}
[Semiring β]
[Add α]
[Add α₂]
{F : Type u_6}
[FunLike F α α₂]
[AddHomClass F α α₂]
(f : F)
(x y : AddMonoidAlgebra β α)
:
AddMonoidAlgebra.mapDomain (⇑f) (x * y) = AddMonoidAlgebra.mapDomain (⇑f) x * AddMonoidAlgebra.mapDomain (⇑f) y
Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file
The embedding of an additive magma into its additive magma algebra.
Equations
- AddMonoidAlgebra.ofMagma k G = { toFun := fun (a : Multiplicative G) => AddMonoidAlgebra.single a 1, map_mul' := ⋯ }
@[simp]
theorem
AddMonoidAlgebra.ofMagma_apply
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[Add G]
(a : Multiplicative G)
:
(AddMonoidAlgebra.ofMagma k G) a = AddMonoidAlgebra.single a 1
def
AddMonoidAlgebra.of
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[AddZeroClass G]
:
Multiplicative G →* AddMonoidAlgebra k G
Embedding of a magma with zero into its magma algebra.
Equations
- AddMonoidAlgebra.of k G = { toFun := fun (a : Multiplicative G) => AddMonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }
Embedding of a magma with zero G, into its magma algebra, having G as source.
Equations
- AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1
@[simp]
theorem
AddMonoidAlgebra.of_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(a : Multiplicative G)
:
(AddMonoidAlgebra.of k G) a = AddMonoidAlgebra.single (Multiplicative.toAdd a) 1
@[simp]
theorem
AddMonoidAlgebra.of'_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(a : G)
:
AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1
theorem
AddMonoidAlgebra.of'_eq_of
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(a : G)
:
AddMonoidAlgebra.of' k G a = (AddMonoidAlgebra.of k G) (Multiplicative.ofAdd a)
theorem
AddMonoidAlgebra.of_injective
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Nontrivial k]
[AddZeroClass G]
:
theorem
AddMonoidAlgebra.of'_commute
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
{a : G}
(h : ∀ (a' : G), AddCommute a a')
(f : AddMonoidAlgebra k G)
:
Commute (AddMonoidAlgebra.of' k G a) f
def
AddMonoidAlgebra.singleHom
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
:
k × Multiplicative G →* AddMonoidAlgebra k G
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 : k × Multiplicative G) => AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1, map_one' := ⋯, map_mul' := ⋯ }
@[simp]
theorem
AddMonoidAlgebra.singleHom_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(a : k × Multiplicative G)
:
AddMonoidAlgebra.singleHom a = AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1
@[simp]
theorem
AddMonoidAlgebra.smul_single'
{k : Type u₁}
{G : Type u₂}
[Semiring k]
(c : k)
(a : G)
(b : k)
:
c • AddMonoidAlgebra.single a b = AddMonoidAlgebra.single a (c * b)
Copy of Finsupp.smul_single' that avoids the AddMonoidAlgebra = Finsupp defeq abuse.
theorem
AddMonoidAlgebra.mul_single_apply_aux
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
(f : AddMonoidAlgebra k G)
(r : k)
(x y z : G)
(H : ∀ (a : G), a + x = z ↔ a = y)
:
(f * AddMonoidAlgebra.single x r) z = f y * r
theorem
AddMonoidAlgebra.mul_single_zero_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(f : AddMonoidAlgebra k G)
(r : k)
(x : G)
:
(f * AddMonoidAlgebra.single 0 r) x = f x * r
theorem
AddMonoidAlgebra.mul_single_apply_of_not_exists_add
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
(r : k)
{g g' : G}
(x : AddMonoidAlgebra k G)
(h : ¬∃ (d : G), g' = d + g)
:
(x * AddMonoidAlgebra.single g r) g' = 0
theorem
AddMonoidAlgebra.single_mul_apply_aux
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
(f : AddMonoidAlgebra k G)
(r : k)
(x y z : G)
(H : ∀ (a : G), x + a = y ↔ a = z)
:
(AddMonoidAlgebra.single x r * f) y = r * f z
theorem
AddMonoidAlgebra.single_zero_mul_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddZeroClass G]
(f : AddMonoidAlgebra k G)
(r : k)
(x : G)
:
(AddMonoidAlgebra.single 0 r * f) x = r * f x
theorem
AddMonoidAlgebra.single_mul_apply_of_not_exists_add
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[Add G]
(r : k)
{g g' : G}
(x : AddMonoidAlgebra k G)
(h : ¬∃ (d : G), g' = g + d)
:
(AddMonoidAlgebra.single g r * x) g' = 0
theorem
AddMonoidAlgebra.mul_single_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddGroup G]
(f : AddMonoidAlgebra k G)
(r : k)
(x y : G)
:
(f * AddMonoidAlgebra.single x r) y = f (y - x) * r
theorem
AddMonoidAlgebra.single_mul_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddGroup G]
(r : k)
(x : G)
(f : AddMonoidAlgebra k G)
(y : G)
:
theorem
AddMonoidAlgebra.liftNC_smul
{k : Type u₁}
{G : Type u₂}
[Semiring k]
{R : Type u_3}
[AddZeroClass G]
[Semiring R]
(f : k →+* R)
(g : Multiplicative G →* R)
(c : k)
(φ : MonoidAlgebra k G)
:
(AddMonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (AddMonoidAlgebra.liftNC ↑f ⇑g) φ
theorem
AddMonoidAlgebra.induction_on
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddMonoid G]
{p : AddMonoidAlgebra k G → Prop}
(f : AddMonoidAlgebra k G)
(hM : ∀ (g : G), p ((AddMonoidAlgebra.of k G) (Multiplicative.ofAdd g)))
(hadd : ∀ (f g : AddMonoidAlgebra k G), p f → p g → p (f + g))
(hsmul : ∀ (r : k) (f : AddMonoidAlgebra k G), p f → p (r • f))
:
p f
def
AddMonoidAlgebra.mapDomainRingHom
{G : Type u₂}
(k : Type u_3)
[Semiring k]
{H : Type u_4}
{F : Type u_5}
[AddMonoid G]
[AddMonoid H]
[FunLike F G H]
[AddMonoidHomClass F G H]
(f : F)
:
AddMonoidAlgebra k G →+* AddMonoidAlgebra k H
If f : G → H is an additive homomorphism between two additive monoids, then
Finsupp.mapDomain f is a ring homomorphism between their add monoid algebras.
Equations
- AddMonoidAlgebra.mapDomainRingHom k f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
AddMonoidAlgebra.mapDomainRingHom_apply
{G : Type u₂}
(k : Type u_3)
[Semiring k]
{H : Type u_4}
{F : Type u_5}
[AddMonoid G]
[AddMonoid H]
[FunLike F G H]
[AddMonoidHomClass F G H]
(f : F)
(a✝ : G →₀ k)
:
(AddMonoidAlgebra.mapDomainRingHom k f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝
Conversions between AddMonoidAlgebra and MonoidAlgebra #
We have not defined k[G] = MonoidAlgebra k (Multiplicative G)
because historically this caused problems;
since the changes that have made nsmul definitional, this would be possible,
but for now we just construct the ring isomorphisms using RingEquiv.refl _.
def
AddMonoidAlgebra.toMultiplicative
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[Add G]
:
AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G)
The equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of
Multiplicative
Equations
- One or more equations did not get rendered due to their size.
def
MonoidAlgebra.toAdditive
(k : Type u₁)
(G : Type u₂)
[Semiring k]
[Mul G]
:
MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G)
The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive
Equations
- One or more equations did not get rendered due to their size.
Non-unital, non-associative algebra structure #
instance
AddMonoidAlgebra.isScalarTower_self
(k : Type u₁)
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
[Add G]
[IsScalarTower R k k]
:
IsScalarTower R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G)
instance
AddMonoidAlgebra.smulCommClass_self
(k : Type u₁)
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
[Add G]
[SMulCommClass R k k]
:
SMulCommClass R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G)
Note that if k is a CommSemiring then we have SMulCommClass k k k and so we can take
R = k in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication.
instance
AddMonoidAlgebra.smulCommClass_symm_self
(k : Type u₁)
{G : Type u₂}
{R : Type u_2}
[Semiring k]
[DistribSMul R k]
[Add G]
[SMulCommClass k R k]
:
SMulCommClass (AddMonoidAlgebra k G) R (AddMonoidAlgebra k G)
Algebra structure #
def
AddMonoidAlgebra.singleZeroRingHom
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddMonoid G]
:
k →+* AddMonoidAlgebra k G
Finsupp.single 0 as a RingHom
Equations
- AddMonoidAlgebra.singleZeroRingHom = { toFun := (↑(Finsupp.singleAddHom 0)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
AddMonoidAlgebra.singleZeroRingHom_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddMonoid G]
(a✝ : k)
:
AddMonoidAlgebra.singleZeroRingHom a✝ = (↑(Finsupp.singleAddHom 0)).toFun a✝
theorem
AddMonoidAlgebra.ringHom_ext
{k : Type u₁}
{G : Type u₂}
{R : Type u_3}
[Semiring k]
[AddMonoid G]
[Semiring R]
{f g : AddMonoidAlgebra k G →+* R}
(h₀ : ∀ (b : k), f (AddMonoidAlgebra.single 0 b) = g (AddMonoidAlgebra.single 0 b))
(h_of : ∀ (a : G), f (AddMonoidAlgebra.single a 1) = g (AddMonoidAlgebra.single a 1))
:
f = g
If two ring homomorphisms from k[G] are equal on all single a 1
and single 0 b, then they are equal.
theorem
AddMonoidAlgebra.ringHom_ext'
{k : Type u₁}
{G : Type u₂}
{R : Type u_3}
[Semiring k]
[AddMonoid G]
[Semiring R]
{f g : AddMonoidAlgebra k G →+* R}
(h₁ : f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom)
(h_of : (↑f).comp (AddMonoidAlgebra.of k G) = (↑g).comp (AddMonoidAlgebra.of k G))
:
f = g
If two ring homomorphisms from k[G] are equal on all single a 1
and single 0 b, then they are equal.
See note [partially-applied ext lemmas].
noncomputable def
AddMonoidAlgebra.opRingEquiv
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddCommMonoid G]
:
(AddMonoidAlgebra k G)ᵐᵒᵖ ≃+* AddMonoidAlgebra kᵐᵒᵖ G
The opposite of an R[I] is ring equivalent to
the AddMonoidAlgebra Rᵐᵒᵖ I over the opposite ring, taking elements to their opposite.
Equations
- AddMonoidAlgebra.opRingEquiv = { toEquiv := (MulOpposite.opAddEquiv.symm.trans (Finsupp.mapRange.addEquiv MulOpposite.opAddEquiv)).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
@[simp]
theorem
AddMonoidAlgebra.opRingEquiv_symm_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddCommMonoid G]
(a✝ : G →₀ kᵐᵒᵖ)
:
AddMonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ a✝)
@[simp]
theorem
AddMonoidAlgebra.opRingEquiv_apply
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddCommMonoid G]
(a✝ : (G →₀ k)ᵐᵒᵖ)
:
AddMonoidAlgebra.opRingEquiv a✝ = Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝)
theorem
AddMonoidAlgebra.opRingEquiv_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddCommMonoid G]
(r : k)
(x : G)
:
AddMonoidAlgebra.opRingEquiv (MulOpposite.op (AddMonoidAlgebra.single x r)) = AddMonoidAlgebra.single x (MulOpposite.op r)
theorem
AddMonoidAlgebra.opRingEquiv_symm_single
{k : Type u₁}
{G : Type u₂}
[Semiring k]
[AddCommMonoid G]
(r : kᵐᵒᵖ)
(x : Gᵐᵒᵖ)
:
theorem
AddMonoidAlgebra.prod_single
{k : Type u₁}
{G : Type u₂}
{ι : Type ui}
[CommSemiring k]
[AddCommMonoid G]
{s : Finset ι}
{a : ι → G}
{b : ι → k}
:
∏ i ∈ s, AddMonoidAlgebra.single (a i) (b i) = AddMonoidAlgebra.single (∑ i ∈ s, a i) (∏ i ∈ s, b i)