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.ring {k : Type u₁} {G : Type u₂} [ring k] [monoid G] :
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
@[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] [semimodule R k] [semimodule S k] [has_scalar R S] [is_scalar_tower R S k] :
@[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] [semimodule R k] [semimodule S k] [smul_comm_class R S k] :
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.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] [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.

See note [partially-applied ext lemmas].

@[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)) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

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₂} [monoid G] [comm_semiring k] (V : Type u₃) [add_comm_monoid V] [semimodule k V] [semimodule (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₂} [monoid G] [comm_semiring k] (V : Type u₃) [add_comm_monoid V] [semimodule k V] [semimodule (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₂} [monoid G] [comm_semiring k] {V W : Type u₃} [add_comm_monoid V] [semimodule k V] [semimodule (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] [add_comm_monoid W] [semimodule k W] [semimodule (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₂} [monoid G] [comm_semiring k] {V W : Type u₃} [add_comm_monoid V] [semimodule k V] [semimodule (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] [add_comm_monoid W] [semimodule k W] [semimodule (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
@[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] [semimodule R k] [semimodule S k] [has_scalar R S] [is_scalar_tower R S k] :
@[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] [semimodule R k] [semimodule S k] [smul_comm_class R S k] :

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.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] [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.

See note [partially-applied ext lemmas].

@[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)) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

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)