# 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 #

def MonoidAlgebra (k : Type u₁) (G : Type u₂) [] :
Type (max u₁ u₂)

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
Instances For
instance MonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [] :
Equations
instance MonoidAlgebra.addCommMonoid (k : Type u₁) (G : Type u₂) [] :
Equations
instance MonoidAlgebra.instIsCancelAdd (k : Type u₁) (G : Type u₂) [] [] :
Equations
• =
instance MonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [] :
CoeFun (MonoidAlgebra k G) fun (x : ) => Gk
Equations
• = Finsupp.instCoeFun
@[reducible, inline]
abbrev MonoidAlgebra.single {k : Type u₁} {G : Type u₂} [] (a : G) (b : k) :
Equations
Instances For
theorem MonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [] (a : G) :
theorem MonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [] (a : G) (b₁ : k) (b₂ : k) :
MonoidAlgebra.single a (b₁ + b₂) =
@[simp]
theorem MonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [] {N : Type u_3} [] {a : G} {b : k} {h : GkN} (h_zero : h a 0 = 0) :
= h a b
@[simp]
theorem MonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [] (f : ) :
Finsupp.sum f MonoidAlgebra.single = f
theorem MonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [] {a : G} {a' : G} {b : k} [Decidable (a = a')] :
a' = if a = a' then b else 0
@[simp]
theorem MonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [] {a : G} {b : k} :
b = 0
@[reducible, inline]
abbrev MonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [] {G' : Type u_3} (f : GG') (v : ) :
Equations
Instances For
theorem MonoidAlgebra.mapDomain_sum {k : Type u₁} {G : Type u₂} [] {k' : Type u_3} {G' : Type u_4} [Semiring k'] {f : GG'} {s : } {v : Gk'} :
= 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} [] (f : k →+ R) (g : GR) :
→+ 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
Instances For
@[simp]
theorem MonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [] (f : k →+ R) (g : GR) (a : G) (b : k) :
= f b * g a
@[irreducible]
def MonoidAlgebra.mul' {k : Type u₁} {G : Type u₂} [] [Mul G] (f : ) (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
Instances For
instance MonoidAlgebra.instMul {k : Type u₁} {G : Type u₂} [] [Mul 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₂} [] [Mul G] {f : } {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₂)
instance MonoidAlgebra.nonUnitalNonAssocSemiring {k : Type u₁} {G : Type u₂} [] [Mul G] :
Equations
• MonoidAlgebra.nonUnitalNonAssocSemiring =
theorem MonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [Mul G] [] {g_hom : Type u_3} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a : ) (b : ) (h_comm : ∀ {x y : G}, y a.supportCommute (f (b x)) (g y)) :
(MonoidAlgebra.liftNC f g) (a * b) = (MonoidAlgebra.liftNC f g) a * (MonoidAlgebra.liftNC f g) b
instance MonoidAlgebra.nonUnitalSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.nonUnitalSemiring =
instance MonoidAlgebra.one {k : Type u₁} {G : Type u₂} [] [One 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 := }
theorem MonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [] [One G] :
@[simp]
theorem MonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [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
instance MonoidAlgebra.nonAssocSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.nonAssocSemiring =
theorem MonoidAlgebra.natCast_def {k : Type u₁} {G : Type u₂} [] [] (n : ) :
n =
@[deprecated MonoidAlgebra.natCast_def]
theorem MonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [] [] (n : ) :
n =

Alias of MonoidAlgebra.natCast_def.

#### Semiring structure #

instance MonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.semiring = Semiring.mk npowRec
def MonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) :

liftNC as a RingHom, for when f x and g y commute

Equations
Instances For
instance MonoidAlgebra.nonUnitalCommSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.nonUnitalCommSemiring =
instance MonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [] [] [] :
Equations
• =

#### Derived instances #

instance MonoidAlgebra.commSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.commSemiring =
instance MonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.unique = Finsupp.uniqueOfRight
instance MonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :
Equations
instance MonoidAlgebra.nonUnitalNonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [Mul G] :
Equations
• MonoidAlgebra.nonUnitalNonAssocRing =
instance MonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [] :
Equations
• MonoidAlgebra.nonUnitalRing =
instance MonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [] :
Equations
theorem MonoidAlgebra.intCast_def {k : Type u₁} {G : Type u₂} [Ring k] [] (z : ) :
z =
@[deprecated MonoidAlgebra.intCast_def]
theorem MonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [] (z : ) :
z =

Alias of MonoidAlgebra.intCast_def.

instance MonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [] :
Equations
• MonoidAlgebra.ring = Ring.mk SubNegMonoid.zsmul
instance MonoidAlgebra.nonUnitalCommRing {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.nonUnitalCommRing =
instance MonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [] [] :
Equations
• MonoidAlgebra.commRing =
instance MonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] :
Equations
• MonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass
instance MonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] :
Equations
• MonoidAlgebra.distribSMul =
instance MonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] :
Equations
• MonoidAlgebra.distribMulAction =
instance MonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [Module R k] :
Equations
• MonoidAlgebra.module =
instance MonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] [] :
Equations
• =
instance MonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [] [] [] [SMul R S] [] :
Equations
• =
instance MonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [] [] [] [] :
Equations
• =
instance MonoidAlgebra.isCentralScalar {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] [] :
Equations
• =
def MonoidAlgebra.comapDistribMulActionSelf {k : Type u₁} {G : Type u₂} [] [] :

This is not an instance as it conflicts with MonoidAlgebra.distribMulAction when G = kˣ.

Equations
• MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction
Instances For
theorem MonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [] [] [Mul G] (f : ) (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 MonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [] [Mul G] (f : ) (g : ) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p s p.1 * p.2 = x) :
(f * g) x = ps, f p.1 * g p.2
@[simp]
theorem MonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [] [Mul G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} :
* = MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
theorem MonoidAlgebra.single_commute_single {k : Type u₁} {G : Type u₂} [] [Mul G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
theorem MonoidAlgebra.single_commute {k : Type u₁} {G : Type u₂} [] [Mul G] {a : G} {b : k} (ha : ∀ (a' : G), Commute a a') (hb : ∀ (b' : k), Commute b b') (f : ) :
@[simp]
theorem MonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [] [] {a : G} {b : k} (n : ) :
= MonoidAlgebra.single (a ^ n) (b ^ n)
@[simp]
theorem MonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [] [One α] [One α₂] {F : Type u_6} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) :
= 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} [] [Mul α] [Mul α₂] {F : Type u_6} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x : ) (y : ) :

Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

@[simp]
theorem MonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [] [Mul G] (a : G) :
a =
def MonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [] [Mul G] :

The embedding of a magma into its magma algebra.

Equations
• = { toFun := fun (a : G) => , map_mul' := }
Instances For
@[simp]
theorem MonoidAlgebra.of_apply (k : Type u₁) (G : Type u₂) [] [] (a : G) :
def MonoidAlgebra.of (k : Type u₁) (G : Type u₂) [] [] :
G →*

The embedding of a unital magma into its magma algebra.

Equations
• = { toFun := fun (a : G) => , map_one' := , map_mul' := }
Instances For
theorem MonoidAlgebra.smul_of {k : Type u₁} {G : Type u₂} [] [] (g : G) (r : k) :
theorem MonoidAlgebra.of_injective {k : Type u₁} {G : Type u₂} [] [] [] :
theorem MonoidAlgebra.of_commute {k : Type u₁} {G : Type u₂} [] [] {a : G} (h : ∀ (a' : G), Commute a a') (f : ) :
@[simp]
theorem MonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [] [] (a : k × G) :
MonoidAlgebra.singleHom a = MonoidAlgebra.single a.2 a.1
def MonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [] [] :
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' := }
Instances For
theorem MonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [] [Mul G] (f : ) {r : k} {x : G} {y : G} {z : G} (H : ∀ (a : G), a * x = z a = y) :
(f * ) z = f y * r
theorem MonoidAlgebra.mul_single_one_apply {k : Type u₁} {G : Type u₂} [] [] (f : ) (r : k) (x : G) :
(f * ) x = f x * r
theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [] [Mul G] (r : k) {g : G} {g' : G} (x : ) (h : ¬∃ (d : G), g' = d * g) :
(x * ) g' = 0
theorem MonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [] [Mul G] (f : ) {r : k} {x : G} {y : G} {z : G} (H : ∀ (a : G), x * a = y a = z) :
( * f) y = r * f z
theorem MonoidAlgebra.single_one_mul_apply {k : Type u₁} {G : Type u₂} [] [] (f : ) (r : k) (x : G) :
( * f) x = r * f x
theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [] [Mul G] (r : k) {g : G} {g' : G} (x : ) (h : ¬∃ (d : G), g' = g * d) :
( * x) g' = 0
theorem MonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [] [] {R : Type u_3} [] (f : k →+* R) (g : G →* R) (c : k) (φ : ) :
(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} [] [] [Mul G] [] :
Equations
• =
instance MonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [] [] [Mul 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.

Equations
• =
instance MonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [] [] [Mul G] [] :
Equations
• =
theorem MonoidAlgebra.nonUnitalAlgHom_ext (k : Type u₁) {G : Type u₂} [] [Mul G] {A : Type u₃} [] {φ₁ : →ₙₐ[k] A} {φ₂ : →ₙₐ[k] A} (h : ∀ (x : G), φ₁ = φ₂ ) :
φ₁ = φ₂

A non_unital k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

theorem MonoidAlgebra.nonUnitalAlgHom_ext'_iff {k : Type u₁} {G : Type u₂} [] [Mul G] {A : Type u₃} [] {φ₁ : →ₙₐ[k] A} {φ₂ : →ₙₐ[k] A} :
φ₁ = φ₂ φ₁.toMulHom.comp = φ₂.toMulHom.comp
theorem MonoidAlgebra.nonUnitalAlgHom_ext' (k : Type u₁) {G : Type u₂} [] [Mul G] {A : Type u₃} [] {φ₁ : →ₙₐ[k] A} {φ₂ : →ₙₐ[k] A} (h : φ₁.toMulHom.comp = φ₂.toMulHom.comp ) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

@[simp]
theorem MonoidAlgebra.liftMagma_symm_apply (k : Type u₁) {G : Type u₂} [] [Mul G] {A : Type u₃} [Module k A] [] [] (F : →ₙₐ[k] A) :
.symm F = F.toMulHom.comp
@[simp]
theorem MonoidAlgebra.liftMagma_apply_apply (k : Type u₁) {G : Type u₂} [] [Mul G] {A : Type u₃} [Module k A] [] [] (f : G →ₙ* A) (a : ) :
( f) a = Finsupp.sum a fun (m : G) (t : k) => t f m
def MonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [] [Mul G] {A : Type u₃} [Module k A] [] [] :
(G →ₙ* A) ( →ₙₐ[k] A)

The functor G ↦ MonoidAlgebra k G, from the category of magmas to the category of non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other direction.

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

#### Algebra structure #

theorem MonoidAlgebra.single_one_comm {k : Type u₁} {G : Type u₂} [] [] (r : k) (f : ) :
=
@[simp]
theorem MonoidAlgebra.singleOneRingHom_apply {k : Type u₁} {G : Type u₂} [] [] :
∀ (a : k), MonoidAlgebra.singleOneRingHom a = (↑).toFun a
def MonoidAlgebra.singleOneRingHom {k : Type u₁} {G : Type u₂} [] [] :

Finsupp.single 1 as a RingHom

Equations
• MonoidAlgebra.singleOneRingHom = { toFun := (↑).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem MonoidAlgebra.mapDomainRingHom_apply {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [] [] [] [FunLike F G H] [] (f : F) :
∀ (a : G →₀ k), = (↑).toFun a
def MonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [] [] [] [FunLike F G H] [] (f : F) :

If f : G → H is a multiplicative homomorphism between two monoids, then Finsupp.mapDomain f is a ring homomorphism between their monoid algebras.

Equations
• = { toFun := (↑).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem MonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [] [] [] {f : →+* R} {g : →+* R} (h₁ : ∀ (b : k), f = g ) (h_of : ∀ (a : G), f = 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.

theorem MonoidAlgebra.ringHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_3} [] [] [] {f : →+* R} {g : →+* R} :
f = g f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom (↑f).comp (MonoidAlgebra.of k G) = (↑g).comp (MonoidAlgebra.of k G)
theorem MonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [] [] [] {f : →+* R} {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].

instance MonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {A : Type u_3} [] [] [Algebra k A] [] :

The instance Algebra k (MonoidAlgebra A G) whenever we have Algebra k A.

In particular this provides the instance Algebra k (MonoidAlgebra k G).

Equations
@[simp]
theorem MonoidAlgebra.singleOneAlgHom_apply {k : Type u₁} {G : Type u₂} {A : Type u_3} [] [] [Algebra k A] [] :
∀ (a : A), MonoidAlgebra.singleOneAlgHom a =
def MonoidAlgebra.singleOneAlgHom {k : Type u₁} {G : Type u₂} {A : Type u_3} [] [] [Algebra k A] [] :

Finsupp.single 1 as an AlgHom

Equations
• MonoidAlgebra.singleOneAlgHom = { toRingHom := MonoidAlgebra.singleOneRingHom, commutes' := }
Instances For
@[simp]
theorem MonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {A : Type u_3} [] [] [Algebra k A] [] :
(algebraMap k (MonoidAlgebra A G)) = (algebraMap k A)
theorem MonoidAlgebra.single_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} [] [] (a : G) (b : k) :
theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} {A : Type u_3} [] [] [Algebra k A] [] (a : G) (b : k) :
theorem MonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [] [] {p : Prop} (f : ) (hM : ∀ (g : G), p ((MonoidAlgebra.of k G) g)) (hadd : ∀ (f g : ), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : ), p fp (r f)) :
p f
def MonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] {B : Type u_3} [] [Algebra k B] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ (x : A) (y : G), Commute (f x) (g y)) :

liftNCRingHom as an AlgHom, for when f is an AlgHom

Equations
Instances For
theorem MonoidAlgebra.algHom_ext {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] ⦃φ₁ : →ₐ[k] A ⦃φ₂ : →ₐ[k] A (h : ∀ (x : G), φ₁ = φ₂ ) :
φ₁ = φ₂

A k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

theorem MonoidAlgebra.algHom_ext'_iff {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] {φ₁ : →ₐ[k] A} {φ₂ : →ₐ[k] A} :
φ₁ = φ₂ (↑φ₁).comp (MonoidAlgebra.of k G) = (↑φ₂).comp (MonoidAlgebra.of k G)
theorem MonoidAlgebra.algHom_ext' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] ⦃φ₁ : →ₐ[k] A ⦃φ₂ : →ₐ[k] A (h : (↑φ₁).comp (MonoidAlgebra.of k G) = (↑φ₂).comp (MonoidAlgebra.of k G)) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

def MonoidAlgebra.lift (k : Type u₁) (G : Type u₂) [] [] (A : Type u₃) [] [Algebra k A] :
(G →* A) ( →ₐ[k] A)

Any monoid homomorphism G →* A can be lifted to an algebra homomorphism MonoidAlgebra k G →ₐ[k] A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : G →* A) (f : ) :
((MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => (algebraMap k A) b * F a
theorem MonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : G →* A) (f : ) :
((MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => b F a
theorem MonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : G →* A) :
((MonoidAlgebra.lift k G A) F) = (MonoidAlgebra.liftNC (algebraMap k A) F)
@[simp]
theorem MonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : →ₐ[k] A) (x : G) :
((MonoidAlgebra.lift k G A).symm F) x = F
@[simp]
theorem MonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : G →* A) (a : G) (b : k) :
((MonoidAlgebra.lift k G A) F) = b F a
theorem MonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : G →* A) (x : G) :
((MonoidAlgebra.lift k G A) F) ((MonoidAlgebra.of k G) x) = F x
theorem MonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : →ₐ[k] A) :
F = (MonoidAlgebra.lift k G A) ((↑F).comp (MonoidAlgebra.of k G))
theorem MonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : →ₐ[k] A) (f : ) :
F f = Finsupp.sum f fun (a : G) (b : k) => b F

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

@[simp]
theorem MonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_4) (A : Type u_5) [] [] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) :
∀ (a : G →₀ A), = (↑).toFun a
def MonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_4) (A : Type u_5) [] [] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) :

If f : G → H is a homomorphism between two magmas, then Finsupp.mapDomain f is a non-unital algebra homomorphism between their magma algebras.

Equations
• = { toFun := (↑).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
theorem MonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] {F : Type u_4} [FunLike F G H] [] (f : F) (r : k) :
@[simp]
theorem MonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} [] (k : Type u_4) (A : Type u_5) [] [] [Algebra k A] {H : Type u_6} {F : Type u_7} [] [FunLike F G H] [] (f : F) :
∀ (a : G →₀ A), a = Finsupp.mapDomain (⇑f) a
def MonoidAlgebra.mapDomainAlgHom {G : Type u₂} [] (k : Type u_4) (A : Type u_5) [] [] [Algebra k A] {H : Type u_6} {F : Type u_7} [] [FunLike F G H] [] (f : F) :

If f : G → H is a multiplicative homomorphism between two monoids, then Finsupp.mapDomain f is an algebra homomorphism between their monoid algebras.

Equations
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem MonoidAlgebra.mapDomainAlgHom_id {G : Type u₂} [] (k : Type u_4) (A : Type u_5) [] [] [Algebra k A] :
@[simp]
theorem MonoidAlgebra.mapDomainAlgHom_comp (k : Type u_4) (A : Type u_5) {G₁ : Type u_6} {G₂ : Type u_7} {G₃ : Type u_8} [] [] [Algebra k A] [Monoid G₁] [Monoid G₂] [Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) :
MonoidAlgebra.mapDomainAlgHom k A (g.comp f) = .comp
def MonoidAlgebra.domCongr (k : Type u₁) {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] (e : G ≃* H) :

If e : G ≃* H is a multiplicative equivalence between two monoids, then MonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

Equations
Instances For
theorem MonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] (e : G ≃* H) :
=
@[simp]
theorem MonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] (e : G ≃* H) (f : ) (h : H) :
( f) h = f (e.symm h)
@[simp]
theorem MonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] (e : G ≃* H) (f : ) :
( f).support = Finset.map (↑e).toEmbedding f.support
@[simp]
theorem MonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] (e : G ≃* H) (g : G) (a : A) :
@[simp]
theorem MonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} [] [] (A : Type u₃) [] [Algebra k A] :
= AlgEquiv.refl
@[simp]
theorem MonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} [] [] [] (A : Type u₃) [] [Algebra k A] (e : G ≃* H) :
.symm = MonoidAlgebra.domCongr k A e.symm
def MonoidAlgebra.GroupSMul.linearMap (k : Type u₁) {G : Type u₂} [] [] (V : Type u₃) [] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) :

When V is a k[G]-module, multiplication by a group element g is a k-linear map.

Equations
• = { toFun := fun (v : V) => , map_add' := , map_smul' := }
Instances For
@[simp]
theorem MonoidAlgebra.GroupSMul.linearMap_apply (k : Type u₁) {G : Type u₂} [] [] (V : Type u₃) [] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) (v : V) :
v =
def MonoidAlgebra.equivariantOfLinearOfComm {k : Type u₁} {G : Type u₂} [] [] {V : Type u₃} {W : Type u₄} [] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f ( v) = f v) :

Build a k[G]-linear map from a k-linear map and evidence that it is G-equivariant.

Equations
• = { toFun := f, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MonoidAlgebra.equivariantOfLinearOfComm_apply {k : Type u₁} {G : Type u₂} [] [] {V : Type u₃} {W : Type u₄} [] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f ( v) = f v) (v : V) :
= f v
theorem MonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [] [] {s : } {a : ιG} {b : ιk} :
is, MonoidAlgebra.single (a i) (b i) = MonoidAlgebra.single (∏ is, a i) (∏ is, b i)
@[simp]
theorem MonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [] [] (f : ) (r : k) (x : G) (y : G) :
(f * ) y = f (y * x⁻¹) * r
@[simp]
theorem MonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [] [] (r : k) (x : G) (f : ) (y : G) :
( * f) y = r * f (x⁻¹ * y)
theorem MonoidAlgebra.mul_apply_left {k : Type u₁} {G : Type u₂} [] [] (f : ) (g : ) (x : G) :
(f * g) x = Finsupp.sum f fun (a : G) (b : k) => b * g (a⁻¹ * x)
theorem MonoidAlgebra.mul_apply_right {k : Type u₁} {G : Type u₂} [] [] (f : ) (g : ) (x : G) :
(f * g) x = Finsupp.sum g fun (a : G) (b : k) => f (x * a⁻¹) * b
@[simp]
theorem MonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [] [] :
∀ (a : (G →₀ k)ᵐᵒᵖ), MonoidAlgebra.opRingEquiv a = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op )
@[simp]
theorem MonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [] [] :
∀ (a : Gᵐᵒᵖ →₀ kᵐᵒᵖ), MonoidAlgebra.opRingEquiv.symm a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a))
noncomputable def MonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [] [] :

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.
Instances For
theorem MonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [] [] (r : k) (x : G) :
MonoidAlgebra.opRingEquiv =
theorem MonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [] [] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
MonoidAlgebra.opRingEquiv.symm =
def MonoidAlgebra.submoduleOfSMulMem {k : Type u₁} {G : Type u₂} [] [] {V : Type u_3} [] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (W : ) (h : ∀ (g : G), vW, (MonoidAlgebra.of k G) g v W) :

A submodule over k which is stable under scalar multiplication by elements of G is a submodule over MonoidAlgebra k G

Equations
• = { carrier := W, add_mem' := , zero_mem' := , smul_mem' := }
Instances For

def AddMonoidAlgebra (k : Type u₁) (G : Type u₂) [] :
Type (max u₂ u₁)

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
Instances For

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.
Instances For
instance AddMonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [] :
Equations
instance AddMonoidAlgebra.addCommMonoid (k : Type u₁) (G : Type u₂) [] :
Equations
instance AddMonoidAlgebra.instIsCancelAdd (k : Type u₁) (G : Type u₂) [] [] :
Equations
• =
instance AddMonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [] :
CoeFun (AddMonoidAlgebra k G) fun (x : ) => Gk
Equations
• = Finsupp.instCoeFun
@[reducible, inline]
abbrev AddMonoidAlgebra.single {k : Type u₁} {G : Type u₂} [] (a : G) (b : k) :
Equations
Instances For
theorem AddMonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [] (a : G) :
theorem AddMonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [] (a : G) (b₁ : k) (b₂ : k) :
AddMonoidAlgebra.single a (b₁ + b₂) =
@[simp]
theorem AddMonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [] {N : Type u_3} [] {a : G} {b : k} {h : GkN} (h_zero : h a 0 = 0) :
= h a b
@[simp]
theorem AddMonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [] (f : ) :
theorem AddMonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [] {a : G} {a' : G} {b : k} [Decidable (a = a')] :
a' = if a = a' then b else 0
@[simp]
theorem AddMonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [] {a : G} {b : k} :
b = 0
@[reducible, inline]
abbrev AddMonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [] {G' : Type u_3} (f : GG') (v : ) :
Equations
Instances For
theorem AddMonoidAlgebra.mapDomain_sum {k : Type u₁} {G : Type u₂} [] {k' : Type u_3} {G' : Type u_4} [Semiring k'] {f : GG'} {s : } {v : Gk'} :
= Finsupp.sum s fun (a : G) (b : k') => AddMonoidAlgebra.mapDomain f (v a b)
theorem AddMonoidAlgebra.mapDomain_single {k : Type u₁} {G : Type u₂} [] {G' : Type u_3} {f : GG'} {a : G} {b : k} :
def AddMonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [] (f : k →+ R) (g : R) :
→+ 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
Instances For
@[simp]
theorem AddMonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [] (f : k →+ R) (g : R) (a : G) (b : k) :
= f b * g (Multiplicative.ofAdd a)
instance AddMonoidAlgebra.hasMul {k : Type u₁} {G : Type u₂} [] [Add 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 : ) => }
theorem AddMonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [] [Add G] {f : } {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₂} [] [Add G] :
Equations
theorem AddMonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [Add G] [] {g_hom : Type u_3} [FunLike g_hom R] [MulHomClass g_hom R] (f : k →+* R) (g : g_hom) (a : ) (b : ) (h_comm : ∀ {x y : G}, y a.supportCommute (f (b x)) (g (Multiplicative.ofAdd y))) :
instance AddMonoidAlgebra.one {k : Type u₁} {G : Type u₂} [] [Zero 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 := }
theorem AddMonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [] [Zero G] :
@[simp]
theorem AddMonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [Zero G] [] {g_hom : Type u_3} [FunLike g_hom R] [OneHomClass g_hom R] (f : k →+* R) (g : g_hom) :
(AddMonoidAlgebra.liftNC f g) 1 = 1
instance AddMonoidAlgebra.nonUnitalSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
instance AddMonoidAlgebra.nonAssocSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
theorem AddMonoidAlgebra.natCast_def {k : Type u₁} {G : Type u₂} [] [] (n : ) :
n =
theorem AddMonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [] [] (n : ) :
n =

Alias of AddMonoidAlgebra.natCast_def.

#### Semiring structure #

instance AddMonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] :
Equations
instance AddMonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
def AddMonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] (f : k →+* R) (g : ) (h_comm : ∀ (x : k) (y : ), Commute (f x) (g y)) :

liftNC as a RingHom, for when f and g commute

Equations
Instances For
instance AddMonoidAlgebra.nonUnitalCommSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
instance AddMonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [] [] [] :
Equations
• =

#### Derived instances #

instance AddMonoidAlgebra.commSemiring {k : Type u₁} {G : Type u₂} [] [] :
Equations
instance AddMonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [] [] :
Equations
instance AddMonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :
Equations
instance AddMonoidAlgebra.nonUnitalNonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [Add G] :
Equations
instance AddMonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [] :
Equations
instance AddMonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [] :
Equations
theorem AddMonoidAlgebra.intCast_def {k : Type u₁} {G : Type u₂} [Ring k] [] (z : ) :
z =
theorem AddMonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [] (z : ) :
z =

Alias of AddMonoidAlgebra.intCast_def.

instance AddMonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [] :
Equations
instance AddMonoidAlgebra.nonUnitalCommRing {k : Type u₁} {G : Type u₂} [] [] :
Equations
instance AddMonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [] [] :
Equations
instance AddMonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] :
Equations
instance AddMonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] :
Equations
instance AddMonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] [] :
Equations
• =
instance AddMonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [Module R k] :
Equations
instance AddMonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [] [] [] [SMul R S] [] :
Equations
• =
instance AddMonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [] [] [] [] :
Equations
• =
instance AddMonoidAlgebra.isCentralScalar {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [] [] :
Equations
• =

It is hard to state the equivalent of DistribMulAction G k[G] because we've never discussed actions of additive groups.

theorem AddMonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [] [] [Add G] (f : ) (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.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [] [Add G] (f : ) (g : ) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p s p.1 + p.2 = x) :
(f * g) x = ps, f p.1 * g p.2
theorem AddMonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [] [Add G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} :
* = AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
theorem AddMonoidAlgebra.single_commute_single {k : Type u₁} {G : Type u₂} [] [Add G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) :
theorem AddMonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [] [] {a : G} {b : k} (n : ) :
@[simp]
theorem AddMonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [] [Zero α] [Zero α₂] {F : Type u_6} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) :
= 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} [] [Add α] [Add α₂] {F : Type u_6} [FunLike F α α₂] [AddHomClass F α α₂] (f : F) (x : ) (y : ) :

Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

@[simp]
theorem AddMonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [] [Add G] (a : ) :
a =
def AddMonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [] [Add G] :

Equations
• = { toFun := fun (a : ) => , map_mul' := }
Instances For
def AddMonoidAlgebra.of (k : Type u₁) (G : Type u₂) [] [] :

Embedding of a magma with zero into its magma algebra.

Equations
• = { toFun := fun (a : ) => , map_one' := , map_mul' := }
Instances For
def AddMonoidAlgebra.of' (k : Type u₁) (G : Type u₂) [] :
G

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

Equations
Instances For
@[simp]
theorem AddMonoidAlgebra.of_apply {k : Type u₁} {G : Type u₂} [] [] (a : ) :
@[simp]
theorem AddMonoidAlgebra.of'_apply {k : Type u₁} {G : Type u₂} [] (a : G) :
theorem AddMonoidAlgebra.of'_eq_of {k : Type u₁} {G : Type u₂} [] [] (a : G) :
theorem AddMonoidAlgebra.of_injective {k : Type u₁} {G : Type u₂} [] [] [] :
theorem AddMonoidAlgebra.of'_commute {k : Type u₁} {G : Type u₂} [] [] {a : G} (h : ∀ (a' : G), AddCommute a a') (f : ) :
@[simp]
theorem AddMonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [] [] (a : ) :
def AddMonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [] [] :

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 : ) => AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1, map_one' := , map_mul' := }
Instances For
theorem AddMonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [] [Add G] (f : ) (r : k) (x : G) (y : G) (z : G) (H : ∀ (a : G), a + x = z a = y) :
(f * ) z = f y * r
theorem AddMonoidAlgebra.mul_single_zero_apply {k : Type u₁} {G : Type u₂} [] [] (f : ) (r : k) (x : G) :
(f * ) x = f x * r
theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [] [Add G] (r : k) {g : G} {g' : G} (x : ) (h : ¬∃ (d : G), g' = d + g) :
(x * ) g' = 0
theorem AddMonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [] [Add G] (f : ) (r : k) (x : G) (y : G) (z : G) (H : ∀ (a : G), x + a = y a = z) :
( * f) y = r * f z
theorem AddMonoidAlgebra.single_zero_mul_apply {k : Type u₁} {G : Type u₂} [] [] (f : ) (r : k) (x : G) :
( * f) x = r * f x
theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [] [Add G] (r : k) {g : G} {g' : G} (x : ) (h : ¬∃ (d : G), g' = g + d) :
( * x) g' = 0
theorem AddMonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [] [] (f : ) (r : k) (x : G) (y : G) :
(f * ) y = f (y - x) * r
theorem AddMonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [] [] (r : k) (x : G) (f : ) (y : G) :
( * f) y = r * f (-x + y)
theorem AddMonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [] {R : Type u_3} [] [] (f : k →+* R) (g : ) (c : k) (φ : ) :
(AddMonoidAlgebra.liftNC f g) (c φ) = f c * (AddMonoidAlgebra.liftNC f g) φ
theorem AddMonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [] [] {p : Prop} (f : ) (hM : ∀ (g : G), p ( (Multiplicative.ofAdd g))) (hadd : ∀ (f g : ), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : ), p fp (r f)) :
p f
@[simp]
theorem AddMonoidAlgebra.mapDomainRingHom_apply {G : Type u₂} (k : Type u_3) [] {H : Type u_4} {F : Type u_5} [] [] [FunLike F G H] [] (f : F) :
∀ (a : G →₀ k), = (↑).toFun a
def AddMonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) [] {H : Type u_4} {F : Type u_5} [] [] [FunLike F G H] [] (f : F) :

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
• = { toFun := (↑).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For

#### 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₂) [] [Add G] :

The equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MonoidAlgebra.toAdditive (k : Type u₁) (G : Type u₂) [] [Mul G] :

The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive

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

#### Non-unital, non-associative algebra structure #

instance AddMonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [] [] [Add G] [] :
Equations
• =
instance AddMonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [] [] [Add 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.

Equations
• =
instance AddMonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [] [] [Add G] [] :
Equations
• =
theorem AddMonoidAlgebra.nonUnitalAlgHom_ext (k : Type u₁) {G : Type u₂} [] [Add G] {A : Type u₃} [] {φ₁ : →ₙₐ[k] A} {φ₂ : →ₙₐ[k] A} (h : ∀ (x : G), φ₁ = φ₂ ) :
φ₁ = φ₂

A non_unital k-algebra homomorphism from k[G] is uniquely defined by its values on the functions single a 1.

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext'_iff {k : Type u₁} {G : Type u₂} [] [Add G] {A : Type u₃} [] {φ₁ : →ₙₐ[k] A} {φ₂ : →ₙₐ[k] A} :
φ₁ = φ₂ φ₁.toMulHom.comp = φ₂.toMulHom.comp
theorem AddMonoidAlgebra.nonUnitalAlgHom_ext' (k : Type u₁) {G : Type u₂} [] [Add G] {A : Type u₃} [] {φ₁ : →ₙₐ[k] A} {φ₂ : →ₙₐ[k] A} (h : φ₁.toMulHom.comp = φ₂.toMulHom.comp ) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

@[simp]
theorem AddMonoidAlgebra.liftMagma_symm_apply (k : Type u₁) {G : Type u₂} [] [Add G] {A : Type u₃} [Module k A] [] [] (F : →ₙₐ[k] A) :
.symm F = F.toMulHom.comp
@[simp]
theorem AddMonoidAlgebra.liftMagma_apply_apply (k : Type u₁) {G : Type u₂} [] [Add G] {A : Type u₃} [Module k A] [] [] (f : ) (a : ) :
( f) a = Finsupp.sum a fun (m : G) (t : k) => t f (Multiplicative.ofAdd m)
def AddMonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [] [Add G] {A : Type u₃} [Module k A] [] [] :

The functor G ↦ k[G], from the category of magmas to the category of non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other direction.

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

#### Algebra structure #

@[simp]
theorem AddMonoidAlgebra.singleZeroRingHom_apply {k : Type u₁} {G : Type u₂} [] [] :
∀ (a : k), AddMonoidAlgebra.singleZeroRingHom a = (↑).toFun a
def AddMonoidAlgebra.singleZeroRingHom {k : Type u₁} {G : Type u₂} [] [] :

Finsupp.single 0 as a RingHom

Equations
• AddMonoidAlgebra.singleZeroRingHom = { toFun := (↑).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
theorem AddMonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [] [] [] {f : →+* R} {g : →+* R} (h₀ : ∀ (b : k), f = g ) (h_of : ∀ (a : G), f = 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.

theorem AddMonoidAlgebra.ringHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_3} [] [] [] {f : →+* R} {g : →+* R} :
theorem AddMonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [] [] [] {f : →+* R} {g : →+* R} (h₁ : f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom) (h_of : (↑f).comp = (↑g).comp ) :
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].

@[simp]
theorem AddMonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [] [] :
∀ (a : (G →₀ k)ᵐᵒᵖ), AddMonoidAlgebra.opRingEquiv a = Finsupp.mapRange MulOpposite.op
@[simp]
theorem AddMonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [] [] :
∀ (a : G →₀ kᵐᵒᵖ), AddMonoidAlgebra.opRingEquiv.symm a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop a)
noncomputable def AddMonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [] [] :

The opposite of an R[I] is ring equivalent to the AddMonoidAlgebra Rᵐᵒᵖ I over the opposite ring, taking elements to their opposite.

Equations
Instances For
theorem AddMonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [] [] (r : k) (x : G) :
theorem AddMonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [] [] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
instance AddMonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [Algebra R k] [] :

The instance Algebra R k[G] whenever we have Algebra R k.

In particular this provides the instance Algebra k k[G].

Equations
@[simp]
theorem AddMonoidAlgebra.singleZeroAlgHom_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [Algebra R k] [] :
∀ (a : k), AddMonoidAlgebra.singleZeroAlgHom a =
def AddMonoidAlgebra.singleZeroAlgHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [Algebra R k] [] :

Finsupp.single 0 as an AlgHom

Equations
Instances For
@[simp]
theorem AddMonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {R : Type u_2} [] [] [Algebra R k] [] :
def AddMonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] {B : Type u_3} [] [Algebra k B] (f : A →ₐ[k] B) (g : ) (h_comm : ∀ (x : A) (y : ), Commute (f x) (g y)) :

liftNCRingHom as an AlgHom, for when f is an AlgHom

Equations
Instances For
theorem AddMonoidAlgebra.algHom_ext {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] ⦃φ₁ : →ₐ[k] A ⦃φ₂ : →ₐ[k] A (h : ∀ (x : G), φ₁ = φ₂ ) :
φ₁ = φ₂

A k-algebra homomorphism from k[G] is uniquely defined by its values on the functions single a 1.

theorem AddMonoidAlgebra.algHom_ext'_iff {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] {φ₁ : →ₐ[k] A} {φ₂ : →ₐ[k] A} :
φ₁ = φ₂ (↑φ₁).comp = (↑φ₂).comp
theorem AddMonoidAlgebra.algHom_ext' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] ⦃φ₁ : →ₐ[k] A ⦃φ₂ : →ₐ[k] A (h : (↑φ₁).comp = (↑φ₂).comp ) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

def AddMonoidAlgebra.lift (k : Type u₁) (G : Type u₂) [] [] (A : Type u₃) [] [Algebra k A] :
( →* A) ( →ₐ[k] A)

Any monoid homomorphism G →* A can be lifted to an algebra homomorphism k[G] →ₐ[k] A.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : ) (f : ) :
( F) f = Finsupp.sum f fun (a : G) (b : k) => (algebraMap k A) b * F (Multiplicative.ofAdd a)
theorem AddMonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : ) (f : ) :
( F) f = Finsupp.sum f fun (a : G) (b : k) => b F (Multiplicative.ofAdd a)
theorem AddMonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : ) :
( F) = (AddMonoidAlgebra.liftNC (algebraMap k A) F)
@[simp]
theorem AddMonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : →ₐ[k] A) (x : ) :
theorem AddMonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : ) (x : ) :
( F) ( x) = F x
@[simp]
theorem AddMonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : ) (a : G) (b : k) :
( F) = b F (Multiplicative.ofAdd a)
theorem AddMonoidAlgebra.lift_of' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : ) (x : G) :
theorem AddMonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : →ₐ[k] A) :
F = ((↑F).comp )
theorem AddMonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] (F : →ₐ[k] A) (f : ) :
F f = Finsupp.sum f fun (a : G) (b : k) => b F

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

theorem AddMonoidAlgebra.algHom_ext_iff {k : Type u₁} {G : Type u₂} [] [] {A : Type u₃} [] [Algebra k A] {φ₁ : →ₐ[k] A} {φ₂ : →ₐ[k] A} :
(∀ (x : G), φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) φ₁ = φ₂
theorem AddMonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [] [] {s : } {a : ιG} {b : ιk} :
is, AddMonoidAlgebra.single (a i) (b i) = AddMonoidAlgebra.single (∑ is, a i) (∏ is, b i)
theorem AddMonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} (A : Type u_3) {H : Type u_4} {F : Type u_5} [] [] [Algebra k A] [] [] [FunLike F G H] [] (f : F) (r : k) :
@[simp]
theorem AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_3) (A : Type u_4) [] [] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) :
∀ (a : G →₀ A), = (↑).toFun a
def AddMonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_3) (A : Type u_4) [] [] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) :

If f : G → H is a homomorphism between two additive magmas, then Finsupp.mapDomain f is a non-unital algebra homomorphism between their additive magma algebras.

Equations
• = { toFun := (↑).toFun, map_smul' := , map_zero' := , map_add' := , map_mul' := }
Instances For
@[simp]
theorem AddMonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} (k : Type u_3) (A : Type u_4) [] [] [Algebra k A] [] {H : Type u_5} {F : Type u_6} [] [FunLike F G H] [] (f : F) :
∀ (a : G →₀ A), a = Finsupp.mapDomain (⇑f) a
def AddMonoidAlgebra.mapDomainAlgHom {G : Type u₂} (k : Type u_3) (A : Type u_4) [] [] [Algebra k A] [] {H : Type u_5} {F : Type u_6} [] [FunLike F G H] [] (f : F) :

If f : G → H is an additive homomorphism between two additive monoids, then Finsupp.mapDomain f is an algebra homomorphism between their add monoid algebras.

Equations
• = { toRingHom := , commutes' := }
Instances For
@[simp]
theorem AddMonoidAlgebra.mapDomainAlgHom_id {G : Type u₂} (k : Type u_3) (A : Type u_4) [] [] [Algebra k A] [] :
@[simp]
theorem AddMonoidAlgebra.mapDomainAlgHom_comp (k : Type u_3) (A : Type u_4) {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [] [] [Algebra k A] [] [] [] (f : G₁ →+ G₂) (g : G₂ →+ G₃) :
AddMonoidAlgebra.mapDomainAlgHom k A (g.comp f) = .comp
def AddMonoidAlgebra.domCongr (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [] [] [] [] [Algebra k A] (e : G ≃+ H) :

If e : G ≃* H is a multiplicative equivalence between two monoids, then AddMonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

Equations
Instances For
theorem AddMonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [] [] [] [] [Algebra k A] (e : G ≃+ H) :
=
@[simp]
theorem AddMonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [] [] [] [] [Algebra k A] (e : G ≃+ H) (f : ) (h : H) :
( f) h = f (e.symm h)
@[simp]
theorem AddMonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [] [] [] [] [Algebra k A] (e : G ≃+ H) (f : ) :
( f).support = Finset.map (↑e).toEmbedding f.support
@[simp]
theorem AddMonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [] [] [] [] [Algebra k A] (e : G ≃+ H) (g : G) (a : A) :
@[simp]
theorem AddMonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} (A : Type u_3) [] [] [] [Algebra k A] :
= AlgEquiv.refl
@[simp]
theorem AddMonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [] [] [] [] [Algebra k A] (e : G ≃+ H) :
.symm = AddMonoidAlgebra.domCongr k A e.symm
def AddMonoidAlgebra.toMultiplicativeAlgEquiv (k : Type u₁) (G : Type u₂) {R : Type u_2} [] [] [Algebra R k] [] :

The algebra equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative.

Equations
• = { toEquiv := .toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
def MonoidAlgebra.toAdditiveAlgEquiv (k : Type u₁) (G : Type u₂) {R : Type u_2} [] [] [Algebra R k] [] :

The algebra equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive.

Equations
• = { toEquiv := .toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For