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 #

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
Instances for monoid_algebra
source
@[protected, instance]
noncomputable 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.inhabited (k : Type u₁) (G : Type u₂) [semiring k] :
inhabited (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) (λ (_x : monoid_algebra k G), G → k)
Equations
source
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) :
monoid_algebra k 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
source
@[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) :
⇑(monoid_algebra.lift_nc f g) (finsupp.single a b) = ⇑f b * g a
source
@[protected, instance]
noncomputable 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]
noncomputable def monoid_algebra.non_unital_non_assoc_semiring {k : Type u₁} {G : Type u₂} [semiring k] [has_mul G] :
non_unital_non_assoc_semiring (monoid_algebra k G)
Equations
source
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)) :
⇑(monoid_algebra.lift_nc ↑f ⇑g) (a * b) = ⇑(monoid_algebra.lift_nc ↑f ⇑g) a * ⇑(monoid_algebra.lift_nc ↑f ⇑g) b
source
@[protected, instance]
noncomputable def monoid_algebra.non_unital_semiring {k : Type u₁} {G : Type u₂} [semiring k] [semigroup G] :
non_unital_semiring (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable 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
@[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) :
⇑(monoid_algebra.lift_nc ↑f ⇑g) 1 = 1
source
@[protected, instance]
noncomputable def monoid_algebra.non_assoc_semiring {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] :
non_assoc_semiring (monoid_algebra k G)
Equations
source
theorem monoid_algebra.nat_cast_def {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (n : ℕ) :
↑n = finsupp.single 1 ↑n

Semiring structure #

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

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

Equations
source
@[protected, instance]
noncomputable def monoid_algebra.non_unital_comm_semiring {k : Type u₁} {G : Type u₂} [comm_semiring k] [comm_semigroup G] :
non_unital_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]
noncomputable 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.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :
unique (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def monoid_algebra.add_comm_group {k : Type u₁} {G : Type u₂} [ring k] :
add_comm_group (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def monoid_algebra.non_unital_non_assoc_ring {k : Type u₁} {G : Type u₂} [ring k] [has_mul G] :
non_unital_non_assoc_ring (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def monoid_algebra.non_unital_ring {k : Type u₁} {G : Type u₂} [ring k] [semigroup G] :
non_unital_ring (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def monoid_algebra.non_assoc_ring {k : Type u₁} {G : Type u₂} [ring k] [mul_one_class G] :
non_assoc_ring (monoid_algebra k G)
Equations
source
theorem monoid_algebra.int_cast_def {k : Type u₁} {G : Type u₂} [ring k] [mul_one_class G] (z : ℤ) :
↑z = finsupp.single 1 ↑z
source
@[protected, instance]
noncomputable def monoid_algebra.ring {k : Type u₁} {G : Type u₂} [ring k] [monoid G] :
ring (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def monoid_algebra.non_unital_comm_ring {k : Type u₁} {G : Type u₂} [comm_ring k] [comm_semigroup G] :
non_unital_comm_ring (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable 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]
noncomputable def monoid_algebra.smul_zero_class {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [smul_zero_class R k] :
smul_zero_class R (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def monoid_algebra.distrib_smul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [distrib_smul R k] :
distrib_smul R (monoid_algebra k G)
Equations
source
@[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] :
distrib_mul_action R (monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable 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.has_faithful_smul {k : Type u₁} {G : Type u₂} {R : Type u_1} [monoid R] [semiring k] [distrib_mul_action R k] [has_faithful_smul R k] [nonempty G] :
has_faithful_smul R (monoid_algebra k G)
source
@[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] :
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} [monoid R] [monoid S] [semiring k] [distrib_mul_action R k] [distrib_mul_action S k] [smul_comm_class R S k] :
smul_comm_class R S (monoid_algebra k G)
source
@[protected, instance]
def monoid_algebra.is_central_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [monoid R] [semiring k] [distrib_mul_action R k] [distrib_mul_action Rᵐᵒᵖ k] [is_central_scalar R k] :
is_central_scalar R (monoid_algebra k G)
source
noncomputable def monoid_algebra.comap_distrib_mul_action_self {k : Type u₁} {G : Type u₂} [group G] [semiring k] :
distrib_mul_action G (monoid_algebra k G)

This is not an instance as it conflicts with monoid_algebra.distrib_mul_action when G = kˣ.

Equations
source
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))
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 = s.sum (λ (p : G × G), ⇑f p.fst * ⇑g p.snd)
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
@[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) :
finsupp.map_domain ⇑f 1 = 1

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

source
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 β α) :
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
noncomputable def monoid_algebra.of_magma (k : Type u₁) (G : Type u₂) [semiring k] [has_mul G] :
G →ₙ* monoid_algebra k G

The embedding of a magma into its magma algebra.

Equations
source
@[simp]
theorem monoid_algebra.of_magma_apply (k : Type u₁) (G : Type u₂) [semiring k] [has_mul G] (a : G) :
⇑(monoid_algebra.of_magma k G) a = finsupp.single a 1
source
noncomputable def monoid_algebra.of (k : Type u₁) (G : Type u₂) [semiring k] [mul_one_class G] :
G →* monoid_algebra k G

The embedding of a unital magma into its magma 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.smul_of {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (g : G) (r : k) :
r • ⇑(monoid_algebra.of k G) g = finsupp.single g r
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
@[simp]
theorem monoid_algebra.single_hom_apply {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] (a : k × G) :
⇑monoid_algebra.single_hom a = finsupp.single a.snd a.fst
source
noncomputable def monoid_algebra.single_hom {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class G] :
k × G →* monoid_algebra k 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
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.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
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.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
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) φ

Non-unital, non-associative algebra structure #

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

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.

source
@[protected, instance]
def monoid_algebra.smul_comm_class_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring k] [distrib_smul R k] [has_mul G] [smul_comm_class k R k] :
smul_comm_class (monoid_algebra k G) R (monoid_algebra k G)
source
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.

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

source
@[simp]
theorem monoid_algebra.lift_magma_symm_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 : monoid_algebra k G →ₙₐ[k] A) :
⇑((monoid_algebra.lift_magma k).symm) F = F.to_mul_hom.comp (monoid_algebra.of_magma k G)
source
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] :
(G →ₙ* A) ≃ (monoid_algebra k G →ₙₐ[k] 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
source
@[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 #

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
noncomputable def monoid_algebra.single_one_ring_hom {k : Type u₁} {G : Type u₂} [semiring k] [mul_one_class 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] [mul_one_class G] (ᾰ : k) :
⇑monoid_algebra.single_one_ring_hom ᾰ = (finsupp.single_add_hom 1).to_fun ᾰ
source
@[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) :
⇑(monoid_algebra.map_domain_ring_hom k f) ᾰ = (finsupp.map_domain.add_monoid_hom ⇑f).to_fun ᾰ
source
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) :
monoid_algebra k G →+* monoid_algebra k H

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

source
@[ext]
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₁ : 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]
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] :
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
noncomputable 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
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)) :
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
noncomputable 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
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) :
monoid_algebra A G →ₙₐ[k] monoid_algebra A H

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
source
@[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) :
⇑(monoid_algebra.map_domain_non_unital_alg_hom k A f) ᾰ = (finsupp.map_domain.add_monoid_hom ⇑f).to_fun ᾰ
source
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) :
finsupp.map_domain ⇑f (⇑(algebra_map k (monoid_algebra A G)) r) = ⇑(algebra_map k (monoid_algebra A H)) r
source
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) :
monoid_algebra A G →ₐ[k] monoid_algebra A H

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
source
@[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) :
⇑(monoid_algebra.map_domain_alg_hom k A f) ᾰ = (monoid_algebra.map_domain_ring_hom A f).to_fun ᾰ
source
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) :
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} :
s.prod (λ (i : ι), finsupp.single (a i) (b i)) = finsupp.single (s.prod (λ (i : ι), a i)) (s.prod (λ (i : ι), 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
@[simp]
theorem monoid_algebra.op_ring_equiv_symm_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (ᾰ : Gᵐᵒᵖ →₀ kᵐᵒᵖ) :
⇑(monoid_algebra.op_ring_equiv.symm) ᾰ = mul_opposite.op (finsupp.map_range mul_opposite.unop _ (finsupp.equiv_map_domain mul_opposite.op_equiv.symm ᾰ))
source
@[protected]
noncomputable def monoid_algebra.op_ring_equiv {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] :
(monoid_algebra k G)ᵐᵒᵖ ≃+* monoid_algebra kᵐᵒᵖ Gᵐᵒᵖ

The opposite of an monoid_algebra R I equivalent as a ring to the monoid_algebra Rᵐᵒᵖ Iᵐᵒᵖ over the opposite ring, taking elements to their opposite.

Equations
source
@[simp]
theorem monoid_algebra.op_ring_equiv_apply {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (ᾰ : (G →₀ k)ᵐᵒᵖ) :
⇑monoid_algebra.op_ring_equiv ᾰ = finsupp.equiv_map_domain mul_opposite.op_equiv (finsupp.map_range mul_opposite.op _ (mul_opposite.unop ᾰ))
source
@[simp]
theorem monoid_algebra.op_ring_equiv_single {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (r : k) (x : G) :
⇑monoid_algebra.op_ring_equiv (mul_opposite.op (finsupp.single x r)) = finsupp.single (mul_opposite.op x) (mul_opposite.op r)
source
@[simp]
theorem monoid_algebra.op_ring_equiv_symm_single {k : Type u₁} {G : Type u₂} [semiring k] [monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
⇑(monoid_algebra.op_ring_equiv.symm) (finsupp.single x r) = mul_opposite.op (finsupp.single (mul_opposite.unop x) (mul_opposite.unop r))
source
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) :
submodule (monoid_algebra k G) V

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 #

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
Instances for add_monoid_algebra
source
@[protected, instance]
noncomputable 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_coe_to_fun (k : Type u₁) (G : Type u₂) [semiring k] :
has_coe_to_fun (add_monoid_algebra k G) (λ (_x : add_monoid_algebra k G), G → k)
Equations
source
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) :
add_monoid_algebra k 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
source
@[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) :
⇑(add_monoid_algebra.lift_nc f g) (finsupp.single a b) = ⇑f b * g (⇑multiplicative.of_add a)
source
@[protected, instance]
noncomputable 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]
noncomputable def add_monoid_algebra.non_unital_non_assoc_semiring {k : Type u₁} {G : Type u₂} [semiring k] [has_add G] :
non_unital_non_assoc_semiring (add_monoid_algebra k G)
Equations
source
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))) :
⇑(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
source
@[protected, instance]
noncomputable 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
@[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) :
⇑(add_monoid_algebra.lift_nc ↑f ⇑g) 1 = 1
source
@[protected, instance]
noncomputable def add_monoid_algebra.non_unital_semiring {k : Type u₁} {G : Type u₂} [semiring k] [add_semigroup G] :
non_unital_semiring (add_monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def add_monoid_algebra.non_assoc_semiring {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] :
non_assoc_semiring (add_monoid_algebra k G)
Equations
source
theorem add_monoid_algebra.nat_cast_def {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] (n : ℕ) :
↑n = finsupp.single 0 ↑n

Semiring structure #

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

lift_nc as a ring_hom, for when f and g commute

Equations
source
@[protected, instance]
noncomputable def add_monoid_algebra.non_unital_comm_semiring {k : Type u₁} {G : Type u₂} [comm_semiring k] [add_comm_semigroup G] :
non_unital_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]
noncomputable 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.unique {k : Type u₁} {G : Type u₂} [semiring k] [subsingleton k] :
unique (add_monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def add_monoid_algebra.add_comm_group {k : Type u₁} {G : Type u₂} [ring k] :
add_comm_group (add_monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def add_monoid_algebra.non_unital_non_assoc_ring {k : Type u₁} {G : Type u₂} [ring k] [has_add G] :
non_unital_non_assoc_ring (add_monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def add_monoid_algebra.non_unital_ring {k : Type u₁} {G : Type u₂} [ring k] [add_semigroup G] :
non_unital_ring (add_monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable def add_monoid_algebra.non_assoc_ring {k : Type u₁} {G : Type u₂} [ring k] [add_zero_class G] :
non_assoc_ring (add_monoid_algebra k G)
Equations
source
theorem add_monoid_algebra.int_cast_def {k : Type u₁} {G : Type u₂} [ring k] [add_zero_class G] (z : ℤ) :
↑z = finsupp.single 0 ↑z
source
@[protected, instance]
noncomputable 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]
noncomputable def add_monoid_algebra.non_unital_comm_ring {k : Type u₁} {G : Type u₂} [comm_ring k] [add_comm_semigroup G] :
non_unital_comm_ring (add_monoid_algebra k G)
Equations
source
@[protected, instance]
noncomputable 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]
noncomputable def add_monoid_algebra.distrib_smul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [distrib_smul R k] :
distrib_smul R (add_monoid_algebra k G)
Equations
source
@[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] :
distrib_mul_action R (add_monoid_algebra k G)
Equations
source
@[protected, instance]
def add_monoid_algebra.has_faithful_smul {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [smul_zero_class R k] [has_faithful_smul R k] [nonempty G] :
has_faithful_smul R (add_monoid_algebra k G)
source
@[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] :
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 k] [smul_zero_class R k] [smul_zero_class S k] [has_smul 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 k] [smul_zero_class R k] [smul_zero_class S k] [smul_comm_class R S k] :
smul_comm_class R S (add_monoid_algebra k G)
source
@[protected, instance]
def add_monoid_algebra.is_central_scalar {k : Type u₁} {G : Type u₂} {R : Type u_1} [semiring k] [smul_zero_class R k] [smul_zero_class Rᵐᵒᵖ k] [is_central_scalar R k] :
is_central_scalar R (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] [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))
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 = s.sum (λ (p : G × G), ⇑f p.fst * ⇑g p.snd)
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
@[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) :
finsupp.map_domain ⇑f 1 = 1

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

source
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 β α) :
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
noncomputable def add_monoid_algebra.of_magma (k : Type u₁) (G : Type u₂) [semiring k] [has_add G] :
multiplicative G →ₙ* add_monoid_algebra k G

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

Equations
source
@[simp]
theorem add_monoid_algebra.of_magma_apply (k : Type u₁) (G : Type u₂) [semiring k] [has_add G] (a : multiplicative G) :
⇑(add_monoid_algebra.of_magma k G) a = finsupp.single a 1
source
noncomputable 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 magma with zero into its magma algebra.

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

Embedding of a magma with zero G, into its magma 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
@[simp]
theorem add_monoid_algebra.single_hom_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] (a : k × multiplicative G) :
⇑add_monoid_algebra.single_hom a = finsupp.single (⇑multiplicative.to_add a.snd) a.fst
source
noncomputable def add_monoid_algebra.single_hom {k : Type u₁} {G : Type u₂} [semiring k] [add_zero_class G] :
k × multiplicative G →* add_monoid_algebra k 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
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.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
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.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
source
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
source
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)
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
@[simp]
theorem add_monoid_algebra.map_domain_ring_hom_apply {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) (ᾰ : G →₀ k) :
⇑(add_monoid_algebra.map_domain_ring_hom k f) ᾰ = (finsupp.map_domain.add_monoid_hom ⇑f).to_fun ᾰ
source
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) :
add_monoid_algebra k G →+* add_monoid_algebra k H

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

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

Non-unital, non-associative algebra structure #

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

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.

source
@[protected, instance]
def add_monoid_algebra.smul_comm_class_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_1} [semiring k] [distrib_smul R k] [has_add G] [smul_comm_class k R k] :
smul_comm_class (add_monoid_algebra k G) R (add_monoid_algebra k G)
source
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.

source
@[ext]
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 : φ₁.to_mul_hom.comp (add_monoid_algebra.of_magma k G) = φ₂.to_mul_hom.comp (add_monoid_algebra.of_magma k G)) :
φ₁ = φ₂

See note [partially-applied ext lemmas].

source
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] :
(multiplicative G →ₙ* A) ≃ (add_monoid_algebra k G →ₙₐ[k] 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
source
@[simp]
theorem add_monoid_algebra.lift_magma_symm_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 : add_monoid_algebra k G →ₙₐ[k] A) :
⇑((add_monoid_algebra.lift_magma k).symm) F = F.to_mul_hom.comp (add_monoid_algebra.of_magma k G)
source
@[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 : multiplicative G →ₙ* A) (a : add_monoid_algebra k G) :
⇑(⇑(add_monoid_algebra.lift_magma k) f) a = finsupp.sum a (λ (m : G) (t : k), t • ⇑f (⇑multiplicative.of_add m))

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
noncomputable 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]
noncomputable def add_monoid_algebra.op_ring_equiv {k : Type u₁} {G : Type u₂} [semiring k] [add_comm_monoid G] :
(add_monoid_algebra k G)ᵐᵒᵖ ≃+* add_monoid_algebra kᵐᵒᵖ G

The opposite of an add_monoid_algebra R I is ring equivalent to the add_monoid_algebra Rᵐᵒᵖ I over the opposite ring, taking elements to their opposite.

Equations
source
@[simp]
theorem add_monoid_algebra.op_ring_equiv_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_comm_monoid G] (ᾰ : (G →₀ k)ᵐᵒᵖ) :
⇑add_monoid_algebra.op_ring_equiv ᾰ = finsupp.map_range mul_opposite.op _ (mul_opposite.unop ᾰ)
source
@[simp]
theorem add_monoid_algebra.op_ring_equiv_symm_apply {k : Type u₁} {G : Type u₂} [semiring k] [add_comm_monoid G] (ᾰ : G →₀ kᵐᵒᵖ) :
⇑(add_monoid_algebra.op_ring_equiv.symm) ᾰ = mul_opposite.op (finsupp.map_range mul_opposite.unop _ ᾰ)
source
@[simp]
theorem add_monoid_algebra.op_ring_equiv_single {k : Type u₁} {G : Type u₂} [semiring k] [add_comm_monoid G] (r : k) (x : G) :
⇑add_monoid_algebra.op_ring_equiv (mul_opposite.op (finsupp.single x r)) = finsupp.single x (mul_opposite.op r)
source
@[simp]
theorem add_monoid_algebra.op_ring_equiv_symm_single {k : Type u₁} {G : Type u₂} [semiring k] [add_comm_monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
⇑(add_monoid_algebra.op_ring_equiv.symm) (finsupp.single x r) = mul_opposite.op (finsupp.single x (mul_opposite.unop r))
source
@[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] :
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
noncomputable 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
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)) :
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
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] :
(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} :
s.prod (λ (i : ι), finsupp.single (a i) (b i)) = finsupp.single (s.sum (λ (i : ι), a i)) (s.prod (λ (i : ι), b i))
source
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) :
finsupp.map_domain ⇑f (⇑(algebra_map k (add_monoid_algebra A G)) r) = ⇑(algebra_map k (add_monoid_algebra A H)) r
source
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) :
add_monoid_algebra A G →ₙₐ[k] add_monoid_algebra A H

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
source
@[simp]
theorem add_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_add G] [has_add H] [add_hom_class F G H] (f : F) (ᾰ : G →₀ A) :
⇑(add_monoid_algebra.map_domain_non_unital_alg_hom k A f) ᾰ = (finsupp.map_domain.add_monoid_hom ⇑f).to_fun ᾰ
source
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) :
add_monoid_algebra A G →ₐ[k] add_monoid_algebra A H

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
source
@[simp]
theorem add_monoid_algebra.map_domain_alg_hom_apply {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) (ᾰ : add_monoid_algebra A G) :
⇑(add_monoid_algebra.map_domain_alg_hom k A f) ᾰ = (add_monoid_algebra.map_domain_ring_hom A f).to_fun ᾰ
source
noncomputable 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
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] :
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