Documentation

Mathlib.Algebra.MonoidAlgebra.Defs

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 #

def MonoidAlgebra (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

MonoidAlgebra k G = (G →₀ k)

Instances For

instance MonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [Semiring k] :

Inhabited (MonoidAlgebra k G)

Equations

MonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))

instance MonoidAlgebra.addCommMonoid (k : Type u₁) (G : Type u₂) [Semiring k] :

AddCommMonoid (MonoidAlgebra k G)

Equations

MonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))

instance MonoidAlgebra.instIsCancelAdd (k : Type u₁) (G : Type u₂) [Semiring k] [IsCancelAdd k] :

IsCancelAdd (MonoidAlgebra k G)

instance MonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] :

CoeFun (MonoidAlgebra k G) fun (x : MonoidAlgebra k G) => G → k

Equations

MonoidAlgebra.coeFun k G = inferInstanceAs (CoeFun (G →₀ k) fun (x : G →₀ k) => G → k)

@[reducible, inline]

abbrev MonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :

MonoidAlgebra k G

Equations

MonoidAlgebra.single a b = Finsupp.single a b

theorem MonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

single a 0 = 0

theorem MonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b₁ b₂ : k) :

single a (b₁ + b₂) = single a b₁ + single a b₂

@[simp]

theorem MonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [Semiring k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) :

Finsupp.sum (single a b) h = h a b

@[simp]

theorem MonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [Semiring k] (f : MonoidAlgebra k G) :

Finsupp.sum f single = f

theorem MonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [Semiring k] {a a' : G} {b : k} [Decidable (a = a')] :

(single a b) a' = if a = a' then b else 0

@[simp]

theorem MonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {b : k} :

single a b = 0 ↔ b = 0

def MonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) :

MonoidAlgebra k G →+ R

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

@[simp]

theorem MonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : G → R) (a : G) (b : k) :

(liftNC f g) (single a b) = f b * g a

@[irreducible]

def MonoidAlgebra.mul' {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f g : MonoidAlgebra k G) :

MonoidAlgebra k G

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₂)

instance MonoidAlgebra.instMul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] :

Mul (MonoidAlgebra k G)

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' }

theorem MonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {f g : MonoidAlgebra k G} :

f * g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => single (a₁ * a₂) (b₁ * b₂)

instance MonoidAlgebra.nonUnitalNonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] :

NonUnitalNonAssocSemiring (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

theorem MonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Mul G] [Semiring R] {g_hom : Type u_3} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a b : MonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g y)) :

(liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

instance MonoidAlgebra.nonUnitalSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [Semigroup G] :

NonUnitalSemiring (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonUnitalSemiring = NonUnitalSemiring.mk ⋯

instance MonoidAlgebra.one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :

One (MonoidAlgebra k G)

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 }

theorem MonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :

1 = single 1 1

@[simp]

theorem MonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [NonAssocSemiring R] [Semiring k] [One G] {g_hom : Type u_3} [FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) :

(liftNC ↑f ⇑g) 1 = 1

instance MonoidAlgebra.nonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] :

NonAssocSemiring (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

theorem MonoidAlgebra.natCast_def {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (n : ℕ) :

↑n = single 1 ↑n

Semiring structure #

instance MonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :

Semiring (MonoidAlgebra k G)

Equations

MonoidAlgebra.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯

def MonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid G] [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) :

MonoidAlgebra k G →+* R

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' := ⋯ }

instance MonoidAlgebra.nonUnitalCommSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [CommSemigroup G] :

NonUnitalCommSemiring (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

instance MonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [Nonempty G] :

Nontrivial (MonoidAlgebra k G)

Derived instances #

instance MonoidAlgebra.commSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [CommMonoid G] :

CommSemiring (MonoidAlgebra k G)

Equations

MonoidAlgebra.commSemiring = CommSemiring.mk ⋯

instance MonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] :

Unique (MonoidAlgebra k G)

Equations

MonoidAlgebra.unique = Finsupp.uniqueOfRight

instance MonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :

AddCommGroup (MonoidAlgebra k G)

Equations

MonoidAlgebra.addCommGroup = Finsupp.instAddCommGroup

instance MonoidAlgebra.nonUnitalNonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [Mul G] :

NonUnitalNonAssocRing (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance MonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [Semigroup G] :

NonUnitalRing (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonUnitalRing = NonUnitalRing.mk ⋯

instance MonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] :

NonAssocRing (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem MonoidAlgebra.intCast_def {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] (z : ℤ) :

↑z = single 1 ↑z

instance MonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [Monoid G] :

Ring (MonoidAlgebra k G)

Equations

MonoidAlgebra.ring = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MonoidAlgebra.nonUnitalCommRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommSemigroup G] :

NonUnitalCommRing (MonoidAlgebra k G)

Equations

MonoidAlgebra.nonUnitalCommRing = NonUnitalCommRing.mk ⋯

instance MonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommMonoid G] :

CommRing (MonoidAlgebra k G)

Equations

MonoidAlgebra.commRing = CommRing.mk ⋯

instance MonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :

SMulZeroClass R (MonoidAlgebra k G)

Equations

MonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass

instance MonoidAlgebra.noZeroSMulDivisors {k : Type u₁} {G : Type u₂} {R : Type u_2} [Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] :

NoZeroSMulDivisors R (MonoidAlgebra k G)

instance MonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] :

DistribSMul R (MonoidAlgebra k G)

Equations

MonoidAlgebra.distribSMul = Finsupp.distribSMul G k

instance MonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] :

DistribMulAction R (MonoidAlgebra k G)

Equations

MonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k

instance MonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] :

Module R (MonoidAlgebra k G)

Equations

MonoidAlgebra.module = Finsupp.module G k

instance MonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :

FaithfulSMul R (MonoidAlgebra k G)

instance MonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :

IsScalarTower R S (MonoidAlgebra k G)

instance MonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :

SMulCommClass R S (MonoidAlgebra k G)

instance MonoidAlgebra.isCentralScalar {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k] [IsCentralScalar R k] :

IsCentralScalar R (MonoidAlgebra k G)

def MonoidAlgebra.comapDistribMulActionSelf {k : Type u₁} {G : Type u₂} [Group G] [Semiring k] :

DistribMulAction G (MonoidAlgebra k G)

This is not an instance as it conflicts with MonoidAlgebra.distribMulAction when G = kˣ.

Equations

MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction

@[simp]

theorem MonoidAlgebra.smul_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) :

c • single a b = single a (c • b)

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.

theorem MonoidAlgebra.ext {k : Type u₁} {G : Type u₂} [Semiring k] ⦃f g : MonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) :

f = g

A copy of Finsupp.ext for MonoidAlgebra.

@[reducible, inline]

abbrev MonoidAlgebra.singleAddHom {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

k →+ MonoidAlgebra k G

A copy of Finsupp.singleAddHom for MonoidAlgebra.

Equations

MonoidAlgebra.singleAddHom a = Finsupp.singleAddHom a

@[simp]

theorem MonoidAlgebra.singleAddHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :

(singleAddHom a) b = single a b

theorem MonoidAlgebra.addHom_ext' {k : Type u₁} {G : Type u₂} {N : Type u_3} [Semiring k] [AddZeroClass N] ⦃f g : MonoidAlgebra k G →+ N⦄ (H : ∀ (x : G), f.comp (singleAddHom x) = g.comp (singleAddHom x)) :

f = g

A copy of Finsupp.addHom_ext' for MonoidAlgebra.

theorem MonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f g : MonoidAlgebra k G →+[R] N} (h : ∀ (a : G), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) :

f = g

A copy of Finsupp.distribMulActionHom_ext' for MonoidAlgebra.

@[reducible, inline]

abbrev MonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) :

k →ₗ[R] MonoidAlgebra k G

A copy of Finsupp.lsingle for MonoidAlgebra.

Equations

MonoidAlgebra.lsingle a = Finsupp.lsingle a

@[simp]

theorem MonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :

(lsingle a) b = single a b

theorem MonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] ⦃f g : MonoidAlgebra k G →ₗ[R] N⦄ (H : ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x) :

f = g

A copy of Finsupp.lhom_ext' for MonoidAlgebra.

theorem MonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f g : MonoidAlgebra k G) (x : G) :

(f * g) x = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => if a₁ * a₂ = x then b₁ * b₂ else 0

theorem MonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) :

(f * g) x = ∑ p ∈ s, f p.1 * g p.2

@[simp]

theorem MonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} :

single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂)

theorem MonoidAlgebra.single_commute_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :

Commute (single a₁ b₁) (single a₂ b₂)

theorem MonoidAlgebra.single_commute {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a : G} {b : k} (ha : ∀ (a' : G), Commute a a') (hb : ∀ (b' : k), Commute b b') (f : MonoidAlgebra k G) :

Commute (single a b) f

@[simp]

theorem MonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {a : G} {b : k} (n : ℕ) :

single a b ^ n = single (a ^ n) (b ^ n)

def MonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] :

G →ₙ* MonoidAlgebra k G

The embedding of a magma into its magma algebra.

Equations

MonoidAlgebra.ofMagma k G = { toFun := fun (a : G) => MonoidAlgebra.single a 1, map_mul' := ⋯ }

@[simp]

theorem MonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] (a : G) :

(ofMagma k G) a = single a 1

def MonoidAlgebra.of (k : Type u₁) (G : Type u₂) [Semiring k] [MulOneClass G] :

G →* MonoidAlgebra k G

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' := ⋯ }

@[simp]

theorem MonoidAlgebra.of_apply (k : Type u₁) (G : Type u₂) [Semiring k] [MulOneClass G] (a : G) :

(of k G) a = single a 1

theorem MonoidAlgebra.smul_single' {k : Type u₁} {G : Type u₂} [Semiring k] (c : k) (a : G) (b : k) :

c • single a b = single a (c * b)

Copy of Finsupp.smul_single' that avoids the MonoidAlgebra = Finsupp defeq abuse.

theorem MonoidAlgebra.smul_of {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (g : G) (r : k) :

r • (of k G) g = single g r

theorem MonoidAlgebra.of_injective {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] [Nontrivial k] :

Function.Injective ⇑(of k G)

theorem MonoidAlgebra.of_commute {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] {a : G} (h : ∀ (a' : G), Commute a a') (f : MonoidAlgebra k G) :

Commute ((of k G) a) f

def MonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] :

k × G →* MonoidAlgebra k G

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' := ⋯ }

@[simp]

theorem MonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (a : k × G) :

singleHom a = single a.2 a.1

theorem MonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ a ∈ f.support, a * x = z ↔ a = y) :

(f * single x r) z = f y * r

theorem MonoidAlgebra.mul_single_one_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :

(f * single 1 r) x = f x * r

theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G) (h : ¬∃ (d : G), g' = d * g) :

(x * single g r) g' = 0

theorem MonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ a ∈ f.support, x * a = y ↔ a = z) :

(single x r * f) y = r * f z

theorem MonoidAlgebra.single_one_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :

(single 1 r * f) x = r * f x

theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G) (h : ¬∃ (d : G), g' = g * d) :

(single g r * x) g' = 0

theorem MonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] {R : Type u_3} [Semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : MonoidAlgebra k G) :

(liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Non-unital, non-associative algebra structure #

instance MonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [IsScalarTower R k k] :

IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G)

instance MonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [SMulCommClass R k k] :

SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G)

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.

instance MonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [SMulCommClass k R k] :

SMulCommClass (MonoidAlgebra k G) R (MonoidAlgebra k G)

theorem MonoidAlgebra.single_one_comm {k : Type u₁} {G : Type u₂} [CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) :

single 1 r * f = f * single 1 r

def MonoidAlgebra.singleOneRingHom {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] :

k →+* MonoidAlgebra k G

Finsupp.single 1 as a RingHom

Equations

MonoidAlgebra.singleOneRingHom = { toFun := MonoidAlgebra.single 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

MonoidAlgebra.isLocalHom_singleOneRingHom

@[simp]

theorem MonoidAlgebra.singleOneRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (b : k) :

singleOneRingHom b = single 1 b

theorem MonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R} (h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)) (h_of : ∀ (a : G), f (single a 1) = g (single a 1)) :

f = g

If two ring homomorphisms from MonoidAlgebra k G are equal on all single a 1 and single 1 b, then they are equal.

theorem MonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R} (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom) (h_of : (↑f).comp (of k G) = (↑g).comp (of k G)) :

f = g

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

theorem MonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G) (hM : ∀ (g : G), p ((of k G) g)) (hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)) (hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)) :

p f

theorem MonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :

∏ i ∈ s, single (a i) (b i) = single (∏ i ∈ s, a i) (∏ i ∈ s, b i)

@[simp]

theorem MonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (r : k) (x y : G) :

(f * single x r) y = f (y * x⁻¹) * r

@[simp]

theorem MonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) :

(single x r * f) y = r * f (x⁻¹ * y)

theorem MonoidAlgebra.mul_apply_left {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f g : MonoidAlgebra k G) (x : G) :

(f * g) x = Finsupp.sum f fun (a : G) (b : k) => b * g (a⁻¹ * x)

theorem MonoidAlgebra.mul_apply_right {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f g : MonoidAlgebra k G) (x : G) :

(f * g) x = Finsupp.sum g fun (a : G) (b : k) => f (x * a⁻¹) * b

noncomputable def MonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :

(MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ

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.

@[simp]

theorem MonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (a✝ : (G →₀ k)ᵐᵒᵖ) :

MonoidAlgebra.opRingEquiv a✝ = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝))

@[simp]

theorem MonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (a✝ : Gᵐᵒᵖ →₀ kᵐᵒᵖ) :

MonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a✝))

theorem MonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (r : k) (x : G) :

MonoidAlgebra.opRingEquiv (MulOpposite.op (single x r)) = single (MulOpposite.op x) (MulOpposite.op r)

theorem MonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :

MonoidAlgebra.opRingEquiv.symm (single x r) = MulOpposite.op (single (MulOpposite.unop x) (MulOpposite.unop r))

def MonoidAlgebra.submoduleOfSMulMem {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {V : Type u_3} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (W : Submodule k V) (h : ∀ (g : G), ∀ v ∈ W, (of k G) g • v ∈ W) :

Submodule (MonoidAlgebra k G) V

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' := ⋯ }

instance MonoidAlgebra.isLocalHom_singleOneRingHom {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :

IsLocalHom singleOneRingHom

Additive monoids #

def AddMonoidAlgebra (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, denoted by k[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

def AddMonoidAlgebra.«term_[_]» :

Lean.TrailingParserDescr

The monoid algebra over a semiring k generated by the additive monoid G, denoted by k[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.

instance AddMonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [Semiring k] :

Inhabited (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.inhabited k G = inferInstanceAs (Inhabited (G →₀ k))

instance AddMonoidAlgebra.addCommMonoid (k : Type u₁) (G : Type u₂) [Semiring k] :

AddCommMonoid (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.addCommMonoid k G = inferInstanceAs (AddCommMonoid (G →₀ k))

instance AddMonoidAlgebra.instIsCancelAdd (k : Type u₁) (G : Type u₂) [Semiring k] [IsCancelAdd k] :

IsCancelAdd (AddMonoidAlgebra k G)

instance AddMonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] :

CoeFun (AddMonoidAlgebra k G) fun (x : AddMonoidAlgebra k G) => G → k

Equations

AddMonoidAlgebra.coeFun k G = inferInstanceAs (CoeFun (G →₀ k) fun (x : G →₀ k) => G → k)

@[reducible, inline]

abbrev AddMonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :

AddMonoidAlgebra k G

Equations

AddMonoidAlgebra.single a b = Finsupp.single a b

theorem AddMonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

single a 0 = 0

theorem AddMonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b₁ b₂ : k) :

single a (b₁ + b₂) = single a b₁ + single a b₂

@[simp]

theorem AddMonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [Semiring k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) :

Finsupp.sum (single a b) h = h a b

@[simp]

theorem AddMonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [Semiring k] (f : AddMonoidAlgebra k G) :

Finsupp.sum f single = f

theorem AddMonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [Semiring k] {a a' : G} {b : k} [Decidable (a = a')] :

(single a b) a' = if a = a' then b else 0

@[simp]

theorem AddMonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {b : k} :

single a b = 0 ↔ b = 0

def AddMonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative G → R) :

AddMonoidAlgebra k G →+ R

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

@[simp]

theorem AddMonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative G → R) (a : G) (b : k) :

(liftNC f g) (single a b) = f b * g (Multiplicative.ofAdd a)

instance AddMonoidAlgebra.hasMul {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] :

Mul (AddMonoidAlgebra k G)

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 }

theorem AddMonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {f g : AddMonoidAlgebra k G} :

f * g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => single (a₁ + a₂) (b₁ * b₂)

instance AddMonoidAlgebra.nonUnitalNonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] :

NonUnitalNonAssocSemiring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

theorem AddMonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Add G] [Semiring R] {g_hom : Type u_3} [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) (a b : AddMonoidAlgebra k G) (h_comm : ∀ {x y : G}, y ∈ a.support → Commute (f (b x)) (g (Multiplicative.ofAdd y))) :

(liftNC ↑f ⇑g) (a * b) = (liftNC ↑f ⇑g) a * (liftNC ↑f ⇑g) b

instance AddMonoidAlgebra.one {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] :

One (AddMonoidAlgebra k G)

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 }

theorem AddMonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] :

1 = single 0 1

@[simp]

theorem AddMonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Zero G] [NonAssocSemiring R] {g_hom : Type u_3} [FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) :

(liftNC ↑f ⇑g) 1 = 1

instance AddMonoidAlgebra.nonUnitalSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddSemigroup G] :

NonUnitalSemiring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonUnitalSemiring = NonUnitalSemiring.mk ⋯

instance AddMonoidAlgebra.nonAssocSemiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] :

NonAssocSemiring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯

theorem AddMonoidAlgebra.natCast_def {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (n : ℕ) :

↑n = single 0 ↑n

Semiring structure #

instance AddMonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :

SMulZeroClass R (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass

instance AddMonoidAlgebra.noZeroSMulDivisors {k : Type u₁} {G : Type u₂} {R : Type u_2} [Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] :

NoZeroSMulDivisors R (AddMonoidAlgebra k G)

instance AddMonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] :

Semiring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRecAuto ⋯ ⋯

def AddMonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [AddMonoid G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) :

AddMonoidAlgebra k G →+* R

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' := ⋯ }

instance AddMonoidAlgebra.nonUnitalCommSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddCommSemigroup G] :

NonUnitalCommSemiring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonUnitalCommSemiring = NonUnitalCommSemiring.mk ⋯

instance AddMonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [Nonempty G] :

Nontrivial (AddMonoidAlgebra k G)

Derived instances #

instance AddMonoidAlgebra.commSemiring {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddCommMonoid G] :

CommSemiring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.commSemiring = CommSemiring.mk ⋯

instance AddMonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] :

Unique (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.unique = Finsupp.uniqueOfRight

instance AddMonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :

AddCommGroup (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.addCommGroup = Finsupp.instAddCommGroup

instance AddMonoidAlgebra.nonUnitalNonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [Add G] :

NonUnitalNonAssocRing (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

instance AddMonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [AddSemigroup G] :

NonUnitalRing (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonUnitalRing = NonUnitalRing.mk ⋯

instance AddMonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] :

NonAssocRing (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem AddMonoidAlgebra.intCast_def {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] (z : ℤ) :

↑z = single 0 ↑z

instance AddMonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [AddMonoid G] :

Ring (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.ring = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddMonoidAlgebra.nonUnitalCommRing {k : Type u₁} {G : Type u₂} [CommRing k] [AddCommSemigroup G] :

NonUnitalCommRing (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.nonUnitalCommRing = NonUnitalCommRing.mk ⋯

instance AddMonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [AddCommMonoid G] :

CommRing (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.commRing = CommRing.mk ⋯

instance AddMonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] :

DistribSMul R (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.distribSMul = Finsupp.distribSMul G k

instance AddMonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] :

DistribMulAction R (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.distribMulAction = Finsupp.distribMulAction G k

instance AddMonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :

FaithfulSMul R (AddMonoidAlgebra k G)

instance AddMonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] :

Module R (AddMonoidAlgebra k G)

Equations

AddMonoidAlgebra.module = Finsupp.module G k

instance AddMonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :

IsScalarTower R S (AddMonoidAlgebra k G)

instance AddMonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :

SMulCommClass R S (AddMonoidAlgebra k G)

instance AddMonoidAlgebra.isCentralScalar {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k] [IsCentralScalar R k] :

IsCentralScalar R (AddMonoidAlgebra k G)

It is hard to state the equivalent of DistribMulAction G k[G] because we've never discussed actions of additive groups.

@[simp]

theorem AddMonoidAlgebra.smul_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) :

c • single a b = single a (c • b)

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.

theorem AddMonoidAlgebra.ext {k : Type u₁} {G : Type u₂} [Semiring k] ⦃f g : AddMonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) :

f = g

A copy of Finsupp.ext for AddMonoidAlgebra.

@[reducible, inline]

abbrev AddMonoidAlgebra.singleAddHom {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

k →+ AddMonoidAlgebra k G

A copy of Finsupp.singleAddHom for AddMonoidAlgebra.

Equations

AddMonoidAlgebra.singleAddHom a = Finsupp.singleAddHom a

@[simp]

theorem AddMonoidAlgebra.singleAddHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :

(singleAddHom a) b = single a b

theorem AddMonoidAlgebra.addHom_ext' {k : Type u₁} {G : Type u₂} {N : Type u_3} [Semiring k] [AddZeroClass N] ⦃f g : AddMonoidAlgebra k G →+ N⦄ (H : ∀ (x : G), f.comp (singleAddHom x) = g.comp (singleAddHom x)) :

f = g

A copy of Finsupp.addHom_ext' for AddMonoidAlgebra.

theorem AddMonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f g : AddMonoidAlgebra k G →+[R] N} (h : ∀ (a : G), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) :

f = g

A copy of Finsupp.distribMulActionHom_ext' for AddMonoidAlgebra.

@[reducible, inline]

abbrev AddMonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) :

k →ₗ[R] AddMonoidAlgebra k G

A copy of Finsupp.lsingle for AddMonoidAlgebra.

Equations

AddMonoidAlgebra.lsingle a = Finsupp.lsingle a

@[simp]

theorem AddMonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :

(lsingle a) b = single a b

theorem AddMonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] ⦃f g : AddMonoidAlgebra k G →ₗ[R] N⦄ (H : ∀ (x : G), f ∘ₗ lsingle x = g ∘ₗ lsingle x) :

f = g

A copy of Finsupp.lhom_ext' for AddMonoidAlgebra.

theorem AddMonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Add G] (f g : AddMonoidAlgebra k G) (x : G) :

(f * g) x = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => if a₁ + a₂ = x then b₁ * b₂ else 0

theorem AddMonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f g : AddMonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 + p.2 = x) :

(f * g) x = ∑ p ∈ s, f p.1 * g p.2

theorem AddMonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {a₁ a₂ : G} {b₁ b₂ : k} :

single a₁ b₁ * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂)

theorem AddMonoidAlgebra.single_commute_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {a₁ a₂ : G} {b₁ b₂ : k} (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) :

Commute (single a₁ b₁) (single a₂ b₂)

theorem AddMonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] {a : G} {b : k} (n : ℕ) :

single a b ^ n = single (n • a) (b ^ n)

def AddMonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [Semiring k] [Add G] :

Multiplicative G →ₙ* AddMonoidAlgebra k G

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' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [Semiring k] [Add G] (a : Multiplicative G) :

(ofMagma k G) a = single a 1

def AddMonoidAlgebra.of (k : Type u₁) (G : Type u₂) [Semiring k] [AddZeroClass G] :

Multiplicative G →* AddMonoidAlgebra k G

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' := ⋯ }

def AddMonoidAlgebra.of' (k : Type u₁) (G : Type u₂) [Semiring k] :

G → AddMonoidAlgebra k G

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

@[simp]

theorem AddMonoidAlgebra.of_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : Multiplicative G) :

(of k G) a = single (Multiplicative.toAdd a) 1

@[simp]

theorem AddMonoidAlgebra.of'_apply {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

of' k G a = single a 1

theorem AddMonoidAlgebra.of'_eq_of {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : G) :

of' k G a = (of k G) (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.of_injective {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [AddZeroClass G] :

Function.Injective ⇑(of k G)

theorem AddMonoidAlgebra.of'_commute {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] {a : G} (h : ∀ (a' : G), AddCommute a a') (f : AddMonoidAlgebra k G) :

Commute (of' k G a) f

def AddMonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] :

k × Multiplicative G →* AddMonoidAlgebra k G

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' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : k × Multiplicative G) :

singleHom a = single (Multiplicative.toAdd a.2) a.1

theorem AddMonoidAlgebra.smul_single' {k : Type u₁} {G : Type u₂} [Semiring k] (c : k) (a : G) (b : k) :

c • single a b = single a (c * b)

Copy of Finsupp.smul_single' that avoids the AddMonoidAlgebra = Finsupp defeq abuse.

theorem AddMonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (r : k) (x y z : G) (H : ∀ a ∈ f.support, a + x = z ↔ a = y) :

(f * single x r) z = f y * r

theorem AddMonoidAlgebra.mul_single_zero_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k) (x : G) :

(f * single 0 r) x = f x * r

theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (r : k) {g g' : G} (x : AddMonoidAlgebra k G) (h : ¬∃ (d : G), g' = d + g) :

(x * single g r) g' = 0

theorem AddMonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (r : k) (x y z : G) (H : ∀ a ∈ f.support, x + a = y ↔ a = z) :

(single x r * f) y = r * f z

theorem AddMonoidAlgebra.single_zero_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k) (x : G) :

(single 0 r * f) x = r * f x

theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (r : k) {g g' : G} (x : AddMonoidAlgebra k G) (h : ¬∃ (d : G), g' = g + d) :

(single g r * x) g' = 0

theorem AddMonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddGroup G] (f : AddMonoidAlgebra k G) (r : k) (x y : G) :

(f * single x r) y = f (y - x) * r

theorem AddMonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddGroup G] (r : k) (x : G) (f : AddMonoidAlgebra k G) (y : G) :

(single x r * f) y = r * f (-x + y)

theorem AddMonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] {R : Type u_3} [AddZeroClass G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) :

(liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

theorem AddMonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] {p : AddMonoidAlgebra k G → Prop} (f : AddMonoidAlgebra k G) (hM : ∀ (g : G), p ((of k G) (Multiplicative.ofAdd g))) (hadd : ∀ (f g : AddMonoidAlgebra k G), p f → p g → p (f + g)) (hsmul : ∀ (r : k) (f : AddMonoidAlgebra k G), p f → p (r • f)) :

p f

Non-unital, non-associative algebra structure #

instance AddMonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [IsScalarTower R k k] :

IsScalarTower R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G)

instance AddMonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [SMulCommClass R k k] :

SMulCommClass R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G)

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.

instance AddMonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [SMulCommClass k R k] :

SMulCommClass (AddMonoidAlgebra k G) R (AddMonoidAlgebra k G)

Algebra structure #

def AddMonoidAlgebra.singleZeroRingHom {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] :

k →+* AddMonoidAlgebra k G

Finsupp.single 0 as a RingHom

Equations

AddMonoidAlgebra.singleZeroRingHom = { toFun := AddMonoidAlgebra.single 0, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Instances For

AddMonoidAlgebra.isLocalHom_singleZeroRingHom

@[simp]

theorem AddMonoidAlgebra.singleZeroRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] (b : k) :

singleZeroRingHom b = single 0 b

theorem AddMonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f g : AddMonoidAlgebra k G →+* R} (h₀ : ∀ (b : k), f (single 0 b) = g (single 0 b)) (h_of : ∀ (a : G), f (single a 1) = g (single a 1)) :

f = g

If two ring homomorphisms from k[G] are equal on all single a 1 and single 0 b, then they are equal.

theorem AddMonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f g : AddMonoidAlgebra k G →+* R} (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom) (h_of : (↑f).comp (of k G) = (↑g).comp (of k G)) :

f = g

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

noncomputable def AddMonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] :

(AddMonoidAlgebra k G)ᵐᵒᵖ ≃+* AddMonoidAlgebra kᵐᵒᵖ G

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' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (a✝ : G →₀ kᵐᵒᵖ) :

AddMonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ a✝)

@[simp]

theorem AddMonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (a✝ : (G →₀ k)ᵐᵒᵖ) :

AddMonoidAlgebra.opRingEquiv a✝ = Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝)

theorem AddMonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (r : k) (x : G) :

AddMonoidAlgebra.opRingEquiv (MulOpposite.op (single x r)) = single x (MulOpposite.op r)

theorem AddMonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :

AddMonoidAlgebra.opRingEquiv.symm (single x r) = MulOpposite.op (single x (MulOpposite.unop r))

theorem AddMonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :

∏ i ∈ s, single (a i) (b i) = single (∑ i ∈ s, a i) (∏ i ∈ s, b i)

instance AddMonoidAlgebra.isLocalHom_singleZeroRingHom {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] :

IsLocalHom singleZeroRingHom