# mathlibdocumentation

algebra.monoid_algebra

# 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 this file we define monoid_algebra k G := G →₀ k, and add_monoid_algebra 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 α := add_monoid_algebra ℕ α
mv_polynomial σ α := add_monoid_algebra (σ →₀ ℕ) α


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

## 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 add_monoid_algebra k G := monoid_algebra k (multiplicative G), but the definitional equality multiplicative G = G leaks through everywhere, and seems impossible to use.

### Multiplicative monoids #

def monoid_algebra (k : Type u₁) (G : Type u₂) [semiring k] :
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
@[protected, instance]
def monoid_algebra.add_comm_monoid (k : Type u₁) (G : Type u₂) [semiring k] :
@[protected, instance]
def monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :
@[protected, instance]
def monoid_algebra.inhabited (k : Type u₁) (G : Type u₂) [semiring k] :
@[protected, instance]
def monoid_algebra.has_mul {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] :

The product of f g : monoid_algebra 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
theorem monoid_algebra.mul_def {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] {f g : G} :
f * g = (λ (a₁ : G) (b₁ : k), (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ * a₂) (b₁ * b₂)))
@[protected, instance]
def monoid_algebra.distrib {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] :
Equations
@[protected, instance]
def monoid_algebra.mul_zero_class {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] :
Equations
@[protected, instance]
def monoid_algebra.semigroup_with_zero {k : Type u₁} {G : Type u₂} [semiring k] [semigroup G] :
Equations
@[protected, instance]
def monoid_algebra.has_one {k : Type u₁} {G : Type u₂} [semiring k] [has_one G] :

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

Equations
theorem monoid_algebra.one_def {k : Type u₁} {G : Type u₂} [semiring k] [has_one G] :
1 =
@[protected, instance]
def monoid_algebra.mul_zero_one_class {k : Type u₁} {G : Type u₂} [semiring k]  :
Equations
def monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+ R) (g : G →* R) :
→+ R

A non-commutative version of monoid_algebra.lift: given a additive homomorphism f : k →+ R and a multiplicative monoid homomorphism g : G →* R, returns the additive homomorphism from monoid_algebra k G such that lift_nc 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 = algebra_map k R, then the result is an algebra homomorphism called monoid_algebra.lift.

Equations
@[simp]
theorem monoid_algebra.lift_nc_single {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+ R) (g : G →* R) (a : G) (b : k) :
b) = (f b) * g a
@[simp]
theorem monoid_algebra.lift_nc_one {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) :
1 = 1
theorem monoid_algebra.lift_nc_mul {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) (a b : G) (h_comm : ∀ {x y : G}, y a.supportcommute (f (b x)) (g y)) :
(a * b) = ( a) * b

#### Semiring structure #

@[protected, instance]
def monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :
Equations
def monoid_algebra.lift_nc_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), commute (f x) (g y)) :

lift_nc as a ring_hom, for when f x and g y commute

Equations
@[protected, instance]
def monoid_algebra.comm_semiring {k : Type u₁} {G : Type u₂} [comm_monoid G] :
Equations
@[protected, instance]
def monoid_algebra.nontrivial {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] [nonempty G] :

#### Derived instances #

@[protected, instance]
def monoid_algebra.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :
Equations
@[protected, instance]
def monoid_algebra.add_group {k : Type u₁} {G : Type u₂} [ring k] :
Equations
@[protected, instance]
def monoid_algebra.ring {k : Type u₁} {G : Type u₂} [ring k] [monoid G] :
ring G)
Equations
@[protected, instance]
def monoid_algebra.comm_ring {k : Type u₁} {G : Type u₂} [comm_ring k] [comm_monoid G] :
Equations
@[protected, instance]
def monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [ k] :
G)
Equations
@[protected, instance]
def monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [ k] :
G)
Equations
@[protected, instance]
def monoid_algebra.is_scalar_tower {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [semiring k] [ k] [ k] [ S] [ k] :
G)
@[protected, instance]
def monoid_algebra.smul_comm_class {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [semiring k] [ k] [ k] [ k] :
G)
@[protected, instance]
def monoid_algebra.distrib_mul_action {k : Type u₁} {G : Type u₂} [group G] [semiring k] :
G)
Equations
theorem monoid_algebra.mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (f g : G) (x : G) :
(f * g) x = (λ (a₁ : G) (b₁ : k), (λ (a₂ : G) (b₂ : k), ite (a₁ * a₂ = x) (b₁ * b₂) 0))
theorem monoid_algebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (f g : G) (x : G) (s : finset (G × G)) (hs : ∀ {p : G × G}, p s (p.fst) * p.snd = x) :
(f * g) x = ∑ (p : G × G) in s, (f p.fst) * g p.snd
theorem monoid_algebra.support_mul {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (a b : G) :
(a * b).support a.support.bUnion (λ (a₁ : G), b.support.bUnion (λ (a₂ : G), {a₁ * a₂}))
@[simp]
theorem monoid_algebra.single_mul_single {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
b₁) * b₂ = finsupp.single (a₁ * a₂) (b₁ * b₂)
@[simp]
theorem monoid_algebra.single_pow {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {a : G} {b : k} (n : ) :
^ n = finsupp.single (a ^ n) (b ^ n)
theorem monoid_algebra.map_domain_mul {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [has_mul α] [has_mul α₂] {x y : α} (f : α₂) :
(x * y) = x) *

Like finsupp.map_domain_add, but for the convolutive multiplication we define in this file

def monoid_algebra.of (k : Type u₁) (G : Type u₂) [semiring k]  :
G →*

Embedding of a monoid into its monoid algebra.

Equations
@[simp]
theorem monoid_algebra.of_apply {k : Type u₁} {G : Type u₂} [semiring k] (a : G) :
G) a =
theorem monoid_algebra.of_injective {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] :
theorem monoid_algebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (f : G) {r : k} {x y z : G} (H : ∀ (a : G), a * x = z a = y) :
(f * r) z = (f y) * r
theorem monoid_algebra.mul_single_one_apply {k : Type u₁} {G : Type u₂} [semiring k] (f : G) (r : k) (x : G) :
(f * r) x = (f x) * r
theorem monoid_algebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (f : G) {r : k} {x y z : G} (H : ∀ (a : G), x * a = y a = z) :
( r) * f) y = r * f z
theorem monoid_algebra.single_one_mul_apply {k : Type u₁} {G : Type u₂} [semiring k] (f : G) (r : k) (x : G) :
( r) * f) x = r * f x
theorem monoid_algebra.lift_nc_smul {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : G) :
(c φ) = (f c) * φ

#### Algebra structure #

theorem monoid_algebra.single_one_comm {k : Type u₁} {G : Type u₂} (r : k) (f : G) :
r) * f = f *
def monoid_algebra.single_one_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :

finsupp.single 1 as a ring_hom

Equations
@[simp]
theorem monoid_algebra.single_one_ring_hom_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (ᾰ : k) :
theorem monoid_algebra.ring_hom_ext {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [monoid G] [semiring R] {f g : →+* R} (h₁ : ∀ (b : k), f b) = g b)) (h_of : ∀ (a : G), f 1) = g 1)) :
f = g

If two ring homomorphisms from monoid_algebra k G are equal on all single a 1 and single 1 b, then they are equal.

@[ext]
theorem monoid_algebra.ring_hom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [monoid G] [semiring R] {f g : →+* R} (h_of : f.comp G) = g.comp G)) :
f = g

If two ring homomorphisms from monoid_algebra k G are equal on all single a 1 and single 1 b, then they are equal.

@[protected, instance]
def monoid_algebra.algebra {k : Type u₁} {G : Type u₂} {A : Type u_1} [semiring A] [ A] [monoid G] :
G)

The instance algebra k (monoid_algebra A G) whenever we have algebra k A.

In particular this provides the instance algebra k (monoid_algebra k G).

Equations
@[simp]
theorem monoid_algebra.single_one_alg_hom_apply {k : Type u₁} {G : Type u₂} {A : Type u_1} [semiring A] [ A] [monoid G] (ᾰ : A) :
def monoid_algebra.single_one_alg_hom {k : Type u₁} {G : Type u₂} {A : Type u_1} [semiring A] [ A] [monoid G] :

finsupp.single 1 as a alg_hom

Equations
@[simp]
theorem monoid_algebra.coe_algebra_map {k : Type u₁} {G : Type u₂} {A : Type u_1} [semiring A] [ A] [monoid G] :
G)) = A)
theorem monoid_algebra.single_eq_algebra_map_mul_of {k : Type u₁} {G : Type u₂} [monoid G] (a : G) (b : k) :
= ( G)) b) * G) a
theorem monoid_algebra.single_algebra_map_eq_algebra_map_mul_of {k : Type u₁} {G : Type u₂} {A : Type u_1} [semiring A] [ A] [monoid G] (a : G) (b : k) :
( A) b) = ( G)) b) * G) a
theorem monoid_algebra.induction_on {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {p : → Prop} (f : G) (hM : ∀ (g : G), p ( G) g)) (hadd : ∀ (f g : G), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : G), p fp (r f)) :
p f
def monoid_algebra.lift_nc_alg_hom {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] {B : Type u_1} [semiring B] [ B] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ (x : A) (y : G), commute (f x) (g y)) :

lift_nc_ring_hom as a alg_hom, for when f is an alg_hom

Equations
theorem monoid_algebra.alg_hom_ext {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] ⦃φ₁ φ₂ : →ₐ[k] A⦄ (h : ∀ (x : G), φ₁ 1) = φ₂ 1)) :
φ₁ = φ₂

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

@[ext]
theorem monoid_algebra.alg_hom_ext' {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] ⦃φ₁ φ₂ : →ₐ[k] A⦄ (h : φ₁.comp G) = φ₂.comp G)) :
φ₁ = φ₂
def monoid_algebra.lift (k : Type u₁) (G : Type u₂) [monoid G] (A : Type u₃) [semiring A] [ A] :
(G →* A) G →ₐ[k] A)

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

Equations
theorem monoid_algebra.lift_apply' {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : G →* A) (f : G) :
( A) F) f = (λ (a : G) (b : k), ( A) b) * F a)
theorem monoid_algebra.lift_apply {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : G →* A) (f : G) :
( A) F) f = (λ (a : G) (b : k), b F a)
theorem monoid_algebra.lift_def {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : G →* A) :
( A) F) = F)
@[simp]
theorem monoid_algebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : →ₐ[k] A) (x : G) :
( G A).symm) F) x = F 1)
theorem monoid_algebra.lift_of {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : G →* A) (x : G) :
( A) F) ( G) x) = F x
@[simp]
theorem monoid_algebra.lift_single {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : G →* A) (a : G) (b : k) :
( A) F) b) = b F a
theorem monoid_algebra.lift_unique' {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : →ₐ[k] A) :
F = A) (F.comp G))
theorem monoid_algebra.lift_unique {k : Type u₁} {G : Type u₂} [monoid G] {A : Type u₃} [semiring A] [ A] (F : →ₐ[k] A) (f : G) :
F f = (λ (a : G) (b : k), b F 1))

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

def monoid_algebra.group_smul.linear_map (k : Type u₁) {G : Type u₂} [monoid G] (V : Type u₃) [ V] [module G) V] [ G) V] (g : G) :

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

Equations
@[simp]
theorem monoid_algebra.group_smul.linear_map_apply (k : Type u₁) {G : Type u₂} [monoid G] (V : Type u₃) [ V] [module G) V] [ G) V] (g : G) (v : V) :
= v
def monoid_algebra.equivariant_of_linear_of_comm {k : Type u₁} {G : Type u₂} [monoid G] {V W : Type u₃} [ V] [module G) V] [ G) V] [ W] [module G) W] [ G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f 1 v) = f v) :

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

Equations
@[simp]
theorem monoid_algebra.equivariant_of_linear_of_comm_apply {k : Type u₁} {G : Type u₂} [monoid G] {V W : Type u₃} [ V] [module G) V] [ G) V] [ W] [module G) W] [ G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f 1 v) = f v) (v : V) :
theorem monoid_algebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [comm_monoid G] {s : finset ι} {a : ι → G} {b : ι → k} :
∏ (i : ι) in s, finsupp.single (a i) (b i) = finsupp.single (∏ (i : ι) in s, a i) (∏ (i : ι) in s, b i)
@[simp]
theorem monoid_algebra.mul_single_apply {k : Type u₁} {G : Type u₂} [semiring k] [group G] (f : G) (r : k) (x y : G) :
(f * r) y = (f (y * x⁻¹)) * r
@[simp]
theorem monoid_algebra.single_mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [group G] (r : k) (x : G) (f : G) (y : G) :
( r) * f) y = r * f (x⁻¹ * y)
theorem monoid_algebra.mul_apply_left {k : Type u₁} {G : Type u₂} [semiring k] [group G] (f g : G) (x : G) :
(f * g) x = (λ (a : G) (b : k), b * g (a⁻¹ * x))
theorem monoid_algebra.mul_apply_right {k : Type u₁} {G : Type u₂} [semiring k] [group G] (f g : G) (x : G) :
(f * g) x = (λ (a : G) (b : k), (f (x * a⁻¹)) * b)
theorem monoid_algebra.mem_span_support {k : Type u₁} {G : Type u₂} [semiring k] (f : G) :
f ( G) '' (f.support))

An element of monoid_algebra R M is in the subalgebra generated by its support.

@[protected, instance]
def add_monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :
@[protected, instance]
def add_monoid_algebra.inhabited (k : Type u₁) (G : Type u₂) [semiring k] :
def add_monoid_algebra (k : Type u₁) (G : Type u₂) [semiring k] :
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
@[protected, instance]
def add_monoid_algebra.add_comm_monoid (k : Type u₁) (G : Type u₂) [semiring k] :
@[protected, instance]
def add_monoid_algebra.has_mul {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] :

The product of f g : add_monoid_algebra 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
theorem add_monoid_algebra.mul_def {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] {f g : G} :
f * g = (λ (a₁ : G) (b₁ : k), (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ + a₂) (b₁ * b₂)))
@[protected, instance]
def add_monoid_algebra.distrib {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] :
Equations
@[protected, instance]
def add_monoid_algebra.mul_zero_class {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] :
Equations
@[protected, instance]
def add_monoid_algebra.has_one {k : Type u₁} {G : Type u₂} [semiring k] [has_zero G] :

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

Equations
theorem add_monoid_algebra.one_def {k : Type u₁} {G : Type u₂} [semiring k] [has_zero G] :
1 =
@[protected, instance]
def add_monoid_algebra.semigroup_with_zero {k : Type u₁} {G : Type u₂} [semiring k]  :
Equations
@[protected, instance]
def add_monoid_algebra.mul_zero_one_class {k : Type u₁} {G : Type u₂} [semiring k]  :
Equations
def add_monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+ R) (g : →* R) :
→+ R

A non-commutative version of add_monoid_algebra.lift: given a additive homomorphism f : k →+ R and a multiplicative monoid homomorphism g : multiplicative G →* R, returns the additive homomorphism from add_monoid_algebra k G such that lift_nc 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 = algebra_map k R, then the result is an algebra homomorphism called add_monoid_algebra.lift.

Equations
@[simp]
theorem add_monoid_algebra.lift_nc_single {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+ R) (g : →* R) (a : G) (b : k) :
b) = (f b) *
@[simp]
theorem add_monoid_algebra.lift_nc_one {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+* R) (g : →* R) :
1 = 1
theorem add_monoid_algebra.lift_nc_mul {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+* R) (g : →* R) (a b : G) (h_comm : ∀ {x y : G}, y a.supportcommute (f (b x)) (g ) :
(a * b) = ( a) * b

#### Semiring structure #

@[protected, instance]
def add_monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [ k] :
G)
Equations
@[protected, instance]
def add_monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] :
Equations
def add_monoid_algebra.lift_nc_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : →* R) (h_comm : ∀ (x : k) (y : , commute (f x) (g y)) :

lift_nc as a ring_hom, for when f and g commute

Equations
@[protected, instance]
def add_monoid_algebra.comm_semiring {k : Type u₁} {G : Type u₂}  :
Equations
@[protected, instance]
def add_monoid_algebra.nontrivial {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] [nonempty G] :

#### Derived instances #

@[protected, instance]
def add_monoid_algebra.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :
Equations
@[protected, instance]
def add_monoid_algebra.add_group {k : Type u₁} {G : Type u₂} [ring k] :
Equations
@[protected, instance]
def add_monoid_algebra.ring {k : Type u₁} {G : Type u₂} [ring k] [add_monoid G] :
ring G)
Equations
@[protected, instance]
def add_monoid_algebra.comm_ring {k : Type u₁} {G : Type u₂} [comm_ring k]  :
Equations
@[protected, instance]
def add_monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [ k] :
G)
Equations
@[protected, instance]
def add_monoid_algebra.is_scalar_tower {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [semiring k] [ k] [ k] [ S] [ k] :
G)
@[protected, instance]
def add_monoid_algebra.smul_comm_class {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [semiring k] [ k] [ k] [ k] :
G)

It is hard to state the equivalent of distrib_mul_action G (add_monoid_algebra k G) because we've never discussed actions of additive groups.

theorem add_monoid_algebra.mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (f g : G) (x : G) :
(f * g) x = (λ (a₁ : G) (b₁ : k), (λ (a₂ : G) (b₂ : k), ite (a₁ + a₂ = x) (b₁ * b₂) 0))
theorem add_monoid_algebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (f g : G) (x : G) (s : finset (G × G)) (hs : ∀ {p : G × G}, p s p.fst + p.snd = x) :
(f * g) x = ∑ (p : G × G) in s, (f p.fst) * g p.snd
theorem add_monoid_algebra.support_mul {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (a b : G) :
(a * b).support a.support.bUnion (λ (a₁ : G), b.support.bUnion (λ (a₂ : G), {a₁ + a₂}))
theorem add_monoid_algebra.single_mul_single {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] {a₁ a₂ : G} {b₁ b₂ : k} :
b₁) * b₂ = finsupp.single (a₁ + a₂) (b₁ * b₂)
theorem add_monoid_algebra.single_pow {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {a : G} {b : k} (n : ) :
^ n = finsupp.single (n a) (b ^ n)
theorem add_monoid_algebra.map_domain_mul {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [has_add α] [has_add α₂] {x y : α} (f : α₂) :
(x * y) = x) *

Like finsupp.map_domain_add, but for the convolutive multiplication we define in this file

def add_monoid_algebra.of (k : Type u₁) (G : Type u₂) [semiring k]  :

Embedding of a monoid into its monoid algebra.

Equations
def add_monoid_algebra.of' (k : Type u₁) (G : Type u₂) [semiring k] :
G →

Embedding of a monoid into its monoid algebra, having G as source.

Equations
• = λ (a : G),
@[simp]
theorem add_monoid_algebra.of_apply {k : Type u₁} {G : Type u₂} [semiring k] (a : multiplicative G) :
a =
@[simp]
theorem add_monoid_algebra.of'_apply {k : Type u₁} {G : Type u₂} [semiring k] (a : G) :
=
theorem add_monoid_algebra.of'_eq_of {k : Type u₁} {G : Type u₂} [semiring k] (a : G) :
= a
theorem add_monoid_algebra.of_injective {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k]  :
theorem add_monoid_algebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (f : G) (r : k) (x y z : G) (H : ∀ (a : G), a + x = z a = y) :
(f * r) z = (f y) * r
theorem add_monoid_algebra.mul_single_zero_apply {k : Type u₁} {G : Type u₂} [semiring k] (f : G) (r : k) (x : G) :
(f * r) x = (f x) * r
theorem add_monoid_algebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (f : G) (r : k) (x y z : G) (H : ∀ (a : G), x + a = y a = z) :
( r) * f) y = r * f z
theorem add_monoid_algebra.single_zero_mul_apply {k : Type u₁} {G : Type u₂} [semiring k] (f : G) (r : k) (x : G) :
( r) * f) x = r * f x
theorem add_monoid_algebra.lift_nc_smul {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [semiring R] (f : k →+* R) (g : →* R) (c : k) (φ : G) :
(c φ) = (f c) * φ
theorem add_monoid_algebra.induction_on {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {p : → Prop} (f : G) (hM : ∀ (g : G), p ( ) (hadd : ∀ (f g : , p fp gp (f + g)) (hsmul : ∀ (r : k) (f : , p fp (r f)) :
p f
theorem add_monoid_algebra.mem_span_support {k : Type u₁} {G : Type u₂} [semiring k] (f : G) :

An element of add_monoid_algebra R M is in the submodule generated by its support.

theorem add_monoid_algebra.mem_span_support' {k : Type u₁} {G : Type u₂} [semiring k] (f : G) :

An element of add_monoid_algebra R M is in the subalgebra generated by its support, using unbundled inclusion.

#### Conversions between add_monoid_algebra and monoid_algebra#

While we were not able to define add_monoid_algebra k G = monoid_algebra k (multiplicative G) due to definitional inconveniences, we can still show the types are isomorphic.

TODO: with the new definitional nsmul, there is a direct equality here, so this paragraph could be improved.

@[protected]
def add_monoid_algebra.to_multiplicative (k : Type u₁) (G : Type u₂) [semiring k] [has_add G] :

The equivalence between add_monoid_algebra and monoid_algebra in terms of multiplicative

Equations
@[protected]
def monoid_algebra.to_additive (k : Type u₁) (G : Type u₂) [semiring k] [has_mul G] :

The equivalence between monoid_algebra and add_monoid_algebra in terms of additive

Equations

#### Algebra structure #

@[simp]
theorem add_monoid_algebra.single_zero_ring_hom_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (ᾰ : k) :
def add_monoid_algebra.single_zero_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] :

finsupp.single 0 as a ring_hom

Equations
theorem add_monoid_algebra.ring_hom_ext {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [add_monoid G] [semiring R] {f g : →+* R} (h₀ : ∀ (b : k), f b) = g b)) (h_of : ∀ (a : G), f 1) = g 1)) :
f = g

If two ring homomorphisms from add_monoid_algebra k G are equal on all single a 1 and single 0 b, then they are equal.

@[ext]
theorem add_monoid_algebra.ring_hom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [add_monoid G] [semiring R] {f g : →+* R} (h_of : f.comp = g.comp ) :
f = g

If two ring homomorphisms from add_monoid_algebra k G are equal on all single a 1 and single 0 b, then they are equal.

@[protected, instance]
def add_monoid_algebra.algebra {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [ k] [add_monoid G] :
G)

The instance algebra R (add_monoid_algebra k G) whenever we have algebra R k.

In particular this provides the instance algebra k (add_monoid_algebra k G).

Equations
def add_monoid_algebra.single_zero_alg_hom {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [ k] [add_monoid G] :

finsupp.single 0 as a alg_hom

Equations
@[simp]
theorem add_monoid_algebra.single_zero_alg_hom_apply {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [ k] [add_monoid G] (ᾰ : k) :
@[simp]
theorem add_monoid_algebra.coe_algebra_map {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [ k] [add_monoid G] :
G)) = k)
def add_monoid_algebra.lift_nc_alg_hom {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] {B : Type u_1} [semiring B] [ B] (f : A →ₐ[k] B) (g : →* B) (h_comm : ∀ (x : A) (y : , commute (f x) (g y)) :

lift_nc_ring_hom as a alg_hom, for when f is an alg_hom

Equations
theorem add_monoid_algebra.alg_hom_ext {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] ⦃φ₁ φ₂ : →ₐ[k] A⦄ (h : ∀ (x : G), φ₁ 1) = φ₂ 1)) :
φ₁ = φ₂

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

@[ext]
theorem add_monoid_algebra.alg_hom_ext' {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] ⦃φ₁ φ₂ : →ₐ[k] A⦄ (h : φ₁.comp = φ₂.comp ) :
φ₁ = φ₂
def add_monoid_algebra.lift (k : Type u₁) (G : Type u₂) [add_monoid G] (A : Type u₃) [semiring A] [ A] :
→* A) →ₐ[k] A)

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

Equations
theorem add_monoid_algebra.lift_apply' {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →* A) (f : G) :
( A) F) f = (λ (a : G) (b : k), ( A) b) * F
theorem add_monoid_algebra.lift_apply {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →* A) (f : G) :
( A) F) f = (λ (a : G) (b : k), b F
theorem add_monoid_algebra.lift_def {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →* A) :
( A) F) = F)
@[simp]
theorem add_monoid_algebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →ₐ[k] A) (x : multiplicative G) :
( A).symm) F) x = F
theorem add_monoid_algebra.lift_of {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →* A) (x : multiplicative G) :
( A) F) ( x) = F x
@[simp]
theorem add_monoid_algebra.lift_single {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →* A) (a : G) (b : k) :
( A) F) b) = b
theorem add_monoid_algebra.lift_unique' {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →ₐ[k] A) :
F = A) (F.comp G))
theorem add_monoid_algebra.lift_unique {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] (F : →ₐ[k] A) (f : G) :
F f = (λ (a : G) (b : k), b F 1))

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

theorem add_monoid_algebra.alg_hom_ext_iff {k : Type u₁} {G : Type u₂} [add_monoid G] {A : Type u₃} [semiring A] [ A] {φ₁ φ₂ : →ₐ[k] A} :
(∀ (x : G), φ₁ 1) = φ₂ 1)) φ₁ = φ₂
theorem add_monoid_algebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} {s : finset ι} {a : ι → G} {b : ι → k} :
∏ (i : ι) in s, finsupp.single (a i) (b i) = finsupp.single (∑ (i : ι) in s, a i) (∏ (i : ι) in s, b i)
def add_monoid_algebra.to_multiplicative_alg_equiv (k : Type u₁) (G : Type u₂) {R : Type u_1} [semiring k] [ k] [add_monoid G] :

The algebra equivalence between add_monoid_algebra and monoid_algebra in terms of multiplicative.

Equations
def monoid_algebra.to_additive_alg_equiv (k : Type u₁) (G : Type u₂) {R : Type u_1} [semiring k] [ k] [monoid G] :

The algebra equivalence between monoid_algebra and add_monoid_algebra in terms of additive.

Equations