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_polynominal σ α := 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.
@[instance]
@[instance]
def
monoid_algebra.inhabited
(k : Type u₁)
(G : Type u₂)
[semiring k] :
inhabited (monoid_algebra k G)
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
- monoid_algebra k G = (G →₀ k)
@[instance]
def
monoid_algebra.has_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid 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
- monoid_algebra.has_mul = {mul := λ (f g : monoid_algebra k G), finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ * a₂) (b₁ * b₂)))}
theorem
monoid_algebra.mul_def
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
{f g : monoid_algebra k G} :
f * g = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ * a₂) (b₁ * b₂)))
theorem
monoid_algebra.mul_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f g : monoid_algebra k G)
(x : G) :
⇑(f * g) x = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), ite (a₁ * a₂ = x) (b₁ * b₂) 0))
@[instance]
def
monoid_algebra.has_one
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid 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
- monoid_algebra.has_one = {one := finsupp.single 1 1}
theorem
monoid_algebra.one_def
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G] :
1 = finsupp.single 1 1
theorem
monoid_algebra.zero_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f : monoid_algebra k G) :
theorem
monoid_algebra.mul_zero
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f : monoid_algebra k G) :
@[instance]
def
monoid_algebra.semiring
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G] :
semiring (monoid_algebra k G)
Equations
- monoid_algebra.semiring = {add := add_comm_monoid.add finsupp.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero finsupp.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul monoid_algebra.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[simp]
theorem
monoid_algebra.single_mul_single
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
{a₁ a₂ : G}
{b₁ b₂ : k} :
finsupp.single a₁ b₁ * finsupp.single a₂ b₂ = finsupp.single (a₁ * a₂) (b₁ * b₂)
@[simp]
theorem
monoid_algebra.single_pow
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
{a : G}
{b : k}
(n : ℕ) :
finsupp.single a b ^ n = finsupp.single (a ^ n) (b ^ n)
def
monoid_algebra.of
(k : Type u₁)
(G : Type u₂)
[semiring k]
[monoid G] :
G →* monoid_algebra k G
Embedding of a monoid into its monoid algebra.
Equations
- monoid_algebra.of k G = {to_fun := λ (a : G), finsupp.single a 1, map_one' := _, map_mul' := _}
@[simp]
theorem
monoid_algebra.of_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(a : G) :
⇑(monoid_algebra.of k G) a = finsupp.single a 1
theorem
monoid_algebra.mul_single_apply_aux
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f : monoid_algebra k G)
{r : k}
{x y z : G} :
theorem
monoid_algebra.mul_single_one_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f : monoid_algebra k G)
(r : k)
(x : G) :
theorem
monoid_algebra.single_mul_apply_aux
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f : monoid_algebra k G)
{r : k}
{x y z : G} :
theorem
monoid_algebra.single_one_mul_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[monoid G]
(f : monoid_algebra k G)
(r : k)
(x : G) :
@[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
- monoid_algebra.comm_semiring = {add := semiring.add monoid_algebra.semiring, add_assoc := _, zero := semiring.zero monoid_algebra.semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul monoid_algebra.semiring, mul_assoc := _, one := semiring.one monoid_algebra.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Equations
@[instance]
def
monoid_algebra.ring
{k : Type u₁}
{G : Type u₂}
[ring k]
[monoid G] :
ring (monoid_algebra k G)
Equations
- monoid_algebra.ring = {add := semiring.add monoid_algebra.semiring, add_assoc := _, zero := semiring.zero monoid_algebra.semiring, zero_add := _, add_zero := _, neg := has_neg.neg monoid_algebra.has_neg, add_left_neg := _, add_comm := _, mul := semiring.mul monoid_algebra.semiring, mul_assoc := _, one := semiring.one monoid_algebra.semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[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
- monoid_algebra.comm_ring = {add := ring.add monoid_algebra.ring, add_assoc := _, zero := ring.zero monoid_algebra.ring, zero_add := _, add_zero := _, neg := ring.neg monoid_algebra.ring, add_left_neg := _, add_comm := _, mul := ring.mul monoid_algebra.ring, mul_assoc := _, one := ring.one monoid_algebra.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
def
monoid_algebra.has_scalar
{k : Type u₁}
{G : Type u₂}
[semiring k] :
has_scalar k (monoid_algebra k G)
Equations
@[instance]
def
monoid_algebra.semimodule
{k : Type u₁}
{G : Type u₂}
[semiring k] :
semimodule k (monoid_algebra k G)
Equations
theorem
monoid_algebra.single_one_comm
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
(r : k)
(f : monoid_algebra k G) :
finsupp.single 1 r * f = f * finsupp.single 1 r
def
monoid_algebra.algebra_map'
{k : Type u₁}
{G : Type u₂}
{A : Type u_1}
[semiring k]
[semiring A]
(f : k →+* A)
[monoid G] :
k →+* monoid_algebra A G
As a preliminary to defining the k-algebra structure on monoid_algebra k G,
we define the underlying ring homomorphism.
In fact, we do this in more generality, providing the ring homomorphism
k →+* monoid_algebra A G given any ring homomorphism k →+* A.
Equations
- monoid_algebra.algebra_map' f = {to_fun := λ (x : k), finsupp.single 1 (⇑f x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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
- monoid_algebra.algebra = {to_has_scalar := finsupp.has_scalar algebra.to_semimodule, to_ring_hom := {to_fun := (monoid_algebra.algebra_map' (algebra_map k A)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[simp]
theorem
monoid_algebra.coe_algebra_map
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G] :
⇑(algebra_map k (monoid_algebra k G)) = finsupp.single 1
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
@[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)
def
monoid_algebra.lift
(k : Type u₁)
(G : Type u₂)
[comm_semiring k]
[monoid G]
(R : Type u₃)
[semiring R]
[algebra k R] :
(G →* R) ≃ (monoid_algebra k G →ₐ[k] R)
Any monoid homomorphism G →* R can be lifted to an algebra homomorphism
monoid_algebra k G →ₐ[k] R.
Equations
- monoid_algebra.lift k G R = {to_fun := λ (F : G →* R), {to_fun := λ (f : monoid_algebra k G), finsupp.sum f (λ (a : G) (b : k), b • ⇑F a), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv_fun := λ (f : monoid_algebra k G →ₐ[k] R), ↑f.comp (monoid_algebra.of k G), left_inv := _, right_inv := _}
theorem
monoid_algebra.lift_apply
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
(F : G →* R)
(f : monoid_algebra k G) :
⇑(⇑(monoid_algebra.lift k G R) F) f = finsupp.sum f (λ (a : G) (b : k), b • ⇑F a)
@[simp]
theorem
monoid_algebra.lift_symm_apply
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
(F : monoid_algebra k G →ₐ[k] R)
(x : G) :
⇑(⇑((monoid_algebra.lift k G R).symm) F) x = ⇑F (finsupp.single x 1)
theorem
monoid_algebra.lift_of
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
(F : G →* R)
(x : G) :
⇑(⇑(monoid_algebra.lift k G R) F) (⇑(monoid_algebra.of k G) x) = ⇑F x
@[simp]
theorem
monoid_algebra.lift_single
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
(F : G →* R)
(a : G)
(b : k) :
⇑(⇑(monoid_algebra.lift k G R) F) (finsupp.single a b) = b • ⇑F a
theorem
monoid_algebra.lift_unique'
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
(F : monoid_algebra k G →ₐ[k] R) :
F = ⇑(monoid_algebra.lift k G R) (↑F.comp (monoid_algebra.of k G))
theorem
monoid_algebra.lift_unique
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
(F : monoid_algebra k G →ₐ[k] R)
(f : monoid_algebra k G) :
⇑F f = finsupp.sum f (λ (a : G) (b : k), b • ⇑F (finsupp.single a 1))
Decomposition of a k-algebra homomorphism from monoid_algebra k G by
its values on F (single a 1).
theorem
monoid_algebra.alg_hom_ext
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[monoid G]
{R : Type u₃}
[semiring R]
[algebra k R]
⦃φ₁ φ₂ : monoid_algebra k G →ₐ[k] R⦄ :
(∀ (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.
def
monoid_algebra.group_smul.linear_map
(k : Type u₁)
{G : Type u₂}
[group G]
[comm_ring k]
(V : Type u₃)
[add_comm_group V]
[module (monoid_algebra k G) V] :
G → (semimodule.restrict_scalars k (monoid_algebra k G) V →ₗ[k] semimodule.restrict_scalars k (monoid_algebra k G) V)
When V is a k[G]-module, multiplication by a group element g is a k-linear map.
Equations
- monoid_algebra.group_smul.linear_map k V g = {to_fun := λ (v : semimodule.restrict_scalars k (monoid_algebra k G) V), finsupp.single g 1 • v, map_add' := _, map_smul' := _}
@[simp]
theorem
monoid_algebra.group_smul.linear_map_apply
(k : Type u₁)
{G : Type u₂}
[group G]
[comm_ring k]
(V : Type u₃)
[add_comm_group V]
[module (monoid_algebra k G) V]
(g : G)
(v : V) :
⇑(monoid_algebra.group_smul.linear_map k V g) v = finsupp.single g 1 • v
def
monoid_algebra.equivariant_of_linear_of_comm
{k : Type u₁}
{G : Type u₂}
[group G]
[comm_ring k]
{V : Type u₃}
{gV : add_comm_group V}
{mV : module (monoid_algebra k G) V}
{W : Type u₃}
{gW : add_comm_group W}
{mW : module (monoid_algebra k G) W}
(f : semimodule.restrict_scalars k (monoid_algebra k G) V →ₗ[k] semimodule.restrict_scalars k (monoid_algebra k G) W) :
(∀ (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.
@[simp]
theorem
monoid_algebra.equivariant_of_linear_of_comm_apply
{k : Type u₁}
{G : Type u₂}
[group G]
[comm_ring k]
{V : Type u₃}
{gV : add_comm_group V}
{mV : module (monoid_algebra k G) V}
{W : Type u₃}
{gW : add_comm_group W}
{mW : module (monoid_algebra k G) W}
(f : semimodule.restrict_scalars k (monoid_algebra k G) V →ₗ[k] semimodule.restrict_scalars k (monoid_algebra k G) 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
theorem
monoid_algebra.prod_single
{k : Type u₁}
{G : Type u₂}
{ι : Type ui}
[comm_semiring k]
[comm_monoid G]
{s : finset ι}
{a : ι → G}
{b : ι → k} :
s.prod (λ (i : ι), finsupp.single (a i) (b i)) = finsupp.single (s.prod (λ (i : ι), a i)) (s.prod (λ (i : ι), b i))
@[simp]
theorem
monoid_algebra.mul_single_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[group G]
(f : monoid_algebra k G)
(r : k)
(x y : G) :
@[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) :
theorem
monoid_algebra.mul_apply_left
{k : Type u₁}
{G : Type u₂}
[semiring k]
[group G]
(f g : monoid_algebra k G)
(x : G) :
theorem
monoid_algebra.mul_apply_right
{k : Type u₁}
{G : Type u₂}
[semiring k]
[group G]
(f g : monoid_algebra k G)
(x : G) :
@[instance]
@[instance]
def
add_monoid_algebra.inhabited
(k : Type u₁)
(G : Type u₂)
[semiring k] :
inhabited (add_monoid_algebra k G)
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
- add_monoid_algebra k G = (G →₀ k)
@[instance]
def
add_monoid_algebra.has_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid 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
- add_monoid_algebra.has_mul = {mul := λ (f g : add_monoid_algebra k G), finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ + a₂) (b₁ * b₂)))}
theorem
add_monoid_algebra.mul_def
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
{f g : add_monoid_algebra k G} :
f * g = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), finsupp.single (a₁ + a₂) (b₁ * b₂)))
theorem
add_monoid_algebra.mul_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f g : add_monoid_algebra k G)
(x : G) :
⇑(f * g) x = finsupp.sum f (λ (a₁ : G) (b₁ : k), finsupp.sum g (λ (a₂ : G) (b₂ : k), ite (a₁ + a₂ = x) (b₁ * b₂) 0))
theorem
add_monoid_algebra.support_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(a b : add_monoid_algebra k G) :
@[instance]
def
add_monoid_algebra.has_one
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid 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
theorem
add_monoid_algebra.one_def
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G] :
1 = finsupp.single 0 1
theorem
add_monoid_algebra.zero_mul
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f : add_monoid_algebra k G) :
theorem
add_monoid_algebra.mul_zero
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f : add_monoid_algebra k G) :
@[instance]
def
add_monoid_algebra.semiring
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G] :
semiring (add_monoid_algebra k G)
Equations
- add_monoid_algebra.semiring = {add := add_comm_monoid.add finsupp.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero finsupp.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul add_monoid_algebra.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
theorem
add_monoid_algebra.single_mul_single
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
{a₁ a₂ : G}
{b₁ b₂ : k} :
finsupp.single a₁ b₁ * finsupp.single a₂ b₂ = finsupp.single (a₁ + a₂) (b₁ * b₂)
Embedding of a monoid into its monoid algebra.
Equations
- add_monoid_algebra.of k G = {to_fun := λ (a : multiplicative G), finsupp.single a 1, map_one' := _, map_mul' := _}
@[simp]
theorem
add_monoid_algebra.of_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(a : G) :
⇑(add_monoid_algebra.of k G) a = finsupp.single a 1
theorem
add_monoid_algebra.mul_single_apply_aux
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f : add_monoid_algebra k G)
(r : k)
(x y z : G) :
theorem
add_monoid_algebra.mul_single_zero_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f : add_monoid_algebra k G)
(r : k)
(x : G) :
theorem
add_monoid_algebra.single_mul_apply_aux
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f : add_monoid_algebra k G)
(r : k)
(x y z : G) :
theorem
add_monoid_algebra.single_zero_mul_apply
{k : Type u₁}
{G : Type u₂}
[semiring k]
[add_monoid G]
(f : add_monoid_algebra k G)
(r : k)
(x : G) :
@[instance]
def
add_monoid_algebra.comm_semiring
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[add_comm_monoid G] :
Equations
- add_monoid_algebra.comm_semiring = {add := semiring.add add_monoid_algebra.semiring, add_assoc := _, zero := semiring.zero add_monoid_algebra.semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul add_monoid_algebra.semiring, mul_assoc := _, one := semiring.one add_monoid_algebra.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
def
add_monoid_algebra.has_neg
{k : Type u₁}
{G : Type u₂}
[ring k] :
has_neg (add_monoid_algebra k G)
Equations
@[instance]
def
add_monoid_algebra.ring
{k : Type u₁}
{G : Type u₂}
[ring k]
[add_monoid G] :
ring (add_monoid_algebra k G)
Equations
- add_monoid_algebra.ring = {add := semiring.add add_monoid_algebra.semiring, add_assoc := _, zero := semiring.zero add_monoid_algebra.semiring, zero_add := _, add_zero := _, neg := has_neg.neg add_monoid_algebra.has_neg, add_left_neg := _, add_comm := _, mul := semiring.mul add_monoid_algebra.semiring, mul_assoc := _, one := semiring.one add_monoid_algebra.semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[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
- add_monoid_algebra.comm_ring = {add := ring.add add_monoid_algebra.ring, add_assoc := _, zero := ring.zero add_monoid_algebra.ring, zero_add := _, add_zero := _, neg := ring.neg add_monoid_algebra.ring, add_left_neg := _, add_comm := _, mul := ring.mul add_monoid_algebra.ring, mul_assoc := _, one := ring.one add_monoid_algebra.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
def
add_monoid_algebra.has_scalar
{k : Type u₁}
{G : Type u₂}
[semiring k] :
has_scalar k (add_monoid_algebra k G)
Equations
@[instance]
def
add_monoid_algebra.semimodule
{k : Type u₁}
{G : Type u₂}
[semiring k] :
semimodule k (add_monoid_algebra k G)
Equations
def
add_monoid_algebra.algebra_map'
{k : Type u₁}
{G : Type u₂}
{A : Type u_1}
[semiring k]
[semiring A]
(f : k →+* A)
[add_monoid G] :
k →+* add_monoid_algebra A G
As a preliminary to defining the k-algebra structure on add_monoid_algebra k G,
we define the underlying ring homomorphism.
In fact, we do this in more generality, providing the ring homomorphism
k →+* add_monoid_algebra A G given any ring homomorphism k →+* A.
Equations
- add_monoid_algebra.algebra_map' f = {to_fun := λ (x : k), finsupp.single 0 (⇑f x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[instance]
def
add_monoid_algebra.algebra
{k : Type u₁}
{G : Type u₂}
{A : Type u_1}
[comm_semiring k]
[semiring A]
[algebra k A]
[add_monoid G] :
algebra k (add_monoid_algebra A G)
The instance algebra k (add_monoid_algebra A G) whenever we have algebra k A.
In particular this provides the instance algebra k (add_monoid_algebra k G).
Equations
- add_monoid_algebra.algebra = {to_has_scalar := finsupp.has_scalar algebra.to_semimodule, to_ring_hom := {to_fun := (add_monoid_algebra.algebra_map' (algebra_map k A)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[simp]
theorem
add_monoid_algebra.coe_algebra_map
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[add_monoid G] :
⇑(algebra_map k (add_monoid_algebra k G)) = finsupp.single 0
def
add_monoid_algebra.lift
{k : Type u₁}
{G : Type u₂}
[comm_semiring k]
[add_monoid G]
{R : Type u₃}
[semiring R]
[algebra k R] :
(multiplicative G →* R) ≃ (add_monoid_algebra k G →ₐ[k] R)
Any monoid homomorphism multiplicative G →* R can be lifted to an algebra homomorphism
add_monoid_algebra k G →ₐ[k] R.
Equations
- add_monoid_algebra.lift = {to_fun := λ (F : multiplicative G →* R), {to_fun := λ (f : add_monoid_algebra k G), finsupp.sum f (λ (a : G) (b : k), b • ⇑F a), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv_fun := λ (f : add_monoid_algebra k G →ₐ[k] R), ↑↑f.comp (add_monoid_algebra.of k G), left_inv := _, right_inv := _}
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))