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 #

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

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

Equations
source
theorem monoid_algebra.one_def {k : Type u₁} {G : Type u₂} [semiring k] [has_one G] :
1 = finsupp.single 1 1
source
@[protected, instance]
def monoid_algebra.mul_zero_one_class {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] :
mul_zero_one_class (monoid_algebra k G)
Equations
source
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) :
monoid_algebra k 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
source
@[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) :
⇑(monoid_algebra.lift_nc f g) (finsupp.single a b) = (⇑f b) * ⇑g a
source
@[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) :
⇑(monoid_algebra.lift_nc ↑f g) 1 = 1
source
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.support → commute (⇑f (⇑b x)) (⇑g y)) :
⇑(monoid_algebra.lift_nc ↑f g) (a * b) = (⇑(monoid_algebra.lift_nc ↑f g) a) * ⇑(monoid_algebra.lift_nc ↑f g) b

Semiring structure #

source
@[protected, instance]
def monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :
semiring (monoid_algebra k G)
Equations
source
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)) :
monoid_algebra k G →+* R

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

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

Derived instances #

source
@[protected, instance]
def monoid_algebra.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :
unique (monoid_algebra k G)
Equations
source
@[protected, instance]
def monoid_algebra.add_group {k : Type u₁} {G : Type u₂} [ring k] :
add_group (monoid_algebra k G)
Equations
source
@[protected, instance]
def monoid_algebra.ring {k : Type u₁} {G : Type u₂} [ring k] [monoid G] :
ring (monoid_algebra k G)
Equations
source
@[protected, instance]
def monoid_algebra.comm_ring {k : Type u₁} {G : Type u₂} [comm_ring k] [comm_monoid G] :
comm_ring (monoid_algebra k G)
Equations
source
@[protected, instance]
def monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module R k] :
has_scalar R (monoid_algebra k G)
Equations
source
@[protected, instance]
def monoid_algebra.module {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module R k] :
module R (monoid_algebra k G)
Equations
source
@[protected, instance]
def monoid_algebra.is_scalar_tower {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [semiring k] [module R k] [module S k] [has_scalar R S] [is_scalar_tower R S k] :
is_scalar_tower R S (monoid_algebra k G)
source
@[protected, instance]
def monoid_algebra.smul_comm_class {k : Type u₁} {G : Type u₂} {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] [semiring k] [module R k] [module S k] [smul_comm_class R S k] :
smul_comm_class R S (monoid_algebra k G)
source
@[protected, instance]
def monoid_algebra.distrib_mul_action {k : Type u₁} {G : Type u₂} [group G] [semiring k] :
distrib_mul_action G (monoid_algebra k G)
Equations
source
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))
source
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
source
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₂}))
source
@[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₂)
source
@[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)
source
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 α α₂) :
finsupp.map_domain ⇑f (x * y) = (finsupp.map_domain ⇑f x) * finsupp.map_domain ⇑f y

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

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

Embedding of a monoid into its monoid algebra.

Equations
source
@[simp]
theorem monoid_algebra.of_apply {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (a : G) :
⇑(monoid_algebra.of k G) a = finsupp.single a 1
source
theorem monoid_algebra.of_injective {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] [nontrivial k] :
function.injective ⇑(monoid_algebra.of k G)
source
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
source
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
source
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
source
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
source
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) :
⇑(monoid_algebra.lift_nc ↑f g) (c • φ) = (⇑f c) * ⇑(monoid_algebra.lift_nc ↑f g) φ

Algebra structure #

source
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) :
(finsupp.single 1 r) * f = f * finsupp.single 1 r
source
def monoid_algebra.single_one_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :
k →+* monoid_algebra k G

finsupp.single 1 as a ring_hom

Equations
source
@[simp]
theorem monoid_algebra.single_one_ring_hom_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (ᾰ : k) :
⇑monoid_algebra.single_one_ring_hom ᾰ = (finsupp.single_add_hom 1).to_fun ᾰ
source
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.

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

source
@[protected, 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] :
algebra k (monoid_algebra A 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
source
@[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) :
⇑monoid_algebra.single_one_alg_hom ᾰ = monoid_algebra.single_one_ring_hom.to_fun ᾰ
source
def monoid_algebra.single_one_alg_hom {k : Type u₁} {G : Type u₂} {A : Type u_1} [comm_semiring k] [semiring A] [algebra k A] [monoid G] :
A →ₐ[k] monoid_algebra A G

finsupp.single 1 as a alg_hom

Equations
source
@[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] :
⇑(algebra_map k (monoid_algebra A G)) = finsupp.single 1 ∘ ⇑(algebra_map k A)
source
theorem monoid_algebra.single_eq_algebra_map_mul_of {k : Type u₁} {G : Type u₂} [comm_semiring k] [monoid G] (a : G) (b : k) :
finsupp.single a b = (⇑(algebra_map k (monoid_algebra k G)) b) * ⇑(monoid_algebra.of k G) a
source
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) :
finsupp.single a (⇑(algebra_map k A) b) = (⇑(algebra_map k (monoid_algebra A G)) b) * ⇑(monoid_algebra.of A G) a
source
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
source
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)) :
monoid_algebra A G →ₐ[k] B

lift_nc_ring_hom as a alg_hom, for when f is an alg_hom

Equations
source
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.

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

source
def monoid_algebra.lift (k : Type u₁) (G : Type u₂) [comm_semiring k] [monoid G] (A : Type u₃) [semiring A] [algebra k A] :
(G →* A) ≃ (monoid_algebra k G →ₐ[k] A)

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

Equations
source
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)
source
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)
source
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) :
⇑(⇑(monoid_algebra.lift k G A) F) = ⇑(monoid_algebra.lift_nc ↑(algebra_map k A) F)
source
@[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) :
⇑(⇑((monoid_algebra.lift k G A).symm) F) x = ⇑F (finsupp.single x 1)
source
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) :
⇑(⇑(monoid_algebra.lift k G A) F) (⇑(monoid_algebra.of k G) x) = ⇑F x
source
@[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) :
⇑(⇑(monoid_algebra.lift k G A) F) (finsupp.single a b) = b • ⇑F a
source
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.lift k G A) (↑F.comp (monoid_algebra.of k G))
source
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).

source
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) :
V →ₗ[k] V

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

Equations
source
@[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) :
⇑(monoid_algebra.group_smul.linear_map k V g) v = finsupp.single g 1 • v
source
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) :
V →ₗ[monoid_algebra k G] W

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

Equations
source
@[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) :
⇑(monoid_algebra.equivariant_of_linear_of_comm f h) v = ⇑f v
source
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)
source
@[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
source
@[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)
source
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))
source
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)
source
theorem monoid_algebra.mem_span_support {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (f : monoid_algebra k G) :
f ∈ submodule.span k (⇑(monoid_algebra.of k G) '' ↑(f.support))

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

Additive monoids #

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

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

Equations
source
theorem add_monoid_algebra.one_def {k : Type u₁} {G : Type u₂} [semiring k] [has_zero G] :
1 = finsupp.single 0 1
source
@[protected, instance]
def add_monoid_algebra.semigroup_with_zero {k : Type u₁} {G : Type u₂} [semiring k] [add_semigroup G] :
semigroup_with_zero (add_monoid_algebra k G)
Equations
source
@[protected, instance]
def add_monoid_algebra.mul_zero_one_class {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] :
mul_zero_one_class (add_monoid_algebra k G)
Equations
source
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) :
add_monoid_algebra k 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
source
@[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) :
⇑(add_monoid_algebra.lift_nc f g) (finsupp.single a b) = (⇑f b) * ⇑g (⇑multiplicative.of_add a)
source
@[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) :
⇑(add_monoid_algebra.lift_nc ↑f g) 1 = 1
source
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.support → commute (⇑f (⇑b x)) (⇑g (⇑multiplicative.of_add y))) :
⇑(add_monoid_algebra.lift_nc ↑f g) (a * b) = (⇑(add_monoid_algebra.lift_nc ↑f g) a) * ⇑(add_monoid_algebra.lift_nc ↑f g) b

Semiring structure #

source
@[protected, instance]
def add_monoid_algebra.has_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring R] [semiring k] [module R k] :
has_scalar R (add_monoid_algebra k G)
Equations
source
@[protected, instance]
def add_monoid_algebra.semiring {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] :
semiring (add_monoid_algebra k G)
Equations
source
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)) :
add_monoid_algebra k G →+* R

lift_nc as a ring_hom, for when f and g commute

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

Derived instances #

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

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

source
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))
source
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
source
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₂}))
source
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₂)
source
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)
source
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 α α₂) :
finsupp.map_domain ⇑f (x * y) = (finsupp.map_domain ⇑f x) * finsupp.map_domain ⇑f y

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

source
def add_monoid_algebra.of (k : Type u₁) (G : Type u₂) [semiring k] [add_zero_class G] :
multiplicative G →* add_monoid_algebra k G

Embedding of a monoid into its monoid algebra.

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

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

Equations
source
@[simp]
theorem add_monoid_algebra.of_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] (a : multiplicative G) :
⇑(add_monoid_algebra.of k G) a = finsupp.single (⇑multiplicative.to_add a) 1
source
@[simp]
theorem add_monoid_algebra.of'_apply {k : Type u₁} {G : Type u₂} [semiring k] (a : G) :
add_monoid_algebra.of' k G a = finsupp.single a 1
source
theorem add_monoid_algebra.of'_eq_of {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] (a : G) :
add_monoid_algebra.of' k G a = ⇑(add_monoid_algebra.of k G) a
source
theorem add_monoid_algebra.of_injective {k : Type u₁} {G : Type u₂} [semiring k] [nontrivial k] [add_zero_class G] :
function.injective ⇑(add_monoid_algebra.of k G)
source
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
source
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
source
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
source
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
source
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) :
⇑(add_monoid_algebra.lift_nc ↑f g) (c • φ) = (⇑f c) * ⇑(add_monoid_algebra.lift_nc ↑f g) φ
source
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
source
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) :
f ∈ submodule.span k (⇑(add_monoid_algebra.of k G) '' ↑(f.support))

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

source
theorem add_monoid_algebra.mem_span_support' {k : Type u₁} {G : Type u₂} [semiring k] (f : add_monoid_algebra k G) :
f ∈ submodule.span k (add_monoid_algebra.of' k G '' ↑(f.support))

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

Conversions between add_monoid_algebra and monoid_algebra #

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

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

source
@[protected]
def add_monoid_algebra.to_multiplicative (k : Type u₁) (G : Type u₂) [semiring k] [has_add G] :
add_monoid_algebra k G ≃+* monoid_algebra k (multiplicative G)

The equivalence between add_monoid_algebra and monoid_algebra in terms of multiplicative

Equations
source
@[protected]
def monoid_algebra.to_additive (k : Type u₁) (G : Type u₂) [semiring k] [has_mul G] :
monoid_algebra k G ≃+* add_monoid_algebra k (additive G)

The equivalence between monoid_algebra and add_monoid_algebra in terms of additive

Equations

Algebra structure #

source
@[simp]
theorem add_monoid_algebra.single_zero_ring_hom_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] (ᾰ : k) :
⇑add_monoid_algebra.single_zero_ring_hom ᾰ = (finsupp.single_add_hom 0).to_fun ᾰ
source
def add_monoid_algebra.single_zero_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [add_monoid G] :
k →+* add_monoid_algebra k G

finsupp.single 0 as a ring_hom

Equations
source
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.

source
@[ext]
theorem add_monoid_algebra.ring_hom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [add_monoid G] [semiring R] {f g : add_monoid_algebra k G →+* R} (h₁ : f.comp add_monoid_algebra.single_zero_ring_hom = g.comp add_monoid_algebra.single_zero_ring_hom) (h_of : ↑f.comp (add_monoid_algebra.of k G) = ↑g.comp (add_monoid_algebra.of k G)) :
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.

See note [partially-applied ext lemmas].

source
@[protected, 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] :
algebra R (add_monoid_algebra k 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
source
def add_monoid_algebra.single_zero_alg_hom {k : Type u₁} {G : Type u₂} {R : Type u_1} [comm_semiring R] [semiring k] [algebra R k] [add_monoid G] :
k →ₐ[R] add_monoid_algebra k G

finsupp.single 0 as a alg_hom

Equations
source
@[simp]
theorem add_monoid_algebra.single_zero_alg_hom_apply {k : Type u₁} {G : Type u₂} {R : Type u_1} [comm_semiring R] [semiring k] [algebra R k] [add_monoid G] (ᾰ : k) :
⇑add_monoid_algebra.single_zero_alg_hom ᾰ = add_monoid_algebra.single_zero_ring_hom.to_fun ᾰ
source
@[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] :
⇑(algebra_map R (add_monoid_algebra k G)) = finsupp.single 0 ∘ ⇑(algebra_map R k)
source
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)) :
add_monoid_algebra A G →ₐ[k] B

lift_nc_ring_hom as a alg_hom, for when f is an alg_hom

Equations
source
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.

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

source
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] :
(multiplicative G →* A) ≃ (add_monoid_algebra k G →ₐ[k] A)

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

Equations
source
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))
source
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))
source
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) :
⇑(⇑(add_monoid_algebra.lift k G A) F) = ⇑(add_monoid_algebra.lift_nc ↑(algebra_map k A) F)
source
@[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) :
⇑(⇑((add_monoid_algebra.lift k G A).symm) F) x = ⇑F (finsupp.single (⇑multiplicative.to_add x) 1)
source
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) :
⇑(⇑(add_monoid_algebra.lift k G A) F) (⇑(add_monoid_algebra.of k G) x) = ⇑F x
source
@[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) :
⇑(⇑(add_monoid_algebra.lift k G A) F) (finsupp.single a b) = b • ⇑F (⇑multiplicative.of_add a)
source
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 = ⇑(add_monoid_algebra.lift k G A) (↑F.comp (add_monoid_algebra.of k G))
source
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).

source
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)) ↔ φ₁ = φ₂
source
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)
source
def add_monoid_algebra.to_multiplicative_alg_equiv (k : Type u₁) (G : Type u₂) {R : Type u_1} [comm_semiring R] [semiring k] [algebra R k] [add_monoid G] :
add_monoid_algebra k G ≃ₐ[R] monoid_algebra k (multiplicative G)

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

Equations
source
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] :
monoid_algebra k G ≃ₐ[R] add_monoid_algebra k (additive G)

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

Equations