mathlib3 documentation

algebra.monoid_algebra.basic

Monoid algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[protected, instance]
noncomputable def monoid_algebra.add_comm_monoid (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_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
noncomputable def monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [non_unital_non_assoc_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 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₂} {R : Type u_1} [semiring k] [non_unital_non_assoc_semiring R] (f : k →+ R) (g : G R) (a : G) (b : k) :
@[protected, instance]
noncomputable 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₂)))
theorem monoid_algebra.lift_nc_mul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [has_mul G] [semiring R] {g_hom : Type u_2} [mul_hom_class g_hom G R] (f : k →+* R) (g : g_hom) (a b : monoid_algebra k G) (h_comm : {x y : G}, y a.support commute (f (b x)) (g y)) :
@[protected, instance]
noncomputable 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] :
@[simp]
theorem monoid_algebra.lift_nc_one {k : Type u₁} {G : Type u₂} {R : Type u_1} [non_assoc_semiring R] [semiring k] [has_one G] {g_hom : Type u_2} [one_hom_class g_hom G R] (f : k →+* R) (g : g_hom) :
theorem monoid_algebra.nat_cast_def {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (n : ) :

Semiring structure #

@[protected, instance]
noncomputable def monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :
Equations
noncomputable def monoid_algebra.lift_nc_ring_hom {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [monoid G] [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.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]
noncomputable def monoid_algebra.add_comm_group {k : Type u₁} {G : Type u₂} [ring k] :
Equations
theorem monoid_algebra.int_cast_def {k : Type u₁} {G : Type u₂} [ring k] [mul_one_class G] (z : ) :
@[protected, instance]
noncomputable def monoid_algebra.smul_zero_class {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [smul_zero_class R k] :
Equations
@[protected, instance]
noncomputable def monoid_algebra.distrib_smul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [distrib_smul R k] :
Equations
@[protected, instance]
noncomputable 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
@[protected, instance]
noncomputable def monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module R k] :
Equations
@[protected, instance]
@[protected, instance]
def monoid_algebra.is_scalar_tower {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring k] [smul_zero_class R k] [smul_zero_class S k] [has_smul R S] [is_scalar_tower R S k] :
@[protected, 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] :
@[protected, instance]
theorem monoid_algebra.mul_apply {k : Type u₁} {G : Type u₂} [semiring k] [decidable_eq G] [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 = s.sum (λ (p : G × G), f p.fst * g p.snd)
@[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)
@[simp]
theorem monoid_algebra.map_domain_one {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [has_one α] [has_one α₂] {F : Type u_4} [one_hom_class F α α₂] (f : F) :

Like finsupp.map_domain_zero, but for the 1 we define in this file

theorem monoid_algebra.map_domain_mul {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [has_mul α] [has_mul α₂] {F : Type u_4} [mul_hom_class F α α₂] (f : F) (x y : monoid_algebra β α) :

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

noncomputable 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) :
noncomputable 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.smul_of {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (g : G) (r : k) :
@[simp]
noncomputable def monoid_algebra.single_hom {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] :

finsupp.single as a monoid_hom from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of finsupp.single.

Equations
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.mul_single_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (r : k) {g g' : G} (x : monoid_algebra k G) (h : ¬ (d : G), g' = d * g) :
(x * finsupp.single g r) g' = 0
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.single_mul_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] (r : k) {g g' : G} (x : monoid_algebra k G) (h : ¬ (d : G), g' = g * d) :
(finsupp.single g r * x) g' = 0
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 #

@[protected, instance]
@[protected, instance]

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.

@[protected, instance]
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] {φ₁ φ₂ : monoid_algebra k G →ₙₐ[k] 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.

noncomputable 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 : 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.map_domain_ring_hom_apply {G : Type u₂} (k : Type u_1) {H : Type u_2} {F : Type u_3} [semiring k] [monoid G] [monoid H] [monoid_hom_class F G H] (f : F) (ᾰ : G →₀ k) :
noncomputable def monoid_algebra.map_domain_ring_hom {G : Type u₂} (k : Type u_1) {H : Type u_2} {F : Type u_3} [semiring k] [monoid G] [monoid H] [monoid_hom_class F G H] (f : F) :

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

Equations
theorem monoid_algebra.ring_hom_ext {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [mul_one_class 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]

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

@[protected, instance]
noncomputable 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.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 f p g p (f + g)) (hsmul : (r : k) (f : monoid_algebra k G), p f p (r f)) :
p f
noncomputable 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_2} [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].

noncomputable 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).

noncomputable def monoid_algebra.map_domain_non_unital_alg_hom (k : Type u_1) (A : Type u_2) [comm_semiring k] [semiring A] [algebra k A] {G : Type u_3} {H : Type u_4} {F : Type u_5} [has_mul G] [has_mul H] [mul_hom_class F G H] (f : F) :

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

Equations
@[simp]
theorem monoid_algebra.map_domain_non_unital_alg_hom_apply (k : Type u_1) (A : Type u_2) [comm_semiring k] [semiring A] [algebra k A] {G : Type u_3} {H : Type u_4} {F : Type u_5} [has_mul G] [has_mul H] [mul_hom_class F G H] (f : F) (ᾰ : G →₀ A) :
theorem monoid_algebra.map_domain_algebra_map {G : Type u₂} [monoid G] (k : Type u_1) (A : Type u_2) {H : Type u_3} {F : Type u_4} [comm_semiring k] [semiring A] [algebra k A] [monoid H] [monoid_hom_class F G H] (f : F) (r : k) :
noncomputable def monoid_algebra.map_domain_alg_hom {G : Type u₂} [monoid G] (k : Type u_1) (A : Type u_2) [comm_semiring k] [semiring A] [algebra k A] {H : Type u_3} {F : Type u_4} [monoid H] [monoid_hom_class F G H] (f : F) :

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

Equations
@[simp]
theorem monoid_algebra.map_domain_alg_hom_apply {G : Type u₂} [monoid G] (k : Type u_1) (A : Type u_2) [comm_semiring k] [semiring A] [algebra k A] {H : Type u_3} {F : Type u_4} [monoid H] [monoid_hom_class F G H] (f : F) (ᾰ : monoid_algebra A G) :
noncomputable 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]
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} :
s.prod (λ (i : ι), finsupp.single (a i) (b i)) = finsupp.single (s.prod (λ (i : ι), a i)) (s.prod (λ (i : ι), 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)
def monoid_algebra.submodule_of_smul_mem {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] {V : Type u_2} [add_comm_monoid V] [module k V] [module (monoid_algebra k G) V] [is_scalar_tower k (monoid_algebra k G) V] (W : submodule k V) (h : (g : G) (v : V), v W (monoid_algebra.of k G) g v W) :

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

Equations

Additive monoids #

@[protected, instance]
@[protected, instance]
noncomputable def add_monoid_algebra.add_comm_monoid (k : Type u₁) (G : Type u₂) [semiring k] :
@[protected, instance]
def add_monoid_algebra.has_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :
Equations
noncomputable def add_monoid_algebra.lift_nc {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [non_unital_non_assoc_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 map 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₂} {R : Type u_1} [semiring k] [non_unital_non_assoc_semiring R] (f : k →+ R) (g : multiplicative G R) (a : G) (b : k) :
@[protected, instance]
noncomputable 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₂)))
theorem add_monoid_algebra.lift_nc_mul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [has_add G] [semiring R] {g_hom : Type u_2} [mul_hom_class g_hom (multiplicative G) R] (f : k →+* R) (g : g_hom) (a b : add_monoid_algebra k G) (h_comm : {x y : G}, y a.support commute (f (b x)) (g (multiplicative.of_add y))) :
@[protected, instance]
noncomputable 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] :
@[simp]
theorem add_monoid_algebra.lift_nc_one {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [has_zero G] [non_assoc_semiring R] {g_hom : Type u_2} [one_hom_class g_hom (multiplicative G) R] (f : k →+* R) (g : g_hom) :
theorem add_monoid_algebra.nat_cast_def {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] (n : ) :

Semiring structure #

@[protected, instance]
noncomputable def add_monoid_algebra.smul_zero_class {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [smul_zero_class R k] :
Equations
@[protected, instance]
noncomputable def add_monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] :
Equations
noncomputable def add_monoid_algebra.lift_nc_ring_hom {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [add_monoid G] [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
@[protected, instance]

Derived instances #

@[protected, instance]
Equations
@[protected, instance]
noncomputable def add_monoid_algebra.add_comm_group {k : Type u₁} {G : Type u₂} [ring k] :
Equations
theorem add_monoid_algebra.int_cast_def {k : Type u₁} {G : Type u₂} [ring k] [add_zero_class G] (z : ) :
@[protected, instance]
noncomputable def add_monoid_algebra.distrib_smul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [distrib_smul R k] :
Equations
@[protected, instance]
noncomputable def add_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
@[protected, instance]
@[protected, instance]
noncomputable def add_monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module R k] :
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 k] [smul_zero_class R k] [smul_zero_class S k] [has_smul R S] [is_scalar_tower R S k] :
@[protected, instance]
def add_monoid_algebra.smul_comm_class {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring k] [smul_zero_class R k] [smul_zero_class S k] [smul_comm_class R S k] :
@[protected, instance]

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] [decidable_eq G] [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 = s.sum (λ (p : G × G), f p.fst * g p.snd)
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)
@[simp]
theorem add_monoid_algebra.map_domain_one {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [has_zero α] [has_zero α₂] {F : Type u_4} [zero_hom_class F α α₂] (f : F) :

Like finsupp.map_domain_zero, but for the 1 we define in this file

theorem add_monoid_algebra.map_domain_mul {α : Type u_1} {β : Type u_2} {α₂ : Type u_3} [semiring β] [has_add α] [has_add α₂] {F : Type u_4} [add_hom_class F α α₂] (f : F) (x y : add_monoid_algebra β α) :

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

noncomputable 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
noncomputable 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
noncomputable 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]
theorem add_monoid_algebra.of'_apply {k : Type u₁} {G : Type u₂} [semiring k] (a : G) :
noncomputable def add_monoid_algebra.single_hom {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] :

finsupp.single as a monoid_hom from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of finsupp.single.

Equations
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.mul_single_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (r : k) {g g' : G} (x : add_monoid_algebra k G) (h : ¬ (d : G), g' = d + g) :
(x * finsupp.single g r) g' = 0
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.single_mul_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] (r : k) {g g' : G} (x : add_monoid_algebra k G) (h : ¬ (d : G), g' = g + d) :
(finsupp.single g r * x) g' = 0
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.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 f p g p (f + g)) (hsmul : (r : k) (f : add_monoid_algebra k G), p f p (r f)) :
p f
noncomputable def add_monoid_algebra.map_domain_ring_hom {G : Type u₂} (k : Type u_1) [semiring k] {H : Type u_2} {F : Type u_3} [add_monoid G] [add_monoid H] [add_monoid_hom_class F G H] (f : F) :

If f : G → H is an additive homomorphism between two additive monoids, then finsupp.map_domain f is a ring homomorphism between their add monoid algebras.

Equations

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 #

@[protected, instance]
@[protected, instance]

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.

@[protected, instance]
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] {φ₁ φ₂ : add_monoid_algebra k G →ₙₐ[k] 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.

noncomputable 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

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

@[protected, instance]
noncomputable 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]
noncomputable 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_2} [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].

noncomputable 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_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) (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} :
s.prod (λ (i : ι), finsupp.single (a i) (b i)) = finsupp.single (s.sum (λ (i : ι), a i)) (s.prod (λ (i : ι), b i))
theorem add_monoid_algebra.map_domain_algebra_map {k : Type u₁} {G : Type u₂} {A : Type u_1} {H : Type u_2} {F : Type u_3} [comm_semiring k] [semiring A] [algebra k A] [add_monoid G] [add_monoid H] [add_monoid_hom_class F G H] (f : F) (r : k) :
noncomputable def add_monoid_algebra.map_domain_non_unital_alg_hom (k : Type u_1) (A : Type u_2) [comm_semiring k] [semiring A] [algebra k A] {G : Type u_3} {H : Type u_4} {F : Type u_5} [has_add G] [has_add H] [add_hom_class F G H] (f : F) :

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

Equations
@[simp]
noncomputable def add_monoid_algebra.map_domain_alg_hom {G : Type u₂} (k : Type u_1) (A : Type u_2) [comm_semiring k] [semiring A] [algebra k A] [add_monoid G] {H : Type u_3} {F : Type u_4} [add_monoid H] [add_monoid_hom_class F G H] (f : F) :

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

Equations
@[simp]
noncomputable 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