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
- MonoidAlgebra.coeFun k G = inferInstanceAs (CoeFun (G →₀ k) fun (x : G →₀ k) => G → k)
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 ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯
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 ⋯
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
This is not an instance as it conflicts with MonoidAlgebra.distribMulAction
when G = kˣ
.
Equations
- MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction
Instances For
Copies of ext
lemmas and bundled single
s from Finsupp
#
As MonoidAlgebra
is a type synonym, ext
will not unfold it to find ext
lemmas.
We need bundled version of Finsupp.single
with the right types to state these lemmas.
It is good practice to have those, regardless of the ext
issue.
A copy of Finsupp.ext
for MonoidAlgebra
.
A copy of Finsupp.singleAddHom
for MonoidAlgebra
.
Equations
Instances For
A copy of Finsupp.addHom_ext'
for MonoidAlgebra
.
A copy of Finsupp.distribMulActionHom_ext'
for MonoidAlgebra
.
A copy of Finsupp.lsingle
for MonoidAlgebra
.
Equations
Instances For
A copy of Finsupp.lhom_ext'
for MonoidAlgebra
.
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
Copy of Finsupp.smul_single'
that avoids the MonoidAlgebra = Finsupp
defeq abuse.
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 #
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.
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
- AddMonoidAlgebra.coeFun k G = inferInstanceAs (CoeFun (G →₀ k) fun (x : G →₀ k) => G → k)
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 ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯
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 ⋯
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
- AddMonoidAlgebra.module = Finsupp.module G k
It is hard to state the equivalent of DistribMulAction G k[G]
because we've never discussed actions of additive groups.
Copies of ext
lemmas and bundled single
s from Finsupp
#
As AddMonoidAlgebra
is a type synonym, ext
will not unfold it to find ext
lemmas.
We need bundled version of Finsupp.single
with the right types to state these lemmas.
It is good practice to have those, regardless of the ext
issue.
A copy of Finsupp.ext
for AddMonoidAlgebra
.
A copy of Finsupp.singleAddHom
for AddMonoidAlgebra
.
Equations
Instances For
A copy of Finsupp.addHom_ext'
for AddMonoidAlgebra
.
A copy of Finsupp.distribMulActionHom_ext'
for AddMonoidAlgebra
.
A copy of Finsupp.lsingle
for AddMonoidAlgebra
.
Equations
Instances For
A copy of Finsupp.lhom_ext'
for AddMonoidAlgebra
.
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
Copy of Finsupp.smul_single'
that avoids the AddMonoidAlgebra = Finsupp
defeq abuse.
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 #
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.
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' := ⋯ }