mathlib documentation

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
@[instance]
def monoid_algebra.add_comm_monoid (k : Type u₁) (G : Type u₂) [semiring k] :

@[instance]
def monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :

@[instance]
def monoid_algebra.inhabited (k : Type u₁) (G : Type u₂) [semiring k] :

Semiring structure

@[instance]
def monoid_algebra.has_mul {k : Type u₁} {G : Type u₂} [semiring k] [monoid 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] [monoid G] {f g : monoid_algebra k G} :
f * g = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ * a₂) (b₁ * b₂)))

@[instance]
def monoid_algebra.has_one {k : Type u₁} {G : Type u₂} [semiring k] [monoid 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] [monoid G] :

@[instance]
def monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :

Equations
def monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {R : Type u_1} [semiring R] (f : k →+ R) (g : G →* 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] [monoid G] {R : Type u_1} [semiring R] (f : k →+ R) (g : G →* R) (a : G) (b : k) :

@[simp]
theorem monoid_algebra.lift_nc_one {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) :

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

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
@[instance]
def monoid_algebra.nontrivial {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] [monoid G] :

Derived instances

@[instance]
def monoid_algebra.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :

Equations
@[instance]
def monoid_algebra.add_group {k : Type u₁} {G : Type u₂} [ring k] :

Equations
@[instance]
def monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [semimodule R k] :

Equations
@[instance]
def monoid_algebra.semimodule {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [semimodule R k] :

Equations
theorem monoid_algebra.mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (f g : monoid_algebra k G) (x : G) :
(f * g) x = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (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] [monoid G] (f g : monoid_algebra k 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] [monoid G] (a b : monoid_algebra k G) :
(a * b).support a.support.bind (λ (a₁ : G), b.support.bind (λ (a₂ : G), {a₁ * a₂}))

@[simp]
theorem monoid_algebra.single_mul_single {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {a₁ a₂ : G} {b₁ b₂ : k} :
(finsupp.single a₁ b₁) * finsupp.single a₂ 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 : ) :
finsupp.single a b ^ n = finsupp.single (a ^ n) (b ^ n)

theorem monoid_algebra.map_domain_mul {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [monoid α] [monoid α₂] {x y : monoid_algebra β α} (f : mul_hom α α₂) :

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] [monoid G] :

Embedding of a monoid into its monoid algebra.

Equations
@[simp]
theorem monoid_algebra.of_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (a : G) :

theorem monoid_algebra.of_injective {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] [nontrivial k] :

theorem monoid_algebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (f : monoid_algebra k G) {r : k} {x y z : G} (H : ∀ (a : G), a * x = z a = y) :
(f * finsupp.single x r) z = (f y) * r

theorem monoid_algebra.mul_single_one_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (f : monoid_algebra k G) (r : k) (x : G) :
(f * finsupp.single 1 r) x = (f x) * r

theorem monoid_algebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (f : monoid_algebra k G) {r : k} {x y z : G} (H : ∀ (a : G), x * a = y a = z) :
((finsupp.single x r) * f) y = r * f z

theorem monoid_algebra.single_one_mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (f : monoid_algebra k G) (r : k) (x : G) :
((finsupp.single 1 r) * f) x = r * f x

theorem monoid_algebra.lift_nc_smul {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : monoid_algebra k G) :

Algebra structure

theorem monoid_algebra.single_one_comm {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] (r : k) (f : monoid_algebra k G) :

@[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 : monoid_algebra k G →+* R} (h₁ : ∀ (b : k), f (finsupp.single 1 b) = g (finsupp.single 1 b)) (h_of : ∀ (a : G), f (finsupp.single a 1) = g (finsupp.single a 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 : monoid_algebra k G →+* R} (h₁ : f.comp monoid_algebra.single_one_ring_hom = g.comp monoid_algebra.single_one_ring_hom) (h_of : f.comp (monoid_algebra.of k G) = g.comp (monoid_algebra.of k 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.

We formulate this lemma using equality of homomorphisms so that ext tactic can apply type-specific extensionality lemmas to prove equalities of these homomorphisms.

@[instance]
def monoid_algebra.algebra {k : Type u₁} {G : Type u₂} {A : Type u_1} [comm_semiring k] [semiring A] [algebra k A] [monoid 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} [comm_semiring k] [semiring A] [algebra k A] [monoid G] (ᾰ : A) :

@[simp]
theorem monoid_algebra.coe_algebra_map {k : Type u₁} {G : Type u₂} {A : Type u_1} [comm_semiring k] [semiring A] [algebra k A] [monoid G] :

theorem monoid_algebra.single_eq_algebra_map_mul_of {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] (a : G) (b : k) :

theorem monoid_algebra.single_algebra_map_eq_algebra_map_mul_of {k : Type u₁} {G : Type u₂} {A : Type u_1} [comm_semiring k] [semiring A] [algebra k A] [monoid G] (a : G) (b : k) :

def monoid_algebra.lift_nc_alg_hom {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] {B : Type u_1} [semiring B] [algebra k 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₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] ⦃φ₁ φ₂ : monoid_algebra k G →ₐ[k] A⦄ (h : ∀ (x : G), φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 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₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] ⦃φ₁ φ₂ : monoid_algebra k G →ₐ[k] A⦄ (h : φ₁.comp (monoid_algebra.of k G) = φ₂.comp (monoid_algebra.of k G)) :
φ₁ = φ₂

def monoid_algebra.lift (k : Type u₁) (G : Type u₂) [comm_semiring k] [monoid G] (A : Type u₃) [semiring A] [algebra 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₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : G →* A) (f : monoid_algebra k G) :
((monoid_algebra.lift k G A) F) f = finsupp.sum f (λ (a : G) (b : k), ((algebra_map k A) b) * F a)

theorem monoid_algebra.lift_apply {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : G →* A) (f : monoid_algebra k G) :
((monoid_algebra.lift k G A) F) f = finsupp.sum f (λ (a : G) (b : k), b F a)

theorem monoid_algebra.lift_def {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : G →* A) :

@[simp]
theorem monoid_algebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : monoid_algebra k G →ₐ[k] A) (x : G) :

theorem monoid_algebra.lift_of {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : G →* A) (x : G) :

@[simp]
theorem monoid_algebra.lift_single {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : G →* A) (a : G) (b : k) :

theorem monoid_algebra.lift_unique' {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : monoid_algebra k G →ₐ[k] A) :

theorem monoid_algebra.lift_unique {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : monoid_algebra k G →ₐ[k] A) (f : monoid_algebra k G) :
F f = finsupp.sum f (λ (a : G) (b : k), b F (finsupp.single a 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₂} [group G] [comm_ring k] (V : Type u₃) [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k 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₂} [group G] [comm_ring k] (V : Type u₃) [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] (g : G) (v : V) :

def monoid_algebra.equivariant_of_linear_of_comm {k : Type u₁} {G : Type u₂} [group G] [comm_ring k] {V W : Type u₃} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f (finsupp.single g 1 v) = finsupp.single g 1 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₂} [group G] [comm_ring k] {V W : Type u₃} [add_comm_group V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] [add_comm_group W] [module k W] [module (monoid_algebra k G) W] [is_scalar_tower k (monoid_algebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f (finsupp.single g 1 v) = finsupp.single g 1 f v) (v : V) :

theorem monoid_algebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [comm_semiring k] [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 : monoid_algebra k G) (r : k) (x y : G) :
(f * finsupp.single x 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 : monoid_algebra k G) (y : G) :
((finsupp.single x 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 : monoid_algebra k G) (x : G) :
(f * g) x = finsupp.sum f (λ (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 : monoid_algebra k G) (x : G) :
(f * g) x = finsupp.sum g (λ (a : G) (b : k), (f (x * a⁻¹)) * b)

Additive monoids

@[instance]
def add_monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :

@[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
@[instance]
def add_monoid_algebra.add_comm_monoid (k : Type u₁) (G : Type u₂) [semiring k] :

Semiring structure

@[instance]
def add_monoid_algebra.has_mul {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid 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] [add_monoid G] {f g : add_monoid_algebra k G} :
f * g = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ + a₂) (b₁ * b₂)))

@[instance]
def add_monoid_algebra.has_one {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid 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] [add_monoid G] :

def add_monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {R : Type u_1} [semiring R] (f : k →+ R) (g : multiplicative G →* 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] [add_monoid G] {R : Type u_1} [semiring R] (f : k →+ R) (g : multiplicative G →* R) (a : G) (b : k) :

@[simp]
theorem add_monoid_algebra.lift_nc_one {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : multiplicative G →* R) :

theorem add_monoid_algebra.lift_nc_mul {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : multiplicative G →* R) (a b : add_monoid_algebra k G) (h_comm : ∀ {x y : G}, y a.supportcommute (f (b x)) (g (multiplicative.of_add y))) :

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 : multiplicative G →* R) (h_comm : ∀ (x : k) (y : multiplicative G), commute (f x) (g y)) :

lift_nc as a ring_hom, for when f and g commute

Equations
@[instance]
def add_monoid_algebra.nontrivial {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] [add_monoid G] :

Derived instances

@[instance]
def add_monoid_algebra.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :

Equations
@[instance]
def add_monoid_algebra.add_group {k : Type u₁} {G : Type u₂} [ring k] :

Equations
@[instance]
def add_monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [semimodule R k] :

Equations
@[instance]
def add_monoid_algebra.semimodule {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [semimodule R k] :

Equations

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] [add_monoid G] (f g : add_monoid_algebra k G) (x : G) :
(f * g) x = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (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] [add_monoid G] (f g : add_monoid_algebra k 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] [add_monoid G] (a b : add_monoid_algebra k G) :
(a * b).support a.support.bind (λ (a₁ : G), b.support.bind (λ (a₂ : G), {a₁ + a₂}))

theorem add_monoid_algebra.single_mul_single {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {a₁ a₂ : G} {b₁ b₂ : k} :
(finsupp.single a₁ b₁) * finsupp.single a₂ b₂ = finsupp.single (a₁ + a₂) (b₁ * b₂)

theorem add_monoid_algebra.map_domain_mul {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [add_monoid α] [add_monoid α₂] {x y : add_monoid_algebra β α} (f : add_hom α α₂) :

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] [add_monoid G] :

Embedding of a monoid into its monoid algebra.

Equations
@[simp]
theorem add_monoid_algebra.of_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (a : multiplicative G) :

theorem add_monoid_algebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (f : add_monoid_algebra k G) (r : k) (x y z : G) (H : ∀ (a : G), a + x = z a = y) :
(f * finsupp.single x r) z = (f y) * r

theorem add_monoid_algebra.mul_single_zero_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (f : add_monoid_algebra k G) (r : k) (x : G) :
(f * finsupp.single 0 r) x = (f x) * r

theorem add_monoid_algebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (f : add_monoid_algebra k G) (r : k) (x y z : G) (H : ∀ (a : G), x + a = y a = z) :
((finsupp.single x r) * f) y = r * f z

theorem add_monoid_algebra.single_zero_mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (f : add_monoid_algebra k G) (r : k) (x : G) :
((finsupp.single 0 r) * f) x = r * f x

theorem add_monoid_algebra.lift_nc_smul {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {R : Type u_1} [semiring R] (f : k →+* R) (g : multiplicative G →* R) (c : k) (φ : monoid_algebra k G) :

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.

Algebra structure

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 : add_monoid_algebra k G →+* R} (h₀ : ∀ (b : k), f (finsupp.single 0 b) = g (finsupp.single 0 b)) (h_of : ∀ (a : G), f (finsupp.single a 1) = g (finsupp.single a 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]

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.

We formulate this lemma using equality of homomorphisms so that ext tactic can apply type-specific extensionality lemmas to prove equalities of these homomorphisms.

@[instance]
def add_monoid_algebra.algebra {k : Type u₁} {G : Type u₂} {R : Type u_1} [comm_semiring R] [semiring k] [algebra R k] [add_monoid 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
@[simp]
theorem add_monoid_algebra.coe_algebra_map {k : Type u₁} {G : Type u₂} {R : Type u_1} [comm_semiring R] [semiring k] [algebra R k] [add_monoid G] :

def add_monoid_algebra.lift_nc_alg_hom {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] {B : Type u_1} [semiring B] [algebra k B] (f : A →ₐ[k] B) (g : multiplicative G →* B) (h_comm : ∀ (x : A) (y : multiplicative G), 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₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] ⦃φ₁ φ₂ : add_monoid_algebra k G →ₐ[k] A⦄ (h : ∀ (x : G), φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 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₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] ⦃φ₁ φ₂ : add_monoid_algebra k G →ₐ[k] A⦄ (h : φ₁.comp (add_monoid_algebra.of k G) = φ₂.comp (add_monoid_algebra.of k G)) :
φ₁ = φ₂

def add_monoid_algebra.lift (k : Type u₁) (G : Type u₂) [comm_semiring k] [add_monoid G] (A : Type u₃) [semiring A] [algebra 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₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : multiplicative G →* A) (f : monoid_algebra k G) :
((add_monoid_algebra.lift k G A) F) f = finsupp.sum f (λ (a : G) (b : k), ((algebra_map k A) b) * F (multiplicative.of_add a))

theorem add_monoid_algebra.lift_apply {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : multiplicative G →* A) (f : monoid_algebra k G) :
((add_monoid_algebra.lift k G A) F) f = finsupp.sum f (λ (a : G) (b : k), b F (multiplicative.of_add a))

theorem add_monoid_algebra.lift_def {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : multiplicative G →* A) :

@[simp]
theorem add_monoid_algebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : add_monoid_algebra k G →ₐ[k] A) (x : multiplicative G) :

theorem add_monoid_algebra.lift_of {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : multiplicative G →* A) (x : multiplicative G) :

@[simp]
theorem add_monoid_algebra.lift_single {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : multiplicative G →* A) (a : G) (b : k) :

theorem add_monoid_algebra.lift_unique' {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : add_monoid_algebra k G →ₐ[k] A) :

theorem add_monoid_algebra.lift_unique {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] (F : add_monoid_algebra k G →ₐ[k] A) (f : monoid_algebra k G) :
F f = finsupp.sum f (λ (a : G) (b : k), b F (finsupp.single a 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₂} [comm_semiring k] [add_monoid G] {A : Type u₃} [semiring A] [algebra k A] {φ₁ φ₂ : add_monoid_algebra k G →ₐ[k] A} :
(∀ (x : G), φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 1)) φ₁ = φ₂

theorem add_monoid_algebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [comm_semiring k] [add_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)