Monoid algebras #
When the domain of a Finsupp
has a multiplicative or additive structure, we can define
a convolution product. To mathematicians this structure is known as the "monoid algebra",
i.e. the finite formal linear combinations over a given semiring of elements of the monoid.
The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.
In fact the construction of the "monoid algebra" makes sense when G
is not even a monoid, but
merely a magma, i.e., when G
carries a multiplication which is not required to satisfy any
conditions at all. In this case the construction yields a not-necessarily-unital,
not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such
algebras to magmas, and we prove this as MonoidAlgebra.liftMagma
.
In this file we define MonoidAlgebra k G := G →₀ k
, and AddMonoidAlgebra 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 R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)
When the domain is multiplicative, e.g. a group, this will be used to define the group ring.
Notation #
We introduce the notation R[A]
for AddMonoidAlgebra R A
.
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
k[G] := MonoidAlgebra k (Multiplicative G)
, but the definitional equality
Multiplicative G = G
leaks through everywhere, and seems impossible to use.
Multiplicative monoids #
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
- MonoidAlgebra k G = (G →₀ k)
Instances For
Equations
- MonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))
Equations
- MonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))
Equations
- ⋯ = ⋯
Equations
- MonoidAlgebra.coeFun k G = Finsupp.instCoeFun
Equations
- MonoidAlgebra.single a b = Finsupp.single a b
Instances For
Equations
Instances For
A non-commutative version of MonoidAlgebra.lift
: given an additive homomorphism f : k →+ R
and a homomorphism g : G → R
, returns the additive homomorphism from
MonoidAlgebra k G
such that liftNC 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 = algebraMap k R
, then the result is an algebra homomorphism called
MonoidAlgebra.lift
.
Equations
- MonoidAlgebra.liftNC f g = Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g x)).comp f
Instances For
The multiplication in a monoid algebra. We make it irreducible so that Lean doesn't unfold it trying to unify two things that are different.
Equations
- f.mul' g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
Instances For
The product of f g : MonoidAlgebra 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
- MonoidAlgebra.instMul = { mul := MonoidAlgebra.mul' }
Equations
- MonoidAlgebra.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Equations
- MonoidAlgebra.nonUnitalSemiring = NonUnitalSemiring.mk ⋯
The unit of the multiplication is single 1 1
, i.e. the function
that is 1
at 1
and zero elsewhere.
Equations
- MonoidAlgebra.one = { one := MonoidAlgebra.single 1 1 }
Equations
- MonoidAlgebra.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Alias of MonoidAlgebra.natCast_def
.
Semiring structure #
Equations
- MonoidAlgebra.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRec ⋯ ⋯
liftNC
as a RingHom
, for when f x
and g y
commute
Equations
- MonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(MonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- MonoidAlgebra.nonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯
Equations
- ⋯ = ⋯
Derived instances #
Equations
- MonoidAlgebra.commSemiring = CommSemiring.mk ⋯
Equations
- MonoidAlgebra.unique = Finsupp.uniqueOfRight
Equations
- MonoidAlgebra.addCommGroup = Finsupp.instAddCommGroup
Equations
- MonoidAlgebra.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
Equations
- MonoidAlgebra.nonUnitalRing = NonUnitalRing.mk ⋯
Equations
- MonoidAlgebra.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Alias of MonoidAlgebra.intCast_def
.
Equations
- MonoidAlgebra.nonUnitalCommRing = NonUnitalCommRing.mk ⋯
Equations
- MonoidAlgebra.commRing = CommRing.mk ⋯
Equations
- MonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass
Equations
- MonoidAlgebra.distribSMul = Finsupp.distribSMul G k
Equations
- MonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k
Equations
- MonoidAlgebra.module = Finsupp.module G k
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
This is not an instance as it conflicts with MonoidAlgebra.distribMulAction
when G = kˣ
.
Equations
- MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction
Instances For
Like Finsupp.mapDomain_zero
, but for the 1
we define in this file
Like Finsupp.mapDomain_add
, but for the convolutive multiplication we define in this file
The embedding of a magma into its magma algebra.
Equations
- MonoidAlgebra.ofMagma k G = { toFun := fun (a : G) => MonoidAlgebra.single a 1, map_mul' := ⋯ }
Instances For
The embedding of a unital magma into its magma algebra.
Equations
- MonoidAlgebra.of k G = { toFun := fun (a : G) => MonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Finsupp.single
as a MonoidHom
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
- MonoidAlgebra.singleHom = { toFun := fun (a : k × G) => MonoidAlgebra.single a.2 a.1, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Non-unital, non-associative algebra structure #
Equations
- ⋯ = ⋯
Note that if k
is a CommSemiring
then we have SMulCommClass 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.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Finsupp.single 1
as a RingHom
Equations
- MonoidAlgebra.singleOneRingHom = { toFun := (↑(Finsupp.singleAddHom 1)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
If f : G → H
is a multiplicative homomorphism between two monoids, then
Finsupp.mapDomain f
is a ring homomorphism between their monoid algebras.
Equations
- MonoidAlgebra.mapDomainRingHom k f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
If two ring homomorphisms from MonoidAlgebra k G
are equal on all single a 1
and single 1 b
, then they are equal.
If two ring homomorphisms from MonoidAlgebra k G
are equal on all single a 1
and single 1 b
, then they are equal.
See note [partially-applied ext lemmas].
The opposite of a MonoidAlgebra R I
equivalent as a ring to
the MonoidAlgebra Rᵐᵒᵖ Iᵐᵒᵖ
over the opposite ring, taking elements to their opposite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A submodule over k
which is stable under scalar multiplication by elements of G
is a
submodule over MonoidAlgebra k G
Equations
- MonoidAlgebra.submoduleOfSMulMem W h = { carrier := ↑W, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
Additive monoids #
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
- AddMonoidAlgebra k G = (G →₀ k)
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
Equations
- AddMonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))
Equations
- AddMonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))
Equations
- ⋯ = ⋯
Equations
- AddMonoidAlgebra.coeFun k G = Finsupp.instCoeFun
Equations
- AddMonoidAlgebra.single a b = Finsupp.single a b
Instances For
Equations
Instances For
A non-commutative version of AddMonoidAlgebra.lift
: given an additive homomorphism
f : k →+ R
and a map g : Multiplicative G → R
, returns the additive
homomorphism from k[G]
such that liftNC 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 = algebraMap k R
, then the result is an algebra
homomorphism called AddMonoidAlgebra.lift
.
Equations
- AddMonoidAlgebra.liftNC f g = Finsupp.liftAddHom fun (x : G) => (AddMonoidHom.mulRight (g (Multiplicative.ofAdd x))).comp f
Instances For
The product of f g : 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
- AddMonoidAlgebra.hasMul = { mul := fun (f g : AddMonoidAlgebra k G) => MonoidAlgebra.mul' f g }
Equations
- AddMonoidAlgebra.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
The unit of the multiplication is single 0 1
, i.e. the function
that is 1
at 0
and zero elsewhere.
Equations
- AddMonoidAlgebra.one = { one := AddMonoidAlgebra.single 0 1 }
Equations
- AddMonoidAlgebra.nonUnitalSemiring = NonUnitalSemiring.mk ⋯
Equations
- AddMonoidAlgebra.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Alias of AddMonoidAlgebra.natCast_def
.
Semiring structure #
Equations
- AddMonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass
Equations
- AddMonoidAlgebra.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRec ⋯ ⋯
liftNC
as a RingHom
, for when f
and g
commute
Equations
- AddMonoidAlgebra.liftNCRingHom f g h_comm = { toFun := (↑(AddMonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- AddMonoidAlgebra.nonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯
Equations
- ⋯ = ⋯
Derived instances #
Equations
- AddMonoidAlgebra.commSemiring = CommSemiring.mk ⋯
Equations
- AddMonoidAlgebra.unique = Finsupp.uniqueOfRight
Equations
- AddMonoidAlgebra.addCommGroup = Finsupp.instAddCommGroup
Equations
- AddMonoidAlgebra.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
Equations
- AddMonoidAlgebra.nonUnitalRing = NonUnitalRing.mk ⋯
Equations
- AddMonoidAlgebra.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Alias of AddMonoidAlgebra.intCast_def
.
Equations
- AddMonoidAlgebra.nonUnitalCommRing = NonUnitalCommRing.mk ⋯
Equations
- AddMonoidAlgebra.commRing = CommRing.mk ⋯
Equations
- AddMonoidAlgebra.distribSMul = Finsupp.distribSMul G k
Equations
- AddMonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k
Equations
- ⋯ = ⋯
Equations
- AddMonoidAlgebra.module = Finsupp.module G k
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
It is hard to state the equivalent of DistribMulAction G k[G]
because we've never discussed actions of additive groups.
Like Finsupp.mapDomain_zero
, but for the 1
we define in this file
Like Finsupp.mapDomain_add
, but for the convolutive multiplication we define in this file
The embedding of an additive magma into its additive magma algebra.
Equations
- AddMonoidAlgebra.ofMagma k G = { toFun := fun (a : Multiplicative G) => AddMonoidAlgebra.single a 1, map_mul' := ⋯ }
Instances For
Embedding of a magma with zero into its magma algebra.
Equations
- AddMonoidAlgebra.of k G = { toFun := fun (a : Multiplicative G) => AddMonoidAlgebra.single a 1, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Embedding of a magma with zero G
, into its magma algebra, having G
as source.
Equations
- AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1
Instances For
Finsupp.single
as a MonoidHom
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
- AddMonoidAlgebra.singleHom = { toFun := fun (a : k × Multiplicative G) => AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1, map_one' := ⋯, map_mul' := ⋯ }
Instances For
If f : G → H
is an additive homomorphism between two additive monoids, then
Finsupp.mapDomain f
is a ring homomorphism between their add monoid algebras.
Equations
- AddMonoidAlgebra.mapDomainRingHom k f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Conversions between AddMonoidAlgebra
and MonoidAlgebra
#
We have not defined k[G] = MonoidAlgebra 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 construct the ring isomorphisms using RingEquiv.refl _
.
The equivalence between AddMonoidAlgebra
and MonoidAlgebra
in terms of
Multiplicative
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between MonoidAlgebra
and AddMonoidAlgebra
in terms of Additive
Equations
- One or more equations did not get rendered due to their size.
Instances For
Non-unital, non-associative algebra structure #
Equations
- ⋯ = ⋯
Note that if k
is a CommSemiring
then we have SMulCommClass 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.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Algebra structure #
Finsupp.single 0
as a RingHom
Equations
- AddMonoidAlgebra.singleZeroRingHom = { toFun := (↑(Finsupp.singleAddHom 0)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
If two ring homomorphisms from k[G]
are equal on all single a 1
and single 0 b
, then they are equal.
If two ring homomorphisms from k[G]
are equal on all single a 1
and single 0 b
, then they are equal.
See note [partially-applied ext lemmas].
The opposite of an R[I]
is ring equivalent to
the AddMonoidAlgebra Rᵐᵒᵖ I
over the opposite ring, taking elements to their opposite.
Equations
- AddMonoidAlgebra.opRingEquiv = { toEquiv := (MulOpposite.opAddEquiv.symm.trans (Finsupp.mapRange.addEquiv MulOpposite.opAddEquiv)).toEquiv, map_mul' := ⋯, map_add' := ⋯ }