mathlib documentation

algebra.monoid_algebra.basic

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 monoid_algebra.lift_magma.

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.inhabited (k : Type u₁) (G : Type u₂) [semiring k] :
@[instance]
def monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :
has_coe_to_fun (monoid_algebra k G) (λ (_x : monoid_algebra k G), G → k)
Equations
@[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 : 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] [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] :
def monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class 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] [mul_one_class 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] [mul_one_class 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] [mul_one_class 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)) :

Semiring structure #

@[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
@[instance]
def monoid_algebra.nontrivial {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] [nonempty 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} [monoid R] [semiring k] [distrib_mul_action R k] :
Equations
@[instance]
def monoid_algebra.distrib_mul_action {k : Type u₁} {G : Type u₂} {R : Type u_1} [monoid R] [semiring k] [distrib_mul_action R k] :
Equations
@[instance]
def monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module R k] :
Equations
@[instance]
def monoid_algebra.has_faithful_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_scalar R k] [nonempty G] :
@[instance]
def monoid_algebra.is_scalar_tower {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action 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} [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action S k] [smul_comm_class R S k] :
theorem monoid_algebra.mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [has_mul 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] [has_mul 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] [has_mul 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] [has_mul 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 β] [has_mul α] [has_mul α₂] {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_magma (k : Type u₁) (G : Type u₂) [semiring k] [has_mul G] :

The embedding of a magma into its magma algebra.

Equations
@[simp]
theorem monoid_algebra.of_magma_apply (k : Type u₁) (G : Type u₂) [semiring k] [has_mul G] (a : G) :
def monoid_algebra.of (k : Type u₁) (G : Type u₂) [semiring k] [mul_one_class G] :

The embedding of a unital magma into its magma algebra.

Equations
@[simp]
theorem monoid_algebra.of_apply (k : Type u₁) (G : Type u₂) [semiring k] [mul_one_class G] (a : G) :
theorem monoid_algebra.of_injective {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] [nontrivial k] :
theorem monoid_algebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_mul 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] [mul_one_class G] (f : monoid_algebra k G) (r : k) (x : G) :
(f * finsupp.single 1 r) x = (f x) * r
theorem monoid_algebra.support_mul_single {k : Type u₁} {G : Type u₂} [semiring k] [right_cancel_semigroup G] (f : monoid_algebra k G) (r : k) (hr : ∀ (y : k), y * r = 0 y = 0) (x : G) :
theorem monoid_algebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_mul 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] [mul_one_class 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] [mul_one_class G] {R : Type u_1} [semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : monoid_algebra k G) :

Non-unital, non-associative algebra structure #

@[instance]
def monoid_algebra.is_scalar_tower_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [distrib_mul_action R k] [has_mul G] [is_scalar_tower R k k] :
@[instance]
def monoid_algebra.smul_comm_class_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [distrib_mul_action R k] [has_mul G] [smul_comm_class R k k] :

Note that if k is a comm_semiring then we have smul_comm_class k k k and so we can take R = k in the below. In other words, if the coefficients are commutative amongst themselves, they also commute with the algebra multiplication.

@[instance]
def monoid_algebra.smul_comm_class_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [distrib_mul_action R k] [has_mul G] [smul_comm_class k R k] :
theorem monoid_algebra.non_unital_alg_hom_ext (k : Type u₁) {G : Type u₂} [semiring k] [has_mul G] {A : Type u₃} [non_unital_non_assoc_semiring A] [distrib_mul_action k A] {φ₁ φ₂ : non_unital_alg_hom k (monoid_algebra k G) A} (h : ∀ (x : G), φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 1)) :
φ₁ = φ₂

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

@[ext]
theorem monoid_algebra.non_unital_alg_hom_ext' (k : Type u₁) {G : Type u₂} [semiring k] [has_mul G] {A : Type u₃} [non_unital_non_assoc_semiring A] [distrib_mul_action k A] {φ₁ φ₂ : non_unital_alg_hom k (monoid_algebra k G) A} (h : φ₁.to_mul_hom.comp (monoid_algebra.of_magma k G) = φ₂.to_mul_hom.comp (monoid_algebra.of_magma k G)) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

@[simp]
def monoid_algebra.lift_magma (k : Type u₁) {G : Type u₂} [semiring k] [has_mul G] {A : Type u₃} [non_unital_non_assoc_semiring A] [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] :

The functor G ↦ monoid_algebra 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
@[simp]
theorem monoid_algebra.lift_magma_apply_apply (k : Type u₁) {G : Type u₂} [semiring k] [has_mul G] {A : Type u₃} [non_unital_non_assoc_semiring A] [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] (f : mul_hom G A) (a : monoid_algebra k G) :
((monoid_algebra.lift_magma k) f) a = finsupp.sum a (λ (m : G) (t : k), t f m)

Algebra structure #

theorem monoid_algebra.single_one_comm {k : Type u₁} {G : Type u₂} [comm_semiring k] [mul_one_class 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) :
theorem monoid_algebra.induction_on {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] {p : monoid_algebra k G → Prop} (f : monoid_algebra k G) (hM : ∀ (g : G), p ((monoid_algebra.of k G) g)) (hadd : ∀ (f g : monoid_algebra k G), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : monoid_algebra k G), p fp (r f)) :
p f
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] [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₂} [monoid G] [comm_semiring k] (V : Type u₃) [add_comm_monoid 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₂} [monoid G] [comm_semiring k] {V W : Type u₃} [add_comm_monoid V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] [add_comm_monoid 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₂} [monoid G] [comm_semiring k] {V W : Type u₃} [add_comm_monoid V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] [add_comm_monoid 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)
theorem monoid_algebra.mem_span_support {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (f : monoid_algebra k G) :

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

@[simp]

Additive monoids #

@[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] :
@[instance]
def add_monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :
Equations
@[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 : 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] [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] :
def add_monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class 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_zero_class 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_zero_class 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_zero_class 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))) :

Semiring structure #

@[instance]
def add_monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [monoid R] [semiring k] [distrib_mul_action R k] :
Equations
@[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 : 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] [nonempty 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.ring {k : Type u₁} {G : Type u₂} [ring k] [add_monoid G] :
Equations
@[instance]
def add_monoid_algebra.has_faithful_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_scalar R k] [nonempty G] :
@[instance]
def add_monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module 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} [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action 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} [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action 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] [has_add 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] [has_add 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] [has_add 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] [has_add 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.single_pow {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {a : G} {b : k} (n : ) :
finsupp.single a b ^ 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 : 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_magma (k : Type u₁) (G : Type u₂) [semiring k] [has_add G] :

The embedding of an additive magma into its additive magma algebra.

Equations
@[simp]
theorem add_monoid_algebra.of_magma_apply (k : Type u₁) (G : Type u₂) [semiring k] [has_add G] (a : multiplicative G) :
def add_monoid_algebra.of (k : Type u₁) (G : Type u₂) [semiring k] [add_zero_class G] :

Embedding of a magma with zero into its magma algebra.

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

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

Equations
@[simp]
@[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] [add_zero_class G] (a : G) :
theorem add_monoid_algebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [semiring k] [has_add 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_zero_class 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] [has_add 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_zero_class G] (f : add_monoid_algebra k G) (r : k) (x : G) :
((finsupp.single 0 r) * f) x = r * f x
theorem add_monoid_algebra.mul_single_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_group G] (f : add_monoid_algebra k G) (r : k) (x y : G) :
(f * finsupp.single x r) y = (f (y - x)) * r
theorem add_monoid_algebra.single_mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_group G] (r : k) (x : G) (f : add_monoid_algebra k G) (y : G) :
((finsupp.single x r) * f) y = r * f (-x + y)
theorem add_monoid_algebra.support_mul_single {k : Type u₁} {G : Type u₂} [semiring k] [add_right_cancel_semigroup G] (f : add_monoid_algebra k G) (r : k) (hr : ∀ (y : k), y * r = 0 y = 0) (x : G) :
theorem add_monoid_algebra.lift_nc_smul {k : Type u₁} {G : Type u₂} [semiring k] {R : Type u_1} [add_zero_class G] [semiring R] (f : k →+* R) (g : multiplicative G →* R) (c : k) (φ : monoid_algebra k G) :
theorem add_monoid_algebra.induction_on {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] {p : add_monoid_algebra k G → Prop} (f : add_monoid_algebra k G) (hM : ∀ (g : G), p ((add_monoid_algebra.of k G) (multiplicative.of_add g))) (hadd : ∀ (f g : add_monoid_algebra k G), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : add_monoid_algebra k G), p fp (r f)) :
p f
theorem add_monoid_algebra.mem_span_support {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] (f : add_monoid_algebra k 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 : add_monoid_algebra k 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 #

We have not defined add_monoid_algebra k G = monoid_algebra 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 contruct the ring isomorphisms using ring_equiv.refl _.

Non-unital, non-associative algebra structure #

@[instance]
def add_monoid_algebra.is_scalar_tower_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [distrib_mul_action R k] [has_add G] [is_scalar_tower R k k] :
@[instance]
def add_monoid_algebra.smul_comm_class_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [distrib_mul_action R k] [has_add G] [smul_comm_class R k k] :

Note that if k is a comm_semiring then we have smul_comm_class k k k and so we can take R = k in the below. In other words, if the coefficients are commutative amongst themselves, they also commute with the algebra multiplication.

@[instance]
def add_monoid_algebra.smul_comm_class_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [distrib_mul_action R k] [has_add G] [smul_comm_class k R k] :
theorem add_monoid_algebra.non_unital_alg_hom_ext (k : Type u₁) {G : Type u₂} [semiring k] [has_add G] {A : Type u₃} [non_unital_non_assoc_semiring A] [distrib_mul_action k A] {φ₁ φ₂ : non_unital_alg_hom k (add_monoid_algebra k G) A} (h : ∀ (x : G), φ₁ (finsupp.single x 1) = φ₂ (finsupp.single x 1)) :
φ₁ = φ₂

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

def add_monoid_algebra.lift_magma (k : Type u₁) {G : Type u₂} [semiring k] [has_add G] {A : Type u₃} [non_unital_non_assoc_semiring A] [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] :

The functor G ↦ add_monoid_algebra 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
@[simp]
theorem add_monoid_algebra.lift_magma_apply_apply (k : Type u₁) {G : Type u₂} [semiring k] [has_add G] {A : Type u₃} [non_unital_non_assoc_semiring A] [module k A] [is_scalar_tower k A A] [smul_comm_class k A A] (f : mul_hom (multiplicative G) A) (a : add_monoid_algebra k G) :

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

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

Equations